|
| 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 monotonicity — atomic-boundary slice (2026-06-14). |
| 6 | +-- |
| 7 | +-- ## Why this exists |
| 8 | +-- |
| 9 | +-- `RankDoubledLadder` landed the doubled-ladder rank `rank2 : BT → Ord` |
| 10 | +-- together with the arithmetic spine that the single ω-power ladder |
| 11 | +-- could not provide: |
| 12 | +-- |
| 13 | +-- * `rank2-bpsi-below-bOmega` — the equal-Ω room fact; |
| 14 | +-- * `double-cross-gap` — the STRICT cross-index gap |
| 15 | +-- `Ω_ν < ψ_{ν'}(…)` for `ν <Ω ν'`; |
| 16 | +-- * `ω-rank-pow-reflects-<Ω` — the bOmega-case inversion; |
| 17 | +-- * `rank2-bounded` — the WfAdm→rank2 admissibility transfer. |
| 18 | +-- |
| 19 | +-- This slice consumes that spine to discharge the per-constructor |
| 20 | +-- `rank2`-monotonicity primitives for the four ATOMIC-vs-ATOMIC |
| 21 | +-- comparisons of the core `_<ᵇ_` (`Ordinal.Buchholz.Order`): |
| 22 | +-- |
| 23 | +-- * `<ᵇ-ΩΩ : μ <Ω ν → bOmega μ <ᵇ bOmega ν` |
| 24 | +-- * `<ᵇ-Ωψ : μ <Ω ν → bOmega μ <ᵇ bpsi ν α` |
| 25 | +-- * `<ᵇ-ψΩ : μ <Ω ν → bpsi μ α <ᵇ bpsi ν β` |
| 26 | +-- * `<ᵇ-ψΩ≤ : ν ≤Ω μ → bpsi ν α <ᵇ bOmega μ` |
| 27 | +-- |
| 28 | +-- These are exactly the constructors the doubled ladder was BUILT to |
| 29 | +-- enable: the single-ladder `rank-pow` collapses ψ_ν/Ω_ν to the same |
| 30 | +-- block (so it cannot order `<ᵇ-ψΩ≤`), and `rank-adm` ranks ψ ABOVE Ω |
| 31 | +-- (so it inverts `<ᵇ-Ωψ`). The doubled ladder orders all four with |
| 32 | +-- strict room. |
| 33 | +-- |
| 34 | +-- Each primitive is stated relation-agnostically (premise = the |
| 35 | +-- constructor's index data + the LHS `WfAdm` witness where an |
| 36 | +-- admissibility bound is needed), so a `_<ᵇ_` consumer pattern-matches |
| 37 | +-- on its own constructor and applies the matching primitive — the same |
| 38 | +-- discipline as RankPow's `rank-mono-<ᵇ-*` family. |
| 39 | +-- |
| 40 | +-- ## Honest scope |
| 41 | +-- |
| 42 | +-- This slice covers the four atomic-boundary constructors only. NOT |
| 43 | +-- yet landed (documented follow-on): |
| 44 | +-- * the bzero-source positivity cases (`<ᵇ-0-Ω/0-ψ/0-+`); |
| 45 | +-- * the five bplus-recursive cases (`<ᵇ-Ω+/ψ+/+Ω/+ψ/+1`), which |
| 46 | +-- recurse on the `<ᵇ` sub-derivation and combine via `⊕`-mono; |
| 47 | +-- * the full `rank2-mono : WfAdm x → WfAdm y → x <ᵇ y → rank2 x <′ |
| 48 | +-- rank2 y` umbrella + the `wf-<′`-transport headline `wf-<ᵇ`. |
| 49 | +-- |
| 50 | +-- ## Headlines (pin in `Ordinal/Buchholz/Smoke.agda`) |
| 51 | +-- |
| 52 | +-- * `rank2-mono-ΩΩ` |
| 53 | +-- * `rank2-mono-Ωψ` |
| 54 | +-- * `rank2-mono-ψΩ` |
| 55 | +-- * `rank2-mono-ψΩ≤` |
| 56 | + |
| 57 | +module Ordinal.Buchholz.RankDoubledLadderMono where |
| 58 | + |
| 59 | +open import Data.Sum.Base using (_⊎_; inj₁; inj₂) |
| 60 | +open import Relation.Binary.PropositionalEquality using (_≡_; refl) |
| 61 | + |
| 62 | +open import Ordinal.Brouwer using (Ord; osuc) |
| 63 | +open import Ordinal.Brouwer.Phase13 using (_≤′_; _<′_; ≤′-trans; ≤′-self-osuc; ⊕-left-≤-sum) |
| 64 | +open import Ordinal.Brouwer.Arithmetic using (_⊕_) |
| 65 | +open import Ordinal.OmegaMarkers using (OmegaIndex; _<Ω_; _≤Ω_; ≤Ω-split) |
| 66 | +open import Ordinal.Buchholz.Syntax using (BT; bOmega; bpsi) |
| 67 | +open import Ordinal.Buchholz.RankPow using |
| 68 | + ( ω-rank-pow |
| 69 | + ; ω-rank-pow-succ |
| 70 | + ; ω-rank-pow-<-succ |
| 71 | + ) |
| 72 | +open import Ordinal.Buchholz.RankDoubledLadder using |
| 73 | + ( rank2 |
| 74 | + ; double |
| 75 | + ; double-cross-gap |
| 76 | + ; rank2-bpsi-below-bOmega |
| 77 | + ; rank2-bounded |
| 78 | + ) |
| 79 | +open import Ordinal.Buchholz.WellFormedAdmissible using (WfAdm; wf-adm-bpsi) |
| 80 | + |
| 81 | +---------------------------------------------------------------------- |
| 82 | +-- Local strict / mixed transitivity (Phase13 exports only ≤′-trans) |
| 83 | +---------------------------------------------------------------------- |
| 84 | + |
| 85 | +-- `α <′ β` is `osuc α ≤′ β`; chain through `β ≤′ osuc β`. |
| 86 | +<′-trans : ∀ {α β γ} → α <′ β → β <′ γ → α <′ γ |
| 87 | +<′-trans {α} {β} {γ} p q = |
| 88 | + ≤′-trans {osuc α} {β} {γ} p |
| 89 | + (≤′-trans {β} {osuc β} {γ} (≤′-self-osuc β) q) |
| 90 | + |
| 91 | +-- Mixed `<′ ⨾ ≤′`. `α <′ β` is `osuc α ≤′ β`, so this is `≤′-trans`. |
| 92 | +<′-≤′-trans : ∀ {α β γ} → α <′ β → β ≤′ γ → α <′ γ |
| 93 | +<′-≤′-trans {α} {β} {γ} p q = ≤′-trans {osuc α} {β} {γ} p q |
| 94 | + |
| 95 | +---------------------------------------------------------------------- |
| 96 | +-- Admissibility extraction |
| 97 | +---------------------------------------------------------------------- |
| 98 | + |
| 99 | +-- From a `WfAdm (bpsi ν α)` witness, recover the rank2-level |
| 100 | +-- admissibility bound `rank2 α <′ ω-rank-pow (double ν)` via the |
| 101 | +-- scale-transfer bridge. This is the single point where the slice |
| 102 | +-- depends on well-formedness — the bound is what keeps a ψ-rank |
| 103 | +-- strictly inside its own doubled exponent block. |
| 104 | +ψ-adm-rank2 : ∀ {ν α} |
| 105 | + → WfAdm (bpsi ν α) |
| 106 | + → rank2 α <′ ω-rank-pow (double ν) |
| 107 | +ψ-adm-rank2 {ν} {α} (wf-adm-bpsi _ wfα admα) = rank2-bounded {α} {ν} wfα admα |
| 108 | + |
| 109 | +---------------------------------------------------------------------- |
| 110 | +-- The four atomic-boundary rank2-mono primitives |
| 111 | +---------------------------------------------------------------------- |
| 112 | + |
| 113 | +-- `<ᵇ-ΩΩ` — Ω_μ < Ω_ν. Ω-block μ is strictly below ψ-block ν |
| 114 | +-- (`double-cross-gap`), which is strictly below Ω-block ν |
| 115 | +-- (`ω-rank-pow-<-succ`). |
| 116 | +rank2-mono-ΩΩ : ∀ {μ ν} |
| 117 | + → μ <Ω ν |
| 118 | + → rank2 (bOmega μ) <′ rank2 (bOmega ν) |
| 119 | +rank2-mono-ΩΩ {μ} {ν} μ<ν = |
| 120 | + <′-trans {ω-rank-pow-succ (double μ)} {ω-rank-pow (double ν)} {ω-rank-pow-succ (double ν)} |
| 121 | + (double-cross-gap μ<ν) |
| 122 | + (ω-rank-pow-<-succ (double ν)) |
| 123 | + |
| 124 | +-- `<ᵇ-Ωψ` — Ω_μ < ψ_ν(α) for μ <Ω ν. Ω-block μ is strictly below |
| 125 | +-- ψ-block ν (`double-cross-gap`), which is `≤′` the ψ-rank |
| 126 | +-- `ω-rank-pow (double ν) ⊕ rank2 α` (`⊕-left-≤-sum`). No |
| 127 | +-- admissibility needed — the ψ-argument only adds. |
| 128 | +rank2-mono-Ωψ : ∀ {μ ν α} |
| 129 | + → μ <Ω ν |
| 130 | + → rank2 (bOmega μ) <′ rank2 (bpsi ν α) |
| 131 | +rank2-mono-Ωψ {μ} {ν} {α} μ<ν = |
| 132 | + <′-≤′-trans {ω-rank-pow-succ (double μ)} {ω-rank-pow (double ν)} |
| 133 | + {ω-rank-pow (double ν) ⊕ rank2 α} |
| 134 | + (double-cross-gap μ<ν) |
| 135 | + (⊕-left-≤-sum {ω-rank-pow (double ν)} (rank2 α)) |
| 136 | + |
| 137 | +-- `<ᵇ-ψΩ` — ψ_μ(α) < ψ_ν(β) for μ <Ω ν. Under admissibility the |
| 138 | +-- whole ψ_μ(α) rank sits below Ω-block μ (`rank2-bpsi-below-bOmega`), |
| 139 | +-- which is below ψ-block ν (`double-cross-gap`), which is `≤′` the |
| 140 | +-- target ψ-rank (`⊕-left-≤-sum`). |
| 141 | +rank2-mono-ψΩ : ∀ {μ ν α β} |
| 142 | + → WfAdm (bpsi μ α) |
| 143 | + → μ <Ω ν |
| 144 | + → rank2 (bpsi μ α) <′ rank2 (bpsi ν β) |
| 145 | +rank2-mono-ψΩ {μ} {ν} {α} {β} wfμα μ<ν = |
| 146 | + <′-≤′-trans {rank2 (bpsi μ α)} {ω-rank-pow (double ν)} |
| 147 | + {ω-rank-pow (double ν) ⊕ rank2 β} |
| 148 | + (<′-trans {rank2 (bpsi μ α)} {ω-rank-pow-succ (double μ)} {ω-rank-pow (double ν)} |
| 149 | + (rank2-bpsi-below-bOmega {μ} {α} (ψ-adm-rank2 {μ} {α} wfμα)) |
| 150 | + (double-cross-gap μ<ν)) |
| 151 | + (⊕-left-≤-sum {ω-rank-pow (double ν)} (rank2 β)) |
| 152 | + |
| 153 | +-- `<ᵇ-ψΩ≤` — ψ_ν(α) < Ω_μ for ν ≤Ω μ. THE equal-Ω boundary the |
| 154 | +-- single ladder could not order. Split `ν ≤Ω μ`: |
| 155 | +-- * ν ≡ μ — the room fact `rank2-bpsi-below-bOmega` lands the goal |
| 156 | +-- directly (`ω-rank-pow-succ (double ν) = rank2 (bOmega μ)`); |
| 157 | +-- * ν <Ω μ — ψ_ν(α) below Ω-block ν, below ψ-block μ |
| 158 | +-- (`double-cross-gap`), below Ω-block μ (`ω-rank-pow-<-succ`). |
| 159 | +rank2-mono-ψΩ≤ : ∀ {ν μ α} |
| 160 | + → WfAdm (bpsi ν α) |
| 161 | + → ν ≤Ω μ |
| 162 | + → rank2 (bpsi ν α) <′ rank2 (bOmega μ) |
| 163 | +rank2-mono-ψΩ≤ {ν} {μ} {α} wfνα ν≤μ with ≤Ω-split ν≤μ |
| 164 | +... | inj₂ refl = |
| 165 | + rank2-bpsi-below-bOmega {ν} {α} (ψ-adm-rank2 {ν} {α} wfνα) |
| 166 | +... | inj₁ ν<μ = |
| 167 | + <′-trans {rank2 (bpsi ν α)} {ω-rank-pow-succ (double ν)} {rank2 (bOmega μ)} |
| 168 | + (rank2-bpsi-below-bOmega {ν} {α} (ψ-adm-rank2 {ν} {α} wfνα)) |
| 169 | + (<′-trans {ω-rank-pow-succ (double ν)} {ω-rank-pow (double μ)} {ω-rank-pow-succ (double μ)} |
| 170 | + (double-cross-gap ν<μ) |
| 171 | + (ω-rank-pow-<-succ (double μ))) |
0 commit comments