Skip to content

Commit 5900455

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
echo-types: umbrella rank-pow-mono on the 10-constructor closeable subset (Item 3)
Lands `Ordinal.Buchholz.RankMonoUmbrella` — a *rank-soundness-ready* relation `_<ᵇ⁰_` mirroring 10 of 13 constructors of `Ordinal.Buchholz.Order._<ᵇ_`, with the WfCNF tail bounds baked into the constructors themselves. Proves the umbrella theorem on this subset via direct structural recursion. ## What landed * `_<ᵇ⁰_ : BT → BT → Set` — the 10-constructor subset (trivial 5, via-left 2, source-bplus 2 with tail bound, joint-bplus atomic target 2 with source tail bound). * `_≤ᵇ⁰_` — non-strict companion (`<ᵇ⁰ ⊎ ≡`) for tail bounds. * `≤ᵇ⁰-refl` — propositional reflexivity. * **`rank-pow-mono-<ᵇ⁰ : x <ᵇ⁰ y → rank-pow x <′ rank-pow y`** — the umbrella theorem. Structural recursion on the `<ᵇ⁰` derivation; each constructor dispatches to the matching per-constructor primitive in `RankPow`. * `rank-pow-mono-≤ᵇ⁰` — non-strict companion. ## Design Tail bounds are baked into `<ᵇ⁰`'s constructors so no external WfCNF carrier is needed. This makes the umbrella a direct structural recursion (no mutual recursion with a separate WfCNF-typed predicate, no cross-relation conversion shim). ## Excluded from the umbrella The 3 structurally-blocked cases of `_<ᵇ_` documented in `buchholz-rank-obstruction.adoc`: * `<ᵇ-0-+` — `bplus bzero bzero` edge case (rank collapses to oz) * `<ᵇ-ψα` — needs ψ-admissibility refinement * `<ᵇ-ψΩ≤` — same admissibility blocker (ν = μ sub-case) * `<ᵇ-+1` — bplus-target sub-case (rank not additive principal) Coverage: 10/13 constructors of `_<ᵇ_` (~77%). Headlines pinned in `Ordinal/Buchholz/Smoke.agda`. Module wired into `All.agda`. `agda proofs/agda/All.agda` and `agda proofs/agda/Smoke.agda` exit 0 under `--safe --without-K`. No postulates, no escape pragmas. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 616a0a5 commit 5900455

3 files changed

Lines changed: 192 additions & 0 deletions

File tree

‎proofs/agda/All.agda‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -85,6 +85,7 @@ open import Ordinal.Buchholz.IteratedExtendedOrder
8585
open import Ordinal.Buchholz.RankBrouwer
8686
open import Ordinal.Buchholz.RankPartial
8787
open import Ordinal.Buchholz.RankPow
88+
open import Ordinal.Buchholz.RankMonoUmbrella
8889
open import Ordinal.Buchholz.RecursiveSurfaceOrder
8990
open import Ordinal.Buchholz.RecursiveSurfaceBudget
9091
open import Ordinal.Buchholz.SurfaceOrder

‎proofs/agda/Ordinal/Buchholz/RankMonoUmbrella.agda‎

