|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | + |
| 3 | +-- Parallel lex-rank for the joint-bplus bpsi-source-at-equality |
| 4 | +-- sub-case (scaffold, 2026-05-28). |
| 5 | +-- |
| 6 | +-- ## Where this sits |
| 7 | +-- |
| 8 | +-- The Slice 3 umbrella `Ordinal.Buchholz.RankMonoUmbrellaSlice3._<ᵇ¹_` |
| 9 | +-- case-splits the joint-bplus `<ᵇ-+1` discharge on the source's |
| 10 | +-- leftmost-leaf shape (`x₁ = bOmega μ` / `x₁ = bpsi ν α` / |
| 11 | +-- `x₁ = bplus _ _`). The bpsi sub-case further splits on |
| 12 | +-- `head-Ω x₁ vs head-Ω y₁` via `head-Ω-inv-bpsi`: |
| 13 | +-- |
| 14 | +-- * `ν <Ω head-Ω y₁` (strict) — closes via the Slice 3 headline |
| 15 | +-- `rank-mono-<ᵇ-+1-via-head-Ω`. |
| 16 | +-- * `ν ≡ head-Ω y₁` (boundary) — the BPSI-SOURCE-AT-EQUALITY |
| 17 | +-- sub-case. Closed at the ψ-rank level by `Ordinal.Buchholz. |
| 18 | +-- RankLexSlice3.{rank-adm,rank-lex}-bpsi-strict-at-equality`; |
| 19 | +-- OPEN at the bplus-chain rank-pow level because both pre- |
| 20 | +-- identified unblock routes (additive-principal closure on a |
| 21 | +-- generic ω-power-plus-rank-pow sum, strict-left-mono of `_⊕_`) |
| 22 | +-- are now CHECKED-REFUTED in `Ordinal.Brouwer. |
| 23 | +-- {AdditivePrincipalGenericRefuted,StrictLeftMonoRefuted}` |
| 24 | +-- (PR #146, 2026-05-28). |
| 25 | +-- |
| 26 | +-- This module lays the SCAFFOLD for the remaining viable forward |
| 27 | +-- path: a parallel rank `rank-lex-jb : BT → RankLex` whose `bplus` |
| 28 | +-- case carries a richer second component than `Ordinal.Buchholz. |
| 29 | +-- RankLex.rank-lex` (whose `bplus` case is `mkLex (rank-pow (bplus |
| 30 | +-- x y)) oz`, deliberately scoped to the `<ᵇ-ψΩ≤` boundary |
| 31 | +-- discharge per `RankLex.agda` lines 142-148). |
| 32 | +-- |
| 33 | +-- The richer second component carried here is the LEFTMOST-PSI-α |
| 34 | +-- rank `leftmost-α : BT → Ord`: |
| 35 | +-- |
| 36 | +-- leftmost-α bzero = oz |
| 37 | +-- leftmost-α (bOmega _) = oz |
| 38 | +-- leftmost-α (bpsi _ α) = rank-pow α |
| 39 | +-- leftmost-α (bplus x _) = leftmost-α x |
| 40 | +-- |
| 41 | +-- so that for left-leaning `bplus` chains whose leftmost atomic |
| 42 | +-- leaf is `bpsi ν α`, the second component carries `rank-pow α` — |
| 43 | +-- precisely the discriminator `RankLexSlice3.rank-lex-bpsi-strict- |
| 44 | +-- at-equality` exploits at the ψ-rank level. |
| 45 | +-- |
| 46 | +-- ## What this scaffold lands |
| 47 | +-- |
| 48 | +-- 1. `leftmost-α : BT → Ord` — the leftmost-ψ-α-rank function. |
| 49 | +-- 2. `leftmost-α-bzero/bOmega/bpsi/bplus` — definitional sanity |
| 50 | +-- (one per `BT` constructor; all `refl`). |
| 51 | +-- 3. `leftmost-α-bplus-left` — two-level convenience for the |
| 52 | +-- left-leaning `bplus` left-spine (mirrors `head-Ω-bplus-left`). |
| 53 | +-- 4. `rank-lex-jb : BT → RankLex` — the parallel lex rank. |
| 54 | +-- 5. `rank-lex-jb-bzero/bOmega/bpsi/bplus` — definitional sanity. |
| 55 | +-- 6. `rank-lex-jb-vs-rank-lex` — `rank-lex` and `rank-lex-jb` agree |
| 56 | +-- pointwise on first components. Pins the parallel-rank shape |
| 57 | +-- so consumers know what is and isn't preserved by the pivot. |
| 58 | +-- 7. `rank-lex-jb-strict-second-at-equal-first` — the load-bearing |
| 59 | +-- primitive for the bpsi-source-at-equality bplus-chain |
| 60 | +-- discharge: if first components are propositionally equal and |
| 61 | +-- the leftmost-α witnesses are strictly ordered, `<lex-second` |
| 62 | +-- fires. This is the LEX-rank shape the next session's full |
| 63 | +-- headline will consume; this scaffold ships the primitive + |
| 64 | +-- documents the consumer-side missing pieces (the equal-first |
| 65 | +-- propositional witness + the leftmost-α strict witness from |
| 66 | +-- the umbrella's case-split). |
| 67 | +-- |
| 68 | +-- ## What this scaffold deliberately does NOT close (honest scope) |
| 69 | +-- |
| 70 | +-- The full headline |
| 71 | +-- |
| 72 | +-- rank-jb-mono-<ᵇ-+1-joint-bplus-at-equal-head : ∀ {x₁ x₂ y₁ y₂} |
| 73 | +-- → WfCNF (bplus x₁ x₂) |
| 74 | +-- → WfCNF (bplus y₁ y₂) |
| 75 | +-- → x₁ <ᵇ y₁ |
| 76 | +-- → head-Ω x₁ ≡ head-Ω y₁ -- equality sub-case witness |
| 77 | +-- → rank-lex-jb (bplus x₁ x₂) <lex rank-lex-jb (bplus y₁ y₂) |
| 78 | +-- |
| 79 | +-- is NOT shipped in this slice. The case-split for closing it |
| 80 | +-- requires: |
| 81 | +-- |
| 82 | +-- (a) A FIRST-COMPONENT-EQUAL sub-case primitive: if `rank-pow |
| 83 | +-- (bplus x₁ x₂) ≡ rank-pow (bplus y₁ y₂)` and `leftmost-α |
| 84 | +-- (bplus x₁ x₂) <′ leftmost-α (bplus y₁ y₂)`, fire |
| 85 | +-- `<lex-second` (THIS slice's `rank-lex-jb-strict-second-at- |
| 86 | +-- equal-first`). |
| 87 | +-- (b) A FIRST-COMPONENT-STRICT sub-case primitive: if |
| 88 | +-- `rank-pow (bplus x₁ x₂) <′ rank-pow (bplus y₁ y₂)` then |
| 89 | +-- fire `<lex-first`. Decomposes via `⊕-mono-?-?` from the |
| 90 | +-- source `x₁ <ᵇ y₁` derivation; the bplus-chain sum bound is |
| 91 | +-- the same structural challenge that motivated this whole |
| 92 | +-- refactor. |
| 93 | +-- (c) A TRICHOTOMY on `rank-pow (bplus x₁ x₂)` vs |
| 94 | +-- `rank-pow (bplus y₁ y₂)` that hands the case-split to (a) |
| 95 | +-- or (b). Under `--safe --without-K`, this is a non-trivial |
| 96 | +-- decidability question — `Ord`-valued decidability bridges |
| 97 | +-- are not landed in `Ordinal.Brouwer.Phase13` yet. |
| 98 | +-- |
| 99 | +-- The honest verdict: this scaffold is necessary-but-not-sufficient |
| 100 | +-- foundation. The next session's task is the (a) + (b) + (c) |
| 101 | +-- assembly into a full headline; (b) and (c) each represent their |
| 102 | +-- own multi-PR slices. Documented here so the closure path is |
| 103 | +-- legible without re-deriving the analysis. |
| 104 | +-- |
| 105 | +-- ## Headlines (pinned in `Ordinal/Buchholz/Smoke.agda`) |
| 106 | +-- |
| 107 | +-- * `leftmost-α` — the discriminator |
| 108 | +-- * `rank-lex-jb` — the parallel rank |
| 109 | +-- * `rank-lex-jb-strict-second-at-equal-first` |
| 110 | +-- — the lex-second |
| 111 | +-- primitive |
| 112 | + |
| 113 | +module Ordinal.Buchholz.RankLexJointBplus where |
| 114 | + |
| 115 | +open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst) |
| 116 | + |
| 117 | +open import Ordinal.Brouwer using (Ord; oz) |
| 118 | +open import Ordinal.Brouwer.Phase13 using (_<′_) |
| 119 | +open import Ordinal.Buchholz.Syntax using |
| 120 | + ( BT |
| 121 | + ; bzero |
| 122 | + ; bOmega |
| 123 | + ; bplus |
| 124 | + ; bpsi |
| 125 | + ) |
| 126 | +open import Ordinal.Buchholz.RankPow using (rank-pow) |
| 127 | +open import Ordinal.Buchholz.RankLex using |
| 128 | + ( RankLex |
| 129 | + ; mkLex |
| 130 | + ; _<lex_ |
| 131 | + ; <lex-second |
| 132 | + ) |
| 133 | + |
| 134 | +---------------------------------------------------------------------- |
| 135 | +-- `leftmost-α : BT → Ord` — the leftmost-ψ-α-rank discriminator |
| 136 | +---------------------------------------------------------------------- |
| 137 | + |
| 138 | +-- For left-leaning `bplus` chains, walks the left spine to the |
| 139 | +-- atomic leaf and reads off `rank-pow α` if the leaf is `bpsi _ α`. |
| 140 | +-- For non-bpsi leaves (`bzero` / `bOmega _`), returns `oz` — the |
| 141 | +-- discriminator is only meaningful when the leftmost leaf is a |
| 142 | +-- ψ-source, which is the only case the bpsi-source-at-equality |
| 143 | +-- sub-case ever reaches. |
| 144 | + |
| 145 | +leftmost-α : BT → Ord |
| 146 | +leftmost-α bzero = oz |
| 147 | +leftmost-α (bOmega _) = oz |
| 148 | +leftmost-α (bpsi _ α) = rank-pow α |
| 149 | +leftmost-α (bplus x _) = leftmost-α x |
| 150 | + |
| 151 | +---------------------------------------------------------------------- |
| 152 | +-- Definitional sanity for `leftmost-α` |
| 153 | +---------------------------------------------------------------------- |
| 154 | + |
| 155 | +leftmost-α-bzero : leftmost-α bzero ≡ oz |
| 156 | +leftmost-α-bzero = refl |
| 157 | + |
| 158 | +leftmost-α-bOmega : ∀ ν → leftmost-α (bOmega ν) ≡ oz |
| 159 | +leftmost-α-bOmega _ = refl |
| 160 | + |
| 161 | +leftmost-α-bpsi : ∀ ν α → leftmost-α (bpsi ν α) ≡ rank-pow α |
| 162 | +leftmost-α-bpsi _ _ = refl |
| 163 | + |
| 164 | +leftmost-α-bplus : ∀ x y → leftmost-α (bplus x y) ≡ leftmost-α x |
| 165 | +leftmost-α-bplus _ _ = refl |
| 166 | + |
| 167 | +---------------------------------------------------------------------- |
| 168 | +-- Two-level convenience |
| 169 | +---------------------------------------------------------------------- |
| 170 | + |
| 171 | +-- Mirrors `HeadOmega.head-Ω-bplus-left`: walking two `bplus` levels |
| 172 | +-- bottoms out at the leftmost atomic leaf's `leftmost-α`. The |
| 173 | +-- bpsi-source-at-equality sub-case at the umbrella consumes the |
| 174 | +-- joint-bplus shape `bplus (bpsi ν α) x₂`, where the leftmost atom |
| 175 | +-- is one level deep; this lemma generalises to two levels for the |
| 176 | +-- nested case `bplus (bplus _ _) _`. |
| 177 | + |
| 178 | +leftmost-α-bplus-left : |
| 179 | + ∀ x y z → leftmost-α (bplus (bplus x y) z) ≡ leftmost-α x |
| 180 | +leftmost-α-bplus-left _ _ _ = refl |
| 181 | + |
| 182 | +---------------------------------------------------------------------- |
| 183 | +-- `rank-lex-jb : BT → RankLex` — the parallel lex rank |
| 184 | +---------------------------------------------------------------------- |
| 185 | + |
| 186 | +-- First component matches `RankLex.rank-lex` pointwise on all four |
| 187 | +-- constructors (the `bplus` case in `RankLex.rank-lex` is `rank-pow |
| 188 | +-- (bplus x y)` already, so `rank-lex-jb`'s first component matches |
| 189 | +-- by definition). Second component diverges only on `bplus`, |
| 190 | +-- replacing `oz` with `leftmost-α`. |
| 191 | +-- |
| 192 | +-- The atomic-leaf cases (`bzero`, `bOmega`, `bpsi`) keep the |
| 193 | +-- existing `RankLex.rank-lex` second component to preserve the |
| 194 | +-- existing `RankLex.rank-mono-<ᵇ-ψΩ≤-lex` boundary-discharge — the |
| 195 | +-- pivot is `bplus`-only. |
| 196 | + |
| 197 | +rank-lex-jb : BT → RankLex |
| 198 | +rank-lex-jb bzero = mkLex oz oz |
| 199 | +rank-lex-jb (bOmega ν) = mkLex (rank-pow (bOmega ν)) (rank-pow (bOmega ν)) |
| 200 | +rank-lex-jb (bpsi ν α) = mkLex (rank-pow (bpsi ν α)) (rank-pow α) |
| 201 | +rank-lex-jb (bplus x y) = mkLex (rank-pow (bplus x y)) (leftmost-α (bplus x y)) |
| 202 | + |
| 203 | +---------------------------------------------------------------------- |
| 204 | +-- Definitional sanity for `rank-lex-jb` |
| 205 | +---------------------------------------------------------------------- |
| 206 | + |
| 207 | +rank-lex-jb-bzero : rank-lex-jb bzero ≡ mkLex oz oz |
| 208 | +rank-lex-jb-bzero = refl |
| 209 | + |
| 210 | +rank-lex-jb-bOmega : |
| 211 | + ∀ ν → rank-lex-jb (bOmega ν) |
| 212 | + ≡ mkLex (rank-pow (bOmega ν)) (rank-pow (bOmega ν)) |
| 213 | +rank-lex-jb-bOmega _ = refl |
| 214 | + |
| 215 | +rank-lex-jb-bpsi : |
| 216 | + ∀ ν α → rank-lex-jb (bpsi ν α) |
| 217 | + ≡ mkLex (rank-pow (bpsi ν α)) (rank-pow α) |
| 218 | +rank-lex-jb-bpsi _ _ = refl |
| 219 | + |
| 220 | +rank-lex-jb-bplus : |
| 221 | + ∀ x y → rank-lex-jb (bplus x y) |
| 222 | + ≡ mkLex (rank-pow (bplus x y)) (leftmost-α (bplus x y)) |
| 223 | +rank-lex-jb-bplus _ _ = refl |
| 224 | + |
| 225 | +---------------------------------------------------------------------- |
| 226 | +-- Headline: `<lex-second` at equal first components |
| 227 | +---------------------------------------------------------------------- |
| 228 | + |
| 229 | +-- The load-bearing scaffold primitive. Consumers in the |
| 230 | +-- bpsi-source-at-equality bplus-chain context supply: |
| 231 | +-- |
| 232 | +-- * a propositional witness that the source's first component |
| 233 | +-- equals the target's (`rank-pow (bplus x₁ x₂) ≡ rank-pow |
| 234 | +-- (bplus y₁ y₂)`), which they must obtain from the (a)+(b)+(c) |
| 235 | +-- case-split documented in this module's preamble; AND |
| 236 | +-- * a strict-less-than witness on the leftmost-α discriminators |
| 237 | +-- (`leftmost-α (bplus x₁ x₂) <′ leftmost-α (bplus y₁ y₂)`), |
| 238 | +-- which the umbrella's `head-Ω-inv-bpsi` + the original |
| 239 | +-- `x₁ <ᵇ y₁` derivation supplies via `RankLexSlice3.rank-lex- |
| 240 | +-- bpsi-strict-at-equality` semantics: at the bpsi-source-at- |
| 241 | +-- equality sub-case `x₁ = bpsi ν α`, `y₁ = bpsi ν β`, with |
| 242 | +-- `α <ᵇ β` from the source derivation, `rank-pow α <′ rank-pow |
| 243 | +-- β` from the existing `RankMonoUmbrella.rank-pow-mono-<ᵇ⁰`, |
| 244 | +-- and `leftmost-α (bplus (bpsi ν α) x₂) = rank-pow α` (resp. |
| 245 | +-- β) by `leftmost-α-bplus` + `leftmost-α-bpsi`. |
| 246 | +-- |
| 247 | +-- Given both, fire `<lex-second` against the strict witness. The |
| 248 | +-- propositional first-component equality is rewritten in via |
| 249 | +-- `subst`-style content (here, by pattern-matching the equality |
| 250 | +-- and reusing the source `mkLex` on both sides). |
| 251 | + |
| 252 | +rank-lex-jb-strict-second-at-equal-first : |
| 253 | + ∀ {x₁ x₂ y₁ y₂} |
| 254 | + → rank-pow (bplus x₁ x₂) ≡ rank-pow (bplus y₁ y₂) |
| 255 | + → leftmost-α (bplus x₁ x₂) <′ leftmost-α (bplus y₁ y₂) |
| 256 | + → rank-lex-jb (bplus x₁ x₂) <lex rank-lex-jb (bplus y₁ y₂) |
| 257 | +rank-lex-jb-strict-second-at-equal-first {x₁} {x₂} {y₁} {y₂} first-eq strict = |
| 258 | + -- The `<lex-second` constructor requires the source and target |
| 259 | + -- first components to be syntactically equal under unification. |
| 260 | + -- Here they are propositionally equal (via `first-eq`) but not |
| 261 | + -- syntactically — `--without-K` forbids the `refl`-pattern |
| 262 | + -- shortcut. Transport the goal along `first-eq` via `subst` so |
| 263 | + -- the constructor's implicit first-component unifies. |
| 264 | + subst |
| 265 | + (λ a → mkLex a (leftmost-α (bplus x₁ x₂)) |
| 266 | + <lex |
| 267 | + mkLex (rank-pow (bplus y₁ y₂)) (leftmost-α (bplus y₁ y₂))) |
| 268 | + (sym-≡ first-eq) |
| 269 | + (<lex-second strict) |
| 270 | + where |
| 271 | + -- Local `sym` to avoid an extra stdlib import. |
| 272 | + sym-≡ : ∀ {ℓ} {A : Set ℓ} {a b : A} → a ≡ b → b ≡ a |
| 273 | + sym-≡ refl = refl |
0 commit comments