Skip to content

Commit e150b35

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
proof(ordinal): doubled-ladder umbrella rank2-mono-<ᵇ² + wf-<ᵇ² (Gate 1 capstone) (#208)
## What The capstone of the doubled-ladder programme. New module `RankDoubledLadderUmbrella.agda`: ```agda _<ᵇ²_ : BT → BT → Set -- complete rank2-ready relation (all 12 constructors) rank2-mono-<ᵇ² : s <ᵇ² t → rank2 s <′ rank2 t -- THE UMBRELLA rank2-mono-≤ᵇ² : x ≤ᵇ² y → rank2 x ≤′ rank2 y -- non-strict companion wf-<ᵇ² : WellFounded _<ᵇ²_ -- well-foundedness ``` ## How `_<ᵇ²_` is a *rank2-soundness-ready* relation mirroring **all 12** core `_<ᵇ_` constructors, with the side conditions baked in: `WfAdm` witnesses for the ψ-source atomic cases, the leading-power admissibility bound `rank-pow x <′ ω-rank-pow ν` for `<ᵇ-+ψ`, and the WfCNF tail bounds `y ≤ᵇ² x` for the source-bplus cases. The umbrella is a structural recursion dispatching each case to its landed `rank2`-mono primitive (from the four primitive modules), so termination is structural — no `TERMINATING` pragma. **Completeness vs the single ladder.** `RankMonoUmbrella._<ᵇ⁰_` closes only 10 of 13 constructors — `<ᵇ-0-+`, `<ᵇ-ψΩ≤`, and the bplus-target `<ᵇ-+1` were structurally blocked under `rank-pow`. The doubled ladder closes **all 12**, because each has a landed primitive. **The `<ᵇ-+ψ` leading-power bridge.** `rank2-mono-+ψ` needs the source pieces below the ψ-block's *leading power* `ω-rank-pow (double ν)` — stronger than "below the whole ψ-rank", which is all plain recursion gives. So `<ᵇ²-+ψ` carries `WfAdm x` + `rank-pow x <′ ω-rank-pow ν`, and the umbrella transfers it to `rank2 x <′ ω-rank-pow (double ν)` through the scale-transfer bridge `rank2-bounded` (#204); the tail rides `y ≤ᵇ² x` via `rank2-mono-≤ᵇ²` + `≤′-<′-trans`. **Well-foundedness** is the standard rank-embedding transport (`Subrelation.wellFounded` + `On.wellFounded rank2 wf-<′`), the same recipe as `RankMonoUnionWF.wf-<ᵇᵘ`, routed through `rank2` — zero new proof obligations. ## Significance This is the doubled-ladder route to **well-foundedness of the core Buchholz order**, closing the Gate 1 equal-Ω programme: the equal-Ω boundary `bpsi ν α <ᵇ bOmega ν` that the single ladder could not rank is now ordered, and the complete relation is proved well-founded. ## Verification - `agda -i proofs/agda proofs/agda/All.agda` exits 0 under `--safe --without-K`. - Headlines pinned in the Buchholz `Smoke.agda` (own block). - Zero postulates / escape pragmas; structural recursion (no `TERMINATING`). https://claude.ai/code/session_017t53M7W7ubmXpwymveLcCE --- _Generated by [Claude Code](https://claude.ai/code/session_017t53M7W7ubmXpwymveLcCE)_ Co-authored-by: Claude <noreply@anthropic.com>
1 parent 675a215 commit e150b35

3 files changed

Lines changed: 213 additions & 0 deletions

File tree

‎proofs/agda/All.agda‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -157,6 +157,7 @@ open import Ordinal.Buchholz.RankDoubledLadderMono
157157
open import Ordinal.Buchholz.RankDoubledLadderMonoPlus
158158
open import Ordinal.Buchholz.RankDoubledLadderAddPrincipal
159159
open import Ordinal.Buchholz.RankDoubledLadderMonoPlus2
160+
open import Ordinal.Buchholz.RankDoubledLadderUmbrella
160161
open import Ordinal.Buchholz.RankMonoUmbrella
161162
open import Ordinal.Buchholz.RankMonoUmbrellaSlice3
162163
open import Ordinal.Buchholz.RankMonoUmbrellaSlice4

‎proofs/agda/Ordinal/Buchholz/RankDoubledLadderUmbrella.agda‎

Lines changed: 202 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,202 @@
1+
{-# OPTIONS --safe --without-K #-}
2+
-- SPDX-License-Identifier: MPL-2.0
3+
-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
4+
5+
-- The doubled-ladder umbrella `rank2-mono` + well-foundedness `wf-<ᵇ²`
6+
-- (2026-06-14) — the Gate 1 capstone.
7+
--
8+
-- ## What this lands
9+
--
10+
-- A *rank2-soundness-ready* relation `_<ᵇ²_` mirroring ALL 12
11+
-- constructors of the core `Ordinal.Buchholz.Order._<ᵇ_`, with the
12+
-- rank2-soundness side conditions baked into the constructors (the
13+
-- WfAdm witnesses for the ψ-source atomic cases, the leading-power
14+
-- admissibility bound for `<ᵇ-+ψ`, and the WfCNF tail bounds `y ≤ᵇ² x`
15+
-- for the source-bplus cases). On this self-contained relation:
16+
--
17+
-- * `rank2-mono-<ᵇ² : s <ᵇ² t → rank2 s <′ rank2 t` — THE UMBRELLA
18+
-- * `wf-<ᵇ² : WellFounded _<ᵇ²_` — well-foundedness
19+
--
20+
-- Unlike the single-ladder `RankMonoUmbrella._<ᵇ⁰_` (which closes only
21+
-- 10 of 13 constructors — `<ᵇ-0-+`, `<ᵇ-ψΩ≤`, and the bplus-target
22+
-- `<ᵇ-+1` were structurally blocked), the doubled ladder closes ALL
23+
-- 12 core constructors, because each has a landed `rank2`-mono
24+
-- primitive:
25+
--
26+
-- * atomic boundary — RankDoubledLadderMono (ΩΩ Ωψ ψΩ ψΩ≤)
27+
-- * bzero + via-left — RankDoubledLadderMonoPlus (0-Ω 0-ψ 0-+ Ω+ ψ+)
28+
-- * bplus-on-left — RankDoubledLadderAddPrincipal (+Ω)
29+
-- + RankDoubledLadderMonoPlus2 (+ψ +1)
30+
--
31+
-- ## The `<ᵇ-+ψ` leading-power bridge
32+
--
33+
-- `rank2-mono-+ψ` needs the source pieces below the ψ-block's LEADING
34+
-- power `ω-rank-pow (double ν)` — strictly stronger than "below the
35+
-- whole ψ-rank". Plain recursion only gives the weaker bound, so the
36+
-- `<ᵇ²-+ψ` constructor carries `WfAdm x` + `rank-pow x <′ ω-rank-pow ν`
37+
-- and the umbrella derives the leading-power bound through the
38+
-- scale-transfer bridge `rank2-bounded`. The tail bound on `y` rides
39+
-- the WfCNF order `y ≤ᵇ² x` through `rank2-mono-≤ᵇ²` + `≤′-<′-trans`.
40+
--
41+
-- ## Well-foundedness recipe (mechanical, zero new obligations)
42+
--
43+
-- wf-<ᵇ² = Subrelation.wellFounded rank2-mono-<ᵇ²
44+
-- (On.wellFounded rank2 wf-<′)
45+
--
46+
-- — the same rank-embedding transport as `RankMonoUnionWF.wf-<ᵇᵘ`,
47+
-- routed through `rank2` instead of `rank-pow`.
48+
--
49+
-- ## Headlines (pin in `Ordinal/Buchholz/Smoke.agda`)
50+
--
51+
-- * `_<ᵇ²_` -- the rank2-ready relation
52+
-- * `rank2-mono-<ᵇ²` -- THE UMBRELLA (strict)
53+
-- * `rank2-mono-≤ᵇ²` -- non-strict companion
54+
-- * `wf-<ᵇ²` -- well-foundedness via rank2 embedding
55+
56+
module Ordinal.Buchholz.RankDoubledLadderUmbrella where
57+
58+
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
59+
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
60+
open import Induction.WellFounded using (WellFounded; module Subrelation)
61+
open import Relation.Binary.Construct.On as On using (wellFounded)
62+
63+
open import Ordinal.OmegaMarkers using (_<Ω_; _≤Ω_)
64+
open import Ordinal.Buchholz.Syntax using (BT; bzero; bOmega; bpsi; bplus)
65+
open import Ordinal.Brouwer using (Ord; osuc)
66+
open import Ordinal.Brouwer.Phase13 using
67+
( _≤′_
68+
; _<′_
69+
; ≤′-refl
70+
; ≤′-trans
71+
; ≤′-self-osuc
72+
; wf-<′
73+
)
74+
open import Ordinal.Buchholz.RankPow using (rank-pow; ω-rank-pow)
75+
open import Ordinal.Buchholz.WellFormedAdmissible using (WfAdm)
76+
open import Ordinal.Buchholz.RankDoubledLadder using
77+
( rank2
78+
; double
79+
; rank2-bounded
80+
; ≤′-<′-trans
81+
)
82+
open import Ordinal.Buchholz.RankDoubledLadderMono using
83+
( <′-≤′-trans
84+
; rank2-mono-ΩΩ
85+
; rank2-mono-Ωψ
86+
; rank2-mono-ψΩ
87+
; rank2-mono-ψΩ≤
88+
)
89+
open import Ordinal.Buchholz.RankDoubledLadderMonoPlus using
90+
( rank2-pos-bOmega
91+
; rank2-pos-bpsi
92+
; rank2-mono-0-+
93+
; rank2-mono-Ω+
94+
; rank2-mono-ψ+
95+
)
96+
open import Ordinal.Buchholz.RankDoubledLadderAddPrincipal using (rank2-mono-+Ω)
97+
open import Ordinal.Buchholz.RankDoubledLadderMonoPlus2 using (rank2-mono-+ψ; rank2-mono-+1)
98+
99+
----------------------------------------------------------------------
100+
-- The rank2-soundness-ready relation `_<ᵇ²_`
101+
----------------------------------------------------------------------
102+
103+
mutual
104+
105+
data _<ᵇ²_ : BT → BT → Set where
106+
-- bzero-source (positivity; 0-+ carries a positivity sub-derivation)
107+
<ᵇ²-0-Ω : ∀ {μ} → bzero <ᵇ² bOmega μ
108+
<ᵇ²-0-ψ : ∀ {ν α} → bzero <ᵇ² bpsi ν α
109+
<ᵇ²-0-+ : ∀ {x y} → bzero <ᵇ² x → bzero <ᵇ² bplus x y
110+
111+
-- atomic vs atomic (ψ-source cases carry their WfAdm witness)
112+
<ᵇ²-ΩΩ : ∀ {μ ν} → μ <Ω ν → bOmega μ <ᵇ² bOmega ν
113+
<ᵇ²-Ωψ : ∀ {μ ν α} → μ <Ω ν → bOmega μ <ᵇ² bpsi ν α
114+
<ᵇ²-ψΩ : ∀ {μ ν α β} → WfAdm (bpsi μ α) → μ <Ω ν → bpsi μ α <ᵇ² bpsi ν β
115+
<ᵇ²-ψΩ≤ : ∀ {ν μ α} → WfAdm (bpsi ν α) → ν ≤Ω μ → bpsi ν α <ᵇ² bOmega μ
116+
117+
-- via-left (recurse on the sub-derivation)
118+
<ᵇ²-Ω+ : ∀ {μ x y} → bOmega μ <ᵇ² x → bOmega μ <ᵇ² bplus x y
119+
<ᵇ²-ψ+ : ∀ {ν α x y} → bpsi ν α <ᵇ² x → bpsi ν α <ᵇ² bplus x y
120+
121+
-- source-bplus (premise on left summand + tail bound on source)
122+
<ᵇ²-+Ω : ∀ {x y μ}
123+
→ x <ᵇ² bOmega μ
124+
→ y ≤ᵇ² x
125+
→ bplus x y <ᵇ² bOmega μ
126+
-- +ψ carries the leading-power admissibility bridge for x
127+
<ᵇ²-+ψ : ∀ {x y ν α}
128+
→ WfAdm x
129+
→ rank-pow x <′ ω-rank-pow ν
130+
→ y ≤ᵇ² x
131+
→ bplus x y <ᵇ² bpsi ν α
132+
133+
-- joint-bplus (whole source below target head)
134+
<ᵇ²-+1 : ∀ {x₁ x₂ y₁ y₂}
135+
→ bplus x₁ x₂ <ᵇ² y₁
136+
→ bplus x₁ x₂ <ᵇ² bplus y₁ y₂
137+
138+
_≤ᵇ²_ : BT → BT → Set
139+
x ≤ᵇ² y = (x <ᵇ² y) ⊎ (x ≡ y)
140+
141+
infix 4 _<ᵇ²_ _≤ᵇ²_
142+
143+
≤ᵇ²-refl : ∀ {x} → x ≤ᵇ² x
144+
≤ᵇ²-refl = inj₂ refl
145+
146+
----------------------------------------------------------------------
147+
-- The umbrella theorem
148+
----------------------------------------------------------------------
149+
150+
mutual
151+
152+
rank2-mono-<ᵇ² : ∀ {s t} → s <ᵇ² t → rank2 s <′ rank2 t
153+
rank2-mono-<ᵇ² (<ᵇ²-0-Ω {μ}) = rank2-pos-bOmega μ
154+
rank2-mono-<ᵇ² (<ᵇ²-0-ψ {ν} {α}) = rank2-pos-bpsi ν α
155+
rank2-mono-<ᵇ² (<ᵇ²-0-+ {x} {y} p) =
156+
rank2-mono-0-+ {x} {y} (rank2-mono-<ᵇ² p)
157+
rank2-mono-<ᵇ² (<ᵇ²-ΩΩ {μ} {ν} p) = rank2-mono-ΩΩ {μ} {ν} p
158+
rank2-mono-<ᵇ² (<ᵇ²-Ωψ {μ} {ν} {α} p) = rank2-mono-Ωψ {μ} {ν} {α} p
159+
rank2-mono-<ᵇ² (<ᵇ²-ψΩ {μ} {ν} {α} {β} wf p) =
160+
rank2-mono-ψΩ {μ} {ν} {α} {β} wf p
161+
rank2-mono-<ᵇ² (<ᵇ²-ψΩ≤ {ν} {μ} {α} wf p) =
162+
rank2-mono-ψΩ≤ {ν} {μ} {α} wf p
163+
rank2-mono-<ᵇ² (<ᵇ²-Ω+ {μ} {x} {y} p) =
164+
rank2-mono-Ω+ {μ} {x} {y} (rank2-mono-<ᵇ² p)
165+
rank2-mono-<ᵇ² (<ᵇ²-ψ+ {ν} {α} {x} {y} p) =
166+
rank2-mono-ψ+ {ν} {α} {x} {y} (rank2-mono-<ᵇ² p)
167+
rank2-mono-<ᵇ² (<ᵇ²-+Ω {x} {y} {μ} p y≤x) =
168+
rank2-mono-+Ω {x} {y} {μ}
169+
(rank2-mono-<ᵇ² p)
170+
(≤′-<′-trans {rank2 y} {rank2 x} {rank2 (bOmega μ)}
171+
(rank2-mono-≤ᵇ² y≤x)
172+
(rank2-mono-<ᵇ² p))
173+
rank2-mono-<ᵇ² (<ᵇ²-+ψ {x} {y} {ν} {α} wfx rpx y≤x) =
174+
rank2-mono-+ψ {x} {y} {ν} {α}
175+
(rank2-bounded {x} {ν} wfx rpx)
176+
(≤′-<′-trans {rank2 y} {rank2 x} {ω-rank-pow (double ν)}
177+
(rank2-mono-≤ᵇ² y≤x)
178+
(rank2-bounded {x} {ν} wfx rpx))
179+
rank2-mono-<ᵇ² (<ᵇ²-+1 {x₁} {x₂} {y₁} {y₂} p) =
180+
rank2-mono-+1 {x₁} {x₂} {y₁} {y₂} (rank2-mono-<ᵇ² p)
181+
182+
rank2-mono-≤ᵇ² : ∀ {x y} → x ≤ᵇ² y → rank2 x ≤′ rank2 y
183+
rank2-mono-≤ᵇ² {x} {y} (inj₁ p) =
184+
≤′-trans {rank2 x} {osuc (rank2 x)} {rank2 y}
185+
(≤′-self-osuc (rank2 x))
186+
(rank2-mono-<ᵇ² p)
187+
rank2-mono-≤ᵇ² {x} {.x} (inj₂ refl) = ≤′-refl {rank2 x}
188+
189+
----------------------------------------------------------------------
190+
-- Well-foundedness of `_<ᵇ²_` via the rank2 embedding
191+
----------------------------------------------------------------------
192+
193+
-- Step 1 — InverseImage transport: `_<′_` well-founded on `Ord`
194+
-- lifts to the pullback `_<′_ on rank2` on `BT`.
195+
wf-rank2-pullback : WellFounded (λ x y → rank2 x <′ rank2 y)
196+
wf-rank2-pullback = On.wellFounded rank2 wf-<′
197+
198+
-- Step 2 — Subrelation transport: `rank2-mono-<ᵇ²` witnesses that
199+
-- `_<ᵇ²_` is a sub-relation of the pullback, so it inherits
200+
-- well-foundedness.
201+
wf-<ᵇ² : WellFounded _<ᵇ²_
202+
wf-<ᵇ² = Subrelation.wellFounded rank2-mono-<ᵇ² wf-rank2-pullback

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

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -511,6 +511,16 @@ open import Ordinal.Buchholz.RankDoubledLadderMonoPlus2 using
511511
; rank2-mono-+1
512512
)
513513

514+
-- Doubled-ladder umbrella + well-foundedness (own block per CLAUDE.md
515+
-- Working rules) — the Gate 1 capstone: a complete rank2-ready
516+
-- relation over all 12 core `_<ᵇ_` constructors and its WF proof.
517+
open import Ordinal.Buchholz.RankDoubledLadderUmbrella using
518+
( _<ᵇ²_
519+
; rank2-mono-<ᵇ²
520+
; rank2-mono-≤ᵇ²
521+
; wf-<ᵇ²
522+
)
523+
514524
-- Slice 3 prerequisites (own block per CLAUDE.md Working rules):
515525
-- the left-spine NonBzero predicate, the strict-jump bridge from
516526
-- `μ <Ω ν` to `ω-rank-pow-succ μ ≤′ ω-rank-pow ν`, and the head-Ω

0 commit comments

Comments
 (0)