|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | + |
| 3 | +-- Lex-pair rank for Buchholz terms (Lane 3 follow-on slice, 2026-05-27). |
| 4 | +-- |
| 5 | +-- ## Where this sits |
| 6 | +-- |
| 7 | +-- `Ordinal.Buchholz.RankAdm.rank-adm` discharged the `<ᵇ⁺-ψα` |
| 8 | +-- (shared-Ω-index lex) constructor by shifting the ψ-rank from |
| 9 | +-- `ω-rank-pow ν` (α-blind) to `ω-rank-pow ν ⊕ rank-pow α` |
| 10 | +-- (α-discriminating). That fixed `<ᵇ⁺-ψα` cleanly, but it surfaced |
| 11 | +-- a new gap: the `<ᵇ-ψΩ≤` constructor at the ν = μ boundary case is |
| 12 | +-- *structurally impossible* under any scalar `Ord`-valued rank with |
| 13 | +-- `ω-rank-pow ν ≤ rank-adm (bpsi ν α)` — that monotonicity forces |
| 14 | +-- the goal `rank-adm (bpsi ν α) <′ ω-rank-pow ν` to imply the absurd |
| 15 | +-- `ω-rank-pow ν <′ ω-rank-pow ν` (see `RankAdm.agda` |
| 16 | +-- §"<ᵇ-ψΩ≤-still-open" for the full diagnostic). |
| 17 | +-- |
| 18 | +-- The recommended follow-up there was option (A): a two-component |
| 19 | +-- lex rank. This module lands it as a *thin* slice: the lex pair |
| 20 | +-- exists alongside `rank-pow` and `rank-adm`, only for the headline |
| 21 | +-- `<ᵇ-ψΩ≤` close-out. The existing 10 + 1 = 11 closed cases |
| 22 | +-- continue to consume the scalar `rank-pow` / `rank-adm` infrastructure |
| 23 | +-- unchanged. |
| 24 | +-- |
| 25 | +-- ## What this slice closes |
| 26 | +-- |
| 27 | +-- 1. `RankLex` record with two `Ord` fields (`first`, `second`). |
| 28 | +-- 2. `_<lex_` strict order: lex on first, fall through to second on |
| 29 | +-- *syntactic* first-component equality (the second-strict |
| 30 | +-- constructor pattern-matches the same implicit `a` on both |
| 31 | +-- sides, so equality is by unification, not propositional). |
| 32 | +-- 3. `rank-lex : BT → RankLex`: |
| 33 | +-- bzero ↦ mkLex oz oz |
| 34 | +-- bOmega ν ↦ mkLex (ω-rank-pow ν) (ω-rank-pow ν) |
| 35 | +-- bpsi ν α ↦ mkLex (ω-rank-pow ν) (rank-pow α) |
| 36 | +-- bplus x y ↦ mkLex (rank-pow (bplus x y)) oz |
| 37 | +-- The `bOmega ν` second-component placeholder is `ω-rank-pow ν` |
| 38 | +-- itself — large enough to dominate any admissible `rank-pow α` |
| 39 | +-- bound by `<′ ω-rank-pow ν`. |
| 40 | +-- 4. `rank-mono-<ᵇ-ψΩ≤-lex` — the headline. Both the ν <Ω μ strict |
| 41 | +-- case (closes via `<lex-first` + `ω-rank-pow-mono`) and the |
| 42 | +-- ν = μ boundary case (closes via `<lex-second` + the |
| 43 | +-- admissibility bound `rank-pow α <′ ω-rank-pow ν`). |
| 44 | +-- |
| 45 | +-- ## What this slice deliberately does NOT close |
| 46 | +-- |
| 47 | +-- * `<ᵇ-+1` joint-bplus. Unchanged from `RankAdm.agda` / `RankPow.agda` |
| 48 | +-- deferral — needs a coarser dominator (leading-Ω-index) or a |
| 49 | +-- richer rank shape on `bplus`. See `RankPow.agda` and |
| 50 | +-- `docs/echo-types/buchholz-rank-obstruction.adoc`. |
| 51 | +-- * Full `rank-lex-mono-<ᵇ⁻` umbrella. The 11 existing constructor |
| 52 | +-- primitives in `RankPow` / `RankAdm` are scalar; lifting them to |
| 53 | +-- the lex form would require re-stating each (per design note A in |
| 54 | +-- `RankAdm.agda`). This slice ships ONLY the headline lex-mono |
| 55 | +-- for the boundary-case constructor; the umbrella will compose |
| 56 | +-- `rank-pow-mono-<ᵇ⁰` (10 cases) + `rank-mono-<ᵇ⁺-ψα-from-pow` |
| 57 | +-- (`<ᵇ⁺-ψα` via `rank-adm`) + this slice's |
| 58 | +-- `rank-mono-<ᵇ-ψΩ≤-lex` (`<ᵇ-ψΩ≤`) under a single dispatch. |
| 59 | +-- Deferred to the consumer-side umbrella refresh. |
| 60 | +-- |
| 61 | +-- ## Headlines (pinned in `Ordinal/Buchholz/Smoke.agda`) |
| 62 | +-- |
| 63 | +-- * `RankLex` / `mkLex` -- the carrier |
| 64 | +-- * `_<lex_` / `<lex-first` / `<lex-second` -- the strict order |
| 65 | +-- * `rank-lex` -- the lex rank |
| 66 | +-- * `rank-lex-bzero`, `rank-lex-bOmega`, |
| 67 | +-- `rank-lex-bplus`, `rank-lex-bpsi` -- definitional sanity |
| 68 | +-- * `rank-mono-<ᵇ-ψΩ≤-lex` -- the slice's headline |
| 69 | + |
| 70 | +module Ordinal.Buchholz.RankLex where |
| 71 | + |
| 72 | +open import Data.Sum.Base using (inj₁; inj₂) |
| 73 | +open import Relation.Binary.PropositionalEquality using (_≡_; refl) |
| 74 | + |
| 75 | +open import Ordinal.OmegaMarkers using |
| 76 | + ( OmegaIndex |
| 77 | + ; _≤Ω_ |
| 78 | + ; _<Ω_ |
| 79 | + ; ≤Ω-split |
| 80 | + ) |
| 81 | +open import Ordinal.Brouwer using (Ord; oz; osuc) |
| 82 | +open import Ordinal.Brouwer.Phase13 using (_<′_; _≤′_) |
| 83 | +open import Ordinal.Buchholz.Syntax using |
| 84 | + ( BT |
| 85 | + ; bzero |
| 86 | + ; bOmega |
| 87 | + ; bplus |
| 88 | + ; bpsi |
| 89 | + ) |
| 90 | +open import Ordinal.Buchholz.RankPow using |
| 91 | + ( rank-pow |
| 92 | + ; ω-rank-pow |
| 93 | + ; ω-rank-pow-mono |
| 94 | + ) |
| 95 | + |
| 96 | +---------------------------------------------------------------------- |
| 97 | +-- The lex-pair carrier |
| 98 | +---------------------------------------------------------------------- |
| 99 | + |
| 100 | +record RankLex : Set where |
| 101 | + constructor mkLex |
| 102 | + field |
| 103 | + first : Ord |
| 104 | + second : Ord |
| 105 | + |
| 106 | +open RankLex public |
| 107 | + |
| 108 | +---------------------------------------------------------------------- |
| 109 | +-- Lex strict order |
| 110 | +---------------------------------------------------------------------- |
| 111 | + |
| 112 | +-- Two constructors. `<lex-first` covers the strict-on-first case. |
| 113 | +-- `<lex-second` covers the same-first-strict-on-second case; the |
| 114 | +-- shared implicit `a` on both sides makes the equality syntactic, |
| 115 | +-- so callers do not need to thread an `_≡_` witness. |
| 116 | + |
| 117 | +data _<lex_ : RankLex → RankLex → Set where |
| 118 | + <lex-first : ∀ {a₁ a₂ b₁ b₂} |
| 119 | + → a₁ <′ a₂ |
| 120 | + → mkLex a₁ b₁ <lex mkLex a₂ b₂ |
| 121 | + <lex-second : ∀ {a b₁ b₂} |
| 122 | + → b₁ <′ b₂ |
| 123 | + → mkLex a b₁ <lex mkLex a b₂ |
| 124 | + |
| 125 | +infix 4 _<lex_ |
| 126 | + |
| 127 | +---------------------------------------------------------------------- |
| 128 | +-- The lex rank |
| 129 | +---------------------------------------------------------------------- |
| 130 | + |
| 131 | +-- Diverges from `rank-pow` and `rank-adm` only in how it records |
| 132 | +-- the boundary information. For `bOmega ν` the second-component |
| 133 | +-- placeholder is `ω-rank-pow ν` itself — large enough to dominate |
| 134 | +-- any admissible `rank-pow α` (which the admissibility predicate |
| 135 | +-- bounds by `<′ ω-rank-pow ν`). |
| 136 | + |
| 137 | +rank-lex : BT → RankLex |
| 138 | +rank-lex bzero = mkLex oz oz |
| 139 | +rank-lex (bOmega ν) = mkLex (ω-rank-pow ν) (ω-rank-pow ν) |
| 140 | +rank-lex (bpsi ν α) = mkLex (ω-rank-pow ν) (rank-pow α) |
| 141 | +rank-lex (bplus x y) = mkLex (rank-pow (bplus x y)) oz |
| 142 | + -- The `bplus` case uses scalar `rank-pow` on the first component |
| 143 | + -- and `oz` on the second; we have no lex headline that fires on |
| 144 | + -- the `bplus` constructor in this slice (the `<ᵇ-+1` joint-bplus |
| 145 | + -- gap is unchanged). Consumers wanting a lex bplus-mono primitive |
| 146 | + -- would extend this case to `mkLex (rank-pow (bplus x y)) (...)` |
| 147 | + -- with their chosen second-component bound. |
| 148 | + |
| 149 | +---------------------------------------------------------------------- |
| 150 | +-- Definitional sanity |
| 151 | +---------------------------------------------------------------------- |
| 152 | + |
| 153 | +rank-lex-bzero : rank-lex bzero ≡ mkLex oz oz |
| 154 | +rank-lex-bzero = refl |
| 155 | + |
| 156 | +rank-lex-bOmega : ∀ ν → rank-lex (bOmega ν) ≡ mkLex (ω-rank-pow ν) (ω-rank-pow ν) |
| 157 | +rank-lex-bOmega _ = refl |
| 158 | + |
| 159 | +rank-lex-bpsi : ∀ ν α → rank-lex (bpsi ν α) ≡ mkLex (ω-rank-pow ν) (rank-pow α) |
| 160 | +rank-lex-bpsi _ _ = refl |
| 161 | + |
| 162 | +rank-lex-bplus : ∀ x y → rank-lex (bplus x y) ≡ mkLex (rank-pow (bplus x y)) oz |
| 163 | +rank-lex-bplus _ _ = refl |
| 164 | + |
| 165 | +---------------------------------------------------------------------- |
| 166 | +-- Headline: `<ᵇ-ψΩ≤` rank-mono under `rank-lex` |
| 167 | +---------------------------------------------------------------------- |
| 168 | + |
| 169 | +-- The boundary-case constructor. Hypotheses are exactly what |
| 170 | +-- `<ᵇ-ψΩ≤` carries (`ν ≤Ω μ`) plus the admissibility predicate's |
| 171 | +-- rank bound on ψ-arguments (`rank-pow α <′ ω-rank-pow ν`, which |
| 172 | +-- `WfAdm (bpsi ν α)` supplies via its `wf-adm-bpsi` constructor). |
| 173 | +-- |
| 174 | +-- Both sub-cases close: |
| 175 | +-- * `inj₁ ν<μ` — strict on first component via `ω-rank-pow-mono`. |
| 176 | +-- * `inj₂ refl` — ν = μ; first components are syntactically equal, |
| 177 | +-- so `<lex-second` fires with the admissibility bound on the |
| 178 | +-- second component. |
| 179 | + |
| 180 | +rank-mono-<ᵇ-ψΩ≤-lex : ∀ {ν μ α} |
| 181 | + → ν ≤Ω μ |
| 182 | + → rank-pow α <′ ω-rank-pow ν |
| 183 | + → rank-lex (bpsi ν α) <lex rank-lex (bOmega μ) |
| 184 | +rank-mono-<ᵇ-ψΩ≤-lex {ν} {μ} {α} ν≤μ adm with ≤Ω-split ν≤μ |
| 185 | +... | inj₁ ν<μ = <lex-first (ω-rank-pow-mono ν<μ) |
| 186 | +... | inj₂ refl = <lex-second adm |
0 commit comments