|
| 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 | +-- Doubled-ladder rank foundation — Slice 1 (2026-06-13). |
| 6 | +-- |
| 7 | +-- ## Why this exists |
| 8 | +-- |
| 9 | +-- Gate 1's residual is the EQUAL-Ω boundary `bpsi ν α <ᵇ bOmega ν` |
| 10 | +-- (ψ_ν(α) < Ω_ν at the SAME leading marker ν). The session that |
| 11 | +-- isolated it (`RankPowSlice3Headline` + `head-Ω-strict-or-eq`) |
| 12 | +-- and proved the local "room" fact (`RankPowDomination. |
| 13 | +-- ω-rank-pow-⊕-below-succ`) also recorded the obstruction to a |
| 14 | +-- GLOBAL rank: naively placing `Ω_ν` at `ω-rank-pow-succ ν` |
| 15 | +-- (= ω^(ν+2)) breaks the cross-index constructor |
| 16 | +-- `<ᵇ-Ωψ` (`bOmega μ <ᵇ bpsi (suc μ) bzero`), because at ν = suc μ |
| 17 | +-- the source bound ω^(μ+2) MEETS the target ω^((suc μ)+1) = ω^(μ+2) |
| 18 | +-- and the strict gap collapses. |
| 19 | +-- |
| 20 | +-- ## The fix: double the index |
| 21 | +-- |
| 22 | +-- Give ψ and Ω their OWN interleaved exponent blocks by mapping |
| 23 | +-- level ν to TWO ω-power blocks instead of one: |
| 24 | +-- |
| 25 | +-- ψexp ν = 2ν+1 (ψ_ν(α) ranks in the ω^(2ν+1) block) |
| 26 | +-- Ωexp ν = 2ν+2 (Ω_ν ranks at ω^(2ν+2), one block above) |
| 27 | +-- |
| 28 | +-- The intended atomic order |
| 29 | +-- |
| 30 | +-- … < ψ_ν(α) < Ω_ν < ψ_{ν+1}(β) < Ω_{ν+1} < … |
| 31 | +-- |
| 32 | +-- then embeds with STRICT room everywhere, because consecutive |
| 33 | +-- levels are now two exponent-blocks apart: |
| 34 | +-- |
| 35 | +-- * `Ωexp ν = suc (ψexp ν)` — Ω_ν is exactly one block |
| 36 | +-- above the ψ_ν block; |
| 37 | +-- * `Ωexp μ < ψexp (suc μ)` — and Ω_μ is strictly below |
| 38 | +-- the NEXT level's ψ block |
| 39 | +-- (2μ+2 < 2(μ+1)+1 = 2μ+3), |
| 40 | +-- which is exactly the |
| 41 | +-- cross-index gap the single |
| 42 | +-- ladder could not provide. |
| 43 | +-- |
| 44 | +-- ## What this slice lands (the two interleaving facts) |
| 45 | +-- |
| 46 | +-- * `ψ-block-below-Ω-block` — the doubled-ladder room fact: |
| 47 | +-- an admissibility-bounded ψ-rank `ω^(2ν+1) ⊕ β` (with |
| 48 | +-- `β <′ ω^(2ν+1)`) is strictly below `ω^(2ν+2)`. (Same shape |
| 49 | +-- as `ω-rank-pow-⊕-below-succ`, re-expressed on the doubled |
| 50 | +-- exponents so it composes with the cross-index fact below.) |
| 51 | +-- * `Ω-block-below-next-ψ` — the cross-index gap: `ω^(2μ+2) <′ |
| 52 | +-- ω^(2ν+1)` whenever `μ < n`. This is the fact the single |
| 53 | +-- ladder lacked; the doubling buys it as plain `ω^`-strict-mono |
| 54 | +-- on `Ωexp μ < ψexp ν`. |
| 55 | +-- |
| 56 | +-- Together these are the arithmetic spine of the doubled-ladder |
| 57 | +-- rank `rank2 : BT → Ord` (ψ_ν → ω^(2ν+1) ⊕ …, Ω_ν → ω^(2ν+2), |
| 58 | +-- bplus → ⊕), whose per-constructor monotonicity + WF transport are |
| 59 | +-- the follow-on slices. |
| 60 | +-- |
| 61 | +-- ## Honest scope |
| 62 | +-- |
| 63 | +-- Slice 1 is the fin-index arithmetic foundation only. NOT yet |
| 64 | +-- landed: the `rank2` function itself; the OmegaIndex ω (limit) |
| 65 | +-- cases; the per-constructor rank-mono re-proof against `rank2`; |
| 66 | +-- the `wf-<′`-transport. This module proves the doubled ladder |
| 67 | +-- RESOLVES the documented cross-index obstruction at the fin level — |
| 68 | +-- the design is sound; the build-out is mechanical follow-on. |
| 69 | +-- |
| 70 | +-- ## Headlines (pin in `Ordinal/Buchholz/Smoke.agda`) |
| 71 | +-- |
| 72 | +-- * `ψ-block-below-Ω-block` |
| 73 | +-- * `Ω-block-below-next-ψ` |
| 74 | + |
| 75 | +module Ordinal.Buchholz.RankDoubledLadder where |
| 76 | + |
| 77 | +open import Data.Nat using (ℕ; suc; _+_; _<_; _≤_; s≤s) |
| 78 | +open import Data.Nat.Properties using (+-suc; +-mono-≤) |
| 79 | +open import Relation.Binary.PropositionalEquality using (_≡_; subst; cong) |
| 80 | + |
| 81 | +open import Ordinal.Brouwer using (Ord; osuc) |
| 82 | +open import Ordinal.Brouwer.Phase13 using |
| 83 | + ( _≤′_ |
| 84 | + ; _<′_ |
| 85 | + ; ≤′-trans |
| 86 | + ; ≤′-self-osuc |
| 87 | + ) |
| 88 | +open import Ordinal.Brouwer.Arithmetic using (_⊕_) |
| 89 | +open import Ordinal.Brouwer.OmegaPow using |
| 90 | + ( ω^_ |
| 91 | + ; ω^-strict-mono |
| 92 | + ; ω^-strict-mono-suc |
| 93 | + ; additive-principal |
| 94 | + ) |
| 95 | + |
| 96 | +---------------------------------------------------------------------- |
| 97 | +-- Local strict transitivity (Phase13 exports only ≤′-trans) |
| 98 | +---------------------------------------------------------------------- |
| 99 | + |
| 100 | +-- `α <′ β` is `osuc α ≤′ β`; chain through `β ≤′ osuc β`. |
| 101 | +<′-trans : ∀ {α β γ} → α <′ β → β <′ γ → α <′ γ |
| 102 | +<′-trans {α} {β} {γ} p q = |
| 103 | + ≤′-trans {osuc α} {β} {γ} p |
| 104 | + (≤′-trans {β} {osuc β} {γ} (≤′-self-osuc β) q) |
| 105 | + |
| 106 | +---------------------------------------------------------------------- |
| 107 | +-- The doubled-index exponent blocks |
| 108 | +---------------------------------------------------------------------- |
| 109 | + |
| 110 | +-- ψ-block exponent for level n: 2n+1. |
| 111 | +ψexp : ℕ → ℕ |
| 112 | +ψexp n = suc (n + n) |
| 113 | + |
| 114 | +-- Ω-block exponent for level n: 2n+2 = suc (ψexp n). |
| 115 | +Ωexp : ℕ → ℕ |
| 116 | +Ωexp n = suc (suc (n + n)) |
| 117 | + |
| 118 | +---------------------------------------------------------------------- |
| 119 | +-- Fact 1 — ψ-block sits below Ω-block at the SAME level |
| 120 | +---------------------------------------------------------------------- |
| 121 | + |
| 122 | +-- The doubled-ladder room fact. Under admissibility (`β <′ ω^(2ν+1)`), |
| 123 | +-- the ψ-rank `ω^(2ν+1) ⊕ β` is strictly below `ω^(2ν+2)`. Both |
| 124 | +-- summands are `< ω^(suc (ψexp n)) = ω^(Ωexp n)` (left by one-step |
| 125 | +-- strict-mono, right by admissibility + that step), and the target is |
| 126 | +-- additive principal, so the sum stays below. |
| 127 | +ψ-block-below-Ω-block : ∀ {n β} |
| 128 | + → β <′ ω^ (ψexp n) |
| 129 | + → (ω^ (ψexp n) ⊕ β) <′ ω^ (Ωexp n) |
| 130 | +ψ-block-below-Ω-block {n} {β} β<ψ = |
| 131 | + additive-principal {ψexp n} {ω^ (ψexp n)} {β} |
| 132 | + (ω^-strict-mono-suc (ψexp n)) |
| 133 | + (<′-trans {β} {ω^ (ψexp n)} {ω^ (suc (ψexp n))} |
| 134 | + β<ψ |
| 135 | + (ω^-strict-mono-suc (ψexp n))) |
| 136 | + |
| 137 | +---------------------------------------------------------------------- |
| 138 | +-- Fact 2 — Ω-block sits below the NEXT level's ψ-block (cross-index) |
| 139 | +---------------------------------------------------------------------- |
| 140 | + |
| 141 | +-- The fact the single ω-power ladder lacked. For `m < n`, |
| 142 | +-- `Ωexp m = 2m+2 < 2n+1 = ψexp n` (because `m < n` gives |
| 143 | +-- `m+1 ≤ n`, hence `(m+1)+(m+1) ≤ n+n`, i.e. `2m+2 ≤ 2n < 2n+1`). |
| 144 | +-- So `ω^(2m+2) <′ ω^(2n+1)` by plain `ω^`-strict-mono — the strict |
| 145 | +-- gap survives even at the boundary `n = suc m` that defeated the |
| 146 | +-- single ladder. |
| 147 | +Ω-block-below-next-ψ : ∀ {m n} |
| 148 | + → m < n |
| 149 | + → ω^ (Ωexp m) <′ ω^ (ψexp n) |
| 150 | +Ω-block-below-next-ψ {m} {n} m<n = ω^-strict-mono Ωexp-m<ψexp-n |
| 151 | + where |
| 152 | + -- suc m + suc m ≡ suc (suc (m + m)) (def on the left + +-suc) |
| 153 | + +-shift : suc m + suc m ≡ suc (suc (m + m)) |
| 154 | + +-shift = cong suc (+-suc m m) |
| 155 | + |
| 156 | + -- 2m+2 ≤ n+n from (m+1)+(m+1) ≤ n+n |
| 157 | + Ωexp-m≤n+n : suc (suc (m + m)) ≤ n + n |
| 158 | + Ωexp-m≤n+n = subst (_≤ n + n) +-shift (+-mono-≤ m<n m<n) |
| 159 | + |
| 160 | + -- 2m+2 < 2n+1 |
| 161 | + Ωexp-m<ψexp-n : Ωexp m < ψexp n |
| 162 | + Ωexp-m<ψexp-n = s≤s Ωexp-m≤n+n |
0 commit comments