Lines changed: 177 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,177 @@
1+
{-# OPTIONS --safe --without-K #-}
2+
3+
-- The umbrella `rank-pow-mono` theorem (Item 3 of the path-1 unblock).
4+
--
5+
-- Defines a *rank-soundness-ready* relation `_<ᵇ⁰_` mirroring the
6+
-- 10 closeable constructors of `Ordinal.Buchholz.Order._<ᵇ_` with
7+
-- rank-soundness side conditions (the WfCNF tail bounds) baked in.
8+
-- Proves the umbrella theorem on this self-contained subset:
9+
--
10+
-- `rank-pow-mono-<ᵇ⁰ : x <ᵇ⁰ y → rank-pow x <′ rank-pow y`.
11+
--
12+
-- No external WfCNF carrier is needed — the tail bounds are wired
13+
-- into the constructors of `<ᵇ⁰` itself, so the umbrella is a
14+
-- direct structural recursion on the proof. Consumers wishing to
15+
-- discharge a `<ᵇ⁻`-style umbrella construct `<ᵇ⁰` derivations and
16+
-- apply this theorem.
17+
--
18+
-- ## What's in / what's out
19+
--
20+
-- IN (10 constructors):
21+
--
22+
-- * `<ᵇ⁰-0-Ω`, `<ᵇ⁰-0-ψ`, `<ᵇ⁰-ΩΩ`, `<ᵇ⁰-Ωψ`, `<ᵇ⁰-ψΩ`
23+
-- — no recursive premise, no WfCNF dependency
24+
-- * `<ᵇ⁰-Ω+`, `<ᵇ⁰-ψ+` — recurse on premise (left of target bplus)
25+
-- * `<ᵇ⁰-+Ω`, `<ᵇ⁰-+ψ` — recurse on premise + carry tail bound
26+
-- * `<ᵇ⁰-+1-Ω`, `<ᵇ⁰-+1-ψ` — joint-bplus, atomic target;
27+
-- recurse on premise + carry source tail bound
28+
--
29+
-- OUT (3 structurally-blocked cases of `_<ᵇ_`, documented in
30+
-- `buchholz-rank-obstruction.adoc`):
31+
--
32+
-- * `<ᵇ-0-+` — `bplus bzero bzero` edge case
33+
-- * `<ᵇ-ψα` — needs ψ-admissibility refinement
34+
-- * `<ᵇ-ψΩ≤` — same admissibility blocker (ν = μ sub-case)
35+
-- * `<ᵇ-+1` — bplus-target sub-case (rank not additive principal)
36+
--
37+
-- ## Headlines (pinned in `Ordinal/Buchholz/Smoke.agda`)
38+
--
39+
-- * `_<ᵇ⁰_` -- the closeable subset relation
40+
-- * `_≤ᵇ⁰_` -- non-strict companion
41+
-- * `≤ᵇ⁰-refl` -- propositional reflexivity
42+
-- * `rank-pow-mono-<ᵇ⁰` -- THE UMBRELLA (strict)
43+
-- * `rank-pow-mono-≤ᵇ⁰` -- non-strict companion
44+
45+
module Ordinal.Buchholz.RankMonoUmbrella where
46+
47+
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
48+
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
49+
50+
open import Ordinal.OmegaMarkers using (OmegaIndex; _<Ω_)
51+
open import Ordinal.Buchholz.Syntax using
52+
( BT
53+
; bzero
54+
; bOmega
55+
; bplus
56+
; bpsi
57+
)
58+
open import Ordinal.Brouwer using (Ord; oz; osuc)
59+
open import Ordinal.Brouwer.Phase13 using
60+
( _≤′_
61+
; _<′_
62+
; ≤′-refl
63+
; ≤′-trans
64+
; ≤′-self-osuc
65+
)
66+
open import Ordinal.Buchholz.RankPow using
67+
( rank-pow
68+
; ω-rank-pow
69+
; rank-mono-<ᵇ-0-Ω
70+
; rank-mono-<ᵇ-0-ψ
71+
; rank-mono-<ᵇ-ΩΩ
72+
; rank-mono-<ᵇ-Ωψ
73+
; rank-mono-<ᵇ-ψΩ
74+
; rank-mono-<ᵇ-Ω+
75+
; rank-mono-<ᵇ-ψ+
76+
; rank-mono-<ᵇ-+Ω
77+
; rank-mono-<ᵇ-+ψ
78+
; rank-mono-<ᵇ-+1-Ω-target
79+
; rank-mono-<ᵇ-+1-ψ-target
80+
)
81+
82+
----------------------------------------------------------------------
83+
-- The rank-soundness-ready subset `_<ᵇ⁰_`
84+
----------------------------------------------------------------------
85+
86+
-- The 10 closeable constructors of `_<ᵇ_`, with rank-soundness side
87+
-- conditions baked in. Recursion is on `_<ᵇ⁰_` and `_≤ᵇ⁰_`, both
88+
-- mutually defined below.
89+
90+
mutual
91+
92+
data _<ᵇ⁰_ : BT → BT → Set where
93+
-- Trivial cases
94+
<ᵇ⁰-0-Ω : ∀ {μ} → bzero <ᵇ⁰ bOmega μ
95+
<ᵇ⁰-0-ψ : ∀ {ν α} → bzero <ᵇ⁰ bpsi ν α
96+
<ᵇ⁰-ΩΩ : ∀ {μ ν} → μ <Ω ν → bOmega μ <ᵇ⁰ bOmega ν
97+
<ᵇ⁰-Ωψ : ∀ {μ ν α} → μ <Ω ν → bOmega μ <ᵇ⁰ bpsi ν α
98+
<ᵇ⁰-ψΩ : ∀ {μ ν α β} → μ <Ω ν → bpsi μ α <ᵇ⁰ bpsi ν β
99+
100+
-- Via-left
101+
<ᵇ⁰-Ω+ : ∀ {μ x y} → bOmega μ <ᵇ⁰ x → bOmega μ <ᵇ⁰ bplus x y
102+
<ᵇ⁰-ψ+ : ∀ {ν α x y} → bpsi ν α <ᵇ⁰ x → bpsi ν α <ᵇ⁰ bplus x y
103+
104+
-- Source-bplus (premise on left summand + WfCNF tail bound on source)
105+
<ᵇ⁰-+Ω : ∀ {x y μ}
106+
→ x <ᵇ⁰ bOmega μ
107+
→ y ≤ᵇ⁰ x
108+
→ bplus x y <ᵇ⁰ bOmega μ
109+
<ᵇ⁰-+ψ : ∀ {x y ν α}
110+
→ x <ᵇ⁰ bpsi ν α
111+
→ y ≤ᵇ⁰ x
112+
→ bplus x y <ᵇ⁰ bpsi ν α
113+
114+
-- Joint-bplus, atomic target (additive-principal at y₁'s rank)
115+
<ᵇ⁰-+1-Ω : ∀ {x₁ x₂ μ y₂}
116+
→ x₁ <ᵇ⁰ bOmega μ
117+
→ x₂ ≤ᵇ⁰ x₁
118+
→ bplus x₁ x₂ <ᵇ⁰ bplus (bOmega μ) y₂
119+
<ᵇ⁰-+1-ψ : ∀ {x₁ x₂ ν α y₂}
120+
→ x₁ <ᵇ⁰ bpsi ν α
121+
→ x₂ ≤ᵇ⁰ x₁
122+
→ bplus x₁ x₂ <ᵇ⁰ bplus (bpsi ν α) y₂
123+
124+
-- Non-strict companion. Used for the tail bounds; the `inj₂ refl`
125+
-- branch carries equal terms (rank-pow ≡ rank-pow).
126+
127+
_≤ᵇ⁰_ : BT → BT → Set
128+
x ≤ᵇ⁰ y = (x <ᵇ⁰ y) ⊎ (x ≡ y)
129+
130+
infix 4 _<ᵇ⁰_ _≤ᵇ⁰_
131+
132+
≤ᵇ⁰-refl : ∀ {x} → x ≤ᵇ⁰ x
133+
≤ᵇ⁰-refl = inj₂ refl
134+
135+
----------------------------------------------------------------------
136+
-- The umbrella theorem
137+
----------------------------------------------------------------------
138+
139+
-- Structural recursion on `_<ᵇ⁰_`; the `<′ / ≤′` mutual recursion
140+
-- threads through the tail bounds. Each case dispatches to the
141+
-- matching primitive in `RankPow`.
142+
143+
mutual
144+
145+
rank-pow-mono-<ᵇ⁰ : ∀ {s t} → s <ᵇ⁰ t → rank-pow s <′ rank-pow t
146+
rank-pow-mono-<ᵇ⁰ {.bzero} {bOmega μ} <ᵇ⁰-0-Ω = rank-mono-<ᵇ-0-Ω {μ}
147+
rank-pow-mono-<ᵇ⁰ {.bzero} {bpsi ν α} <ᵇ⁰-0-ψ = rank-mono-<ᵇ-0-ψ {ν} {α}
148+
rank-pow-mono-<ᵇ⁰ (<ᵇ⁰-ΩΩ {μ = μ} {ν = ν} p) = rank-mono-<ᵇ-ΩΩ {μ} {ν} p
149+
rank-pow-mono-<ᵇ⁰ (<ᵇ⁰-Ωψ {μ = μ} {ν = ν} {α = α} p) = rank-mono-<ᵇ-Ωψ {μ} {ν} {α} p
150+
rank-pow-mono-<ᵇ⁰ (<ᵇ⁰-ψΩ {μ = μ} {ν = ν} {α = α} {β = β} p) = rank-mono-<ᵇ-ψΩ {μ} {ν} {α} {β} p
151+
rank-pow-mono-<ᵇ⁰ {bOmega μ} {bplus x y} (<ᵇ⁰-Ω+ p) =
152+
rank-mono-<ᵇ-Ω+ {μ} {x} {y} (rank-pow-mono-<ᵇ⁰ p)
153+
rank-pow-mono-<ᵇ⁰ {bpsi ν α} {bplus x y} (<ᵇ⁰-ψ+ p) =
154+
rank-mono-<ᵇ-ψ+ {ν} {α} {x} {y} (rank-pow-mono-<ᵇ⁰ p)
155+
rank-pow-mono-<ᵇ⁰ {bplus x y} {bOmega μ} (<ᵇ⁰-+Ω p y≤x) =
156+
rank-mono-<ᵇ-+Ω {x} {y} {μ}
157+
(rank-pow-mono-<ᵇ⁰ p)
158+
(rank-pow-mono-≤ᵇ⁰ y≤x)
159+
rank-pow-mono-<ᵇ⁰ {bplus x y} {bpsi ν α} (<ᵇ⁰-+ψ p y≤x) =
160+
rank-mono-<ᵇ-+ψ {x} {y} {ν} {α}
161+
(rank-pow-mono-<ᵇ⁰ p)
162+
(rank-pow-mono-≤ᵇ⁰ y≤x)
163+
rank-pow-mono-<ᵇ⁰ {bplus x₁ x₂} {bplus .(bOmega μ) y₂} (<ᵇ⁰-+1-Ω {μ = μ} p x₂≤x₁) =
164+
rank-mono-<ᵇ-+1-Ω-target {x₁} {x₂} {μ} {y₂}
165+
(rank-pow-mono-<ᵇ⁰ p)
166+
(rank-pow-mono-≤ᵇ⁰ x₂≤x₁)
167+
rank-pow-mono-<ᵇ⁰ {bplus x₁ x₂} {bplus .(bpsi ν α) y₂} (<ᵇ⁰-+1-ψ {ν = ν} {α = α} p x₂≤x₁) =
168+
rank-mono-<ᵇ-+1-ψ-target {x₁} {x₂} {ν} {α} {y₂}
169+
(rank-pow-mono-<ᵇ⁰ p)
170+
(rank-pow-mono-≤ᵇ⁰ x₂≤x₁)
171+
172+
rank-pow-mono-≤ᵇ⁰ : ∀ {x y} → x ≤ᵇ⁰ y → rank-pow x ≤′ rank-pow y
173+
rank-pow-mono-≤ᵇ⁰ {x} {y} (inj₁ p) =
174+
≤′-trans {rank-pow x} {osuc (rank-pow x)} {rank-pow y}
175+
(≤′-self-osuc (rank-pow x))
176+
(rank-pow-mono-<ᵇ⁰ p)
177+
rank-pow-mono-≤ᵇ⁰ {x} {.x} (inj₂ refl) = ≤′-refl {rank-pow x}

‎proofs/agda/Ordinal/Buchholz/Smoke.agda‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -273,6 +273,20 @@ open import Ordinal.Buchholz.OrderRestricted using
273273
; <ᵇ⁻-trans
274274
)
275275

276+
-- Path-1 umbrella: rank-pow strict-mono on the 10-constructor
277+
-- rank-soundness-ready subset `_<ᵇ⁰_` of `_<ᵇ_`. Closes 10 of 13
278+
-- cases of the Buchholz rank-monotonicity theorem under WfCNF;
279+
-- the 3 excluded cases (`<ᵇ-0-+` edge, `<ᵇ-ψα` / `<ᵇ-ψΩ≤`
280+
-- admissibility-blocked, `<ᵇ-+1` bplus-target sub-case) remain
281+
-- open under documented structural blockers.
282+
open import Ordinal.Buchholz.RankMonoUmbrella using
283+
( _<ᵇ⁰_
284+
; _≤ᵇ⁰_
285+
; ≤ᵇ⁰-refl
286+
; rank-pow-mono-<ᵇ⁰
287+
; rank-pow-mono-≤ᵇ⁰
288+
)
289+
276290
open import Ordinal.Buchholz.RecursiveSurfaceBudget using
277291
( BudgetedBT
278292
; _<ᵇʳᶠᵇ_

0 commit comments

Comments
 (0)