|
| 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 |
0 commit comments