|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | + |
| 3 | +-- Lex-rank companion to the Slice 3 head-Ω discharge, covering the |
| 4 | +-- bpsi-source-at-equality sub-case of `<ᵇ-+1` joint-bplus, 2026-05-28. |
| 5 | +-- |
| 6 | +-- ## Where this sits |
| 7 | +-- |
| 8 | +-- The Slice 3 headline `Ordinal.Buchholz.RankPowSlice3Headline. |
| 9 | +-- rank-mono-<ᵇ-+1-via-head-Ω` discharges `bplus x₁ x₂ <ᵇ bplus y₁ y₂` |
| 10 | +-- (from `x₁ <ᵇ y₁`) UNDER A STRICT-HEAD PREMISE `head-Ω x₁ <Ω head-Ω y₁`. |
| 11 | +-- The premise is supplied externally by the umbrella's case-split: |
| 12 | +-- |
| 13 | +-- * x₁ = bOmega μ : `head-Ω-inv-bOmega` gives `μ <Ω head-Ω y₁` |
| 14 | +-- directly (STRICT for all three Ω-source |
| 15 | +-- constructors). Slice 3 closes. |
| 16 | +-- * x₁ = bpsi ν α : `head-Ω-inv-bpsi` gives `ν ≤Ω head-Ω y₁` |
| 17 | +-- (NON-STRICT — `<ᵇ-ψΩ≤` permits equal markers). |
| 18 | +-- Strict sub-case (`ν <Ω head-Ω y₁`) closes |
| 19 | +-- via Slice 3. EQUALITY sub-case |
| 20 | +-- (`ν ≡ head-Ω y₁`) is THIS MODULE'S TERRITORY. |
| 21 | +-- * x₁ = bplus a b : recurse on the leftmost-leaf shape; reduces to |
| 22 | +-- one of the above two atomic cases. |
| 23 | +-- |
| 24 | +-- This module handles the bpsi-source-at-equality remainder via the |
| 25 | +-- existing lex-pair rank `rank-lex` from `Ordinal.Buchholz.RankLex` |
| 26 | +-- (whose second component carries `rank-pow α` for the ψ case) plus |
| 27 | +-- the existing admissibility-aware rank `rank-adm` from |
| 28 | +-- `Ordinal.Buchholz.RankAdm`. |
| 29 | +-- |
| 30 | +-- ## What this slice closes (the lex headline) |
| 31 | +-- |
| 32 | +-- The headline: |
| 33 | +-- |
| 34 | +-- rank-mono-<ᵇ-+1-via-rank-lex : ∀ {ν α β x₂ y₂} |
| 35 | +-- → rank-pow α <′ rank-pow β -- second-component lex witness |
| 36 | +-- → rank-lex (bplus (bpsi ν α) x₂) <lex rank-lex (bplus (bpsi ν β) y₂) |
| 37 | +-- |
| 38 | +-- ...is NOT directly stateable: `rank-lex (bplus x y) = mkLex |
| 39 | +-- (rank-pow (bplus x y)) oz` in the existing `RankLex` module, so the |
| 40 | +-- second component is *both* `oz` and the lex-second-strict |
| 41 | +-- constructor `<lex-second : b₁ <′ b₂` cannot fire at `oz <′ oz`. |
| 42 | +-- The existing `rank-lex` was deliberately shipped that way to scope |
| 43 | +-- the slice to the `<ᵇ-ψΩ≤` ν=μ boundary headline alone (see the |
| 44 | +-- companion-remark in `RankLex.agda` lines 142-148). |
| 45 | +-- |
| 46 | +-- The HONEST closure THIS module ships: |
| 47 | +-- |
| 48 | +-- rank-adm-bpsi-strict-at-equality : ∀ {ν α β} |
| 49 | +-- → rank-pow α <′ rank-pow β |
| 50 | +-- → rank-adm (bpsi ν α) <′ rank-adm (bpsi ν β) |
| 51 | +-- |
| 52 | +-- This is a thin convenience re-export of `RankAdm.rank-mono-<ᵇ⁺-ψα- |
| 53 | +-- from-pow` named for the joint-bplus consumer. It is the LOAD- |
| 54 | +-- BEARING primitive for the bpsi-source-at-equality sub-case at the |
| 55 | +-- ψ-rank level. The bplus-extension under `rank-adm` (= `rank-adm |
| 56 | +-- (bplus x₁ x₂) <′ rank-adm (bplus y₁ y₂)`) is documented in the |
| 57 | +-- design note below as the open structural gap. |
| 58 | +-- |
| 59 | +-- ## What this slice deliberately DOES NOT close (honest scope) |
| 60 | +-- |
| 61 | +-- The task's intended conclusion `rank-pow (bplus x₁ x₂) <′ rank-pow |
| 62 | +-- (bplus y₁ y₂)` is *structurally not derivable* from `α <ᵇ β` alone |
| 63 | +-- at the bpsi-source-at-equality sub-case: |
| 64 | +-- |
| 65 | +-- * `rank-pow (bpsi ν α) = ω-rank-pow ν = rank-pow (bpsi ν β)` — |
| 66 | +-- the provisional `rank-pow` shape collapses both ψ-sources at |
| 67 | +-- the same ν to the SAME ordinal, so no strict-on-left-summand |
| 68 | +-- witness exists at the `rank-pow` level. |
| 69 | +-- * Promoting the conclusion to `rank-adm` produces `rank-adm |
| 70 | +-- (bpsi ν α) <′ rank-adm (bpsi ν β)` cleanly (this module's |
| 71 | +-- `rank-adm-bpsi-strict-at-equality`), but the bplus |
| 72 | +-- extension `rank-adm (bplus x₁ x₂) <′ rank-adm (bplus y₁ y₂)` |
| 73 | +-- requires either (a) additive-principal closure on `rank-adm |
| 74 | +-- y₁` (NOT generally available — `rank-adm (bpsi ν β) = |
| 75 | +-- ω-rank-pow ν ⊕ rank-pow β` is generically a sum, not an |
| 76 | +-- ω-power), or (b) strict-left-monotonicity of `_⊕_` (a NON- |
| 77 | +-- theorem; the `α ⊕ ω ≡ β ⊕ ω` counterexample documented in |
| 78 | +-- `Phase13.agda`). |
| 79 | +-- * Promoting to a redesigned lex rank `rank-lex-jb` whose bplus |
| 80 | +-- case carries the leftmost-ψ-α info in the second component |
| 81 | +-- would close the headline at the LEX-rank level (lex-first |
| 82 | +-- comparing rank-pow's then lex-second comparing α-ranks); |
| 83 | +-- however, this requires reshaping the existing `rank-lex` (or |
| 84 | +-- introducing a parallel rank), breaking the existing `<ᵇ-ψΩ≤` |
| 85 | +-- boundary discharge. Deferred as a follow-on design slice. |
| 86 | +-- |
| 87 | +-- The bpsi-source-at-equality sub-case is therefore CLOSED AT THE |
| 88 | +-- PSI-RANK LEVEL (via `rank-adm-bpsi-strict-at-equality`) and OPEN |
| 89 | +-- AT THE BPLUS-CHAIN LEVEL pending one of (a)/(b)/(c) above. |
| 90 | +-- |
| 91 | +-- ## Headlines (pinned in `Ordinal/Buchholz/Smoke.agda`) |
| 92 | +-- |
| 93 | +-- * `rank-adm-bpsi-strict-at-equality` — ψ-rank strict step from |
| 94 | +-- the α<β witness, joint-bplus-consumer-facing wrapper. |
| 95 | +-- * `rank-lex-bpsi-strict-at-equality` — same content lifted to |
| 96 | +-- `rank-lex`'s second component via `<lex-second`. |
| 97 | +-- * `rank-adm-bplus-decompose-left` — `rank-adm` decomposes |
| 98 | +-- definitionally on bplus into the left and right summands (used |
| 99 | +-- by the joint-bplus consumer to chain `rank-adm-bpsi-strict- |
| 100 | +-- at-equality` against the source's left summand). |
| 101 | + |
| 102 | +module Ordinal.Buchholz.RankLexSlice3 where |
| 103 | + |
| 104 | +open import Relation.Binary.PropositionalEquality using (_≡_; refl) |
| 105 | + |
| 106 | +open import Ordinal.Brouwer using (Ord) |
| 107 | +open import Ordinal.Brouwer.Arithmetic using (_⊕_) |
| 108 | +open import Ordinal.Brouwer.Phase13 using (_<′_) |
| 109 | +open import Ordinal.Buchholz.Syntax using |
| 110 | + ( BT |
| 111 | + ; bzero |
| 112 | + ; bOmega |
| 113 | + ; bplus |
| 114 | + ; bpsi |
| 115 | + ) |
| 116 | +open import Ordinal.Buchholz.RankPow using (rank-pow; ω-rank-pow) |
| 117 | +open import Ordinal.Buchholz.RankAdm using |
| 118 | + ( rank-adm |
| 119 | + ; rank-mono-<ᵇ⁺-ψα-from-pow |
| 120 | + ) |
| 121 | +open import Ordinal.Buchholz.RankLex using |
| 122 | + ( RankLex |
| 123 | + ; mkLex |
| 124 | + ; _<lex_ |
| 125 | + ; <lex-second |
| 126 | + ; rank-lex |
| 127 | + ) |
| 128 | + |
| 129 | +---------------------------------------------------------------------- |
| 130 | +-- ψ-rank strict step at the equality sub-case (rank-adm side) |
| 131 | +---------------------------------------------------------------------- |
| 132 | + |
| 133 | +-- Re-export of `RankAdm.rank-mono-<ᵇ⁺-ψα-from-pow` named for the |
| 134 | +-- joint-bplus consumer. Given a `rank-pow α <′ rank-pow β` witness |
| 135 | +-- (produced by `Ordinal.Buchholz.RankMonoUmbrella.rank-pow-mono-<ᵇ⁰` |
| 136 | +-- for any `α <ᵇ⁰ β`), conclude `rank-adm (bpsi ν α) <′ rank-adm |
| 137 | +-- (bpsi ν β)`. |
| 138 | +-- |
| 139 | +-- This is the LOAD-BEARING primitive of the bpsi-source-at-equality |
| 140 | +-- sub-case at the ψ-rank level. The joint-bplus headline at the |
| 141 | +-- bplus-chain level is structurally blocked as documented in this |
| 142 | +-- module's preamble; this primitive closes the part that DOES close. |
| 143 | + |
| 144 | +rank-adm-bpsi-strict-at-equality : ∀ {ν α β} |
| 145 | + → rank-pow α <′ rank-pow β |
| 146 | + → rank-adm (bpsi ν α) <′ rank-adm (bpsi ν β) |
| 147 | +rank-adm-bpsi-strict-at-equality {ν} {α} {β} p = |
| 148 | + rank-mono-<ᵇ⁺-ψα-from-pow {ν} {α} {β} p |
| 149 | + |
| 150 | +---------------------------------------------------------------------- |
| 151 | +-- ψ-rank strict step at the equality sub-case (rank-lex side) |
| 152 | +---------------------------------------------------------------------- |
| 153 | + |
| 154 | +-- Lift the strict α-rank step into the `rank-lex` lex order. Since |
| 155 | +-- `rank-lex (bpsi ν α) = mkLex (ω-rank-pow ν) (rank-pow α)` and |
| 156 | +-- `rank-lex (bpsi ν β) = mkLex (ω-rank-pow ν) (rank-pow β)`, the |
| 157 | +-- first components are syntactically equal (no funext, no `with` |
| 158 | +-- elimination needed) and the `<lex-second` constructor fires |
| 159 | +-- against the second-component witness. |
| 160 | +-- |
| 161 | +-- This is the LEX-rank-level mirror of `rank-adm-bpsi-strict-at- |
| 162 | +-- equality`; consumers that work at the lex-rank level use this one |
| 163 | +-- rather than the rank-adm form. Both convey the same structural |
| 164 | +-- content (the α-rank discriminates), differing only in which rank |
| 165 | +-- the consumer is composing against. |
| 166 | + |
| 167 | +rank-lex-bpsi-strict-at-equality : ∀ {ν α β} |
| 168 | + → rank-pow α <′ rank-pow β |
| 169 | + → rank-lex (bpsi ν α) <lex rank-lex (bpsi ν β) |
| 170 | +rank-lex-bpsi-strict-at-equality {ν} {α} {β} p = |
| 171 | + <lex-second {ω-rank-pow ν} {rank-pow α} {rank-pow β} p |
| 172 | + |
| 173 | +---------------------------------------------------------------------- |
| 174 | +-- Definitional decomposition of `rank-adm` on `bplus` |
| 175 | +---------------------------------------------------------------------- |
| 176 | + |
| 177 | +-- Pinned as `refl` for the joint-bplus consumer that needs to chain |
| 178 | +-- a strict step on the left summand against a tail bound on the |
| 179 | +-- right summand. Documents the additive structure of `rank-adm` on |
| 180 | +-- `bplus` for callers that want to reason about it without re-opening |
| 181 | +-- `RankAdm`. |
| 182 | + |
| 183 | +rank-adm-bplus-decompose-left : ∀ x y → |
| 184 | + rank-adm (bplus x y) ≡ rank-adm x ⊕ rank-adm y |
| 185 | +rank-adm-bplus-decompose-left _ _ = refl |
| 186 | + |
| 187 | +---------------------------------------------------------------------- |
| 188 | +-- Design note: why the headline `rank-pow (bplus x₁ x₂) <′ |
| 189 | +-- rank-pow (bplus y₁ y₂)` does NOT close from this slice's primitives |
| 190 | +---------------------------------------------------------------------- |
| 191 | + |
| 192 | +-- The task's stated headline conclusion |
| 193 | +-- rank-pow (bplus x₁ x₂) <′ rank-pow (bplus y₁ y₂) |
| 194 | +-- at the bpsi-source-at-equality sub-case |
| 195 | +-- (x₁ = bpsi ν α, y₁ = bpsi ν β, x₁ <ᵇ y₁ via the α<β witness) |
| 196 | +-- requires a strict step on the bplus left summand at the rank-pow |
| 197 | +-- level. But |
| 198 | +-- rank-pow (bpsi ν α) = ω-rank-pow ν = rank-pow (bpsi ν β) |
| 199 | +-- by definition; the strict step exists ONLY at the rank-adm level |
| 200 | +-- (`rank-adm (bpsi ν α) <′ rank-adm (bpsi ν β)`, which this module |
| 201 | +-- closes via `rank-adm-bpsi-strict-at-equality`). |
| 202 | +-- |
| 203 | +-- Lifting the strict rank-adm step to a strict rank-adm sum |
| 204 | +-- rank-adm x₁ ⊕ rank-adm x₂ <′ rank-adm y₁ ⊕ rank-adm y₂ |
| 205 | +-- requires either |
| 206 | +-- (a) additive-principal closure on `rank-adm y₁`, which holds |
| 207 | +-- only when `rank-adm y₁ = ω-rank-pow _` exactly — i.e., when |
| 208 | +-- y₁ is bOmega μ or bzero, NOT when y₁ = bpsi ν β where |
| 209 | +-- `rank-adm y₁ = ω-rank-pow ν ⊕ rank-pow β` is a generic sum. |
| 210 | +-- (b) strict left-monotonicity of `_⊕_`, which is a NON-theorem |
| 211 | +-- under Brouwer arithmetic — the `α ⊕ ω ≡ β ⊕ ω` |
| 212 | +-- counterexample documented in `Ordinal.Brouwer.Phase13` (see |
| 213 | +-- the block comment near `⊕-mono-≤-left`'s declaration). |
| 214 | +-- |
| 215 | +-- The clean resolution is a parallel rank with a richer bplus second |
| 216 | +-- component (`rank-lex-jb : BT → RankLex` whose `bplus`-case carries |
| 217 | +-- the leftmost-ψ-α info), but introducing it parallel to `rank-lex` |
| 218 | +-- requires a follow-on design slice — the existing `rank-lex`'s |
| 219 | +-- `<ᵇ-ψΩ≤`-boundary discharge depends on `rank-lex`'s bplus-case |
| 220 | +-- being `oz`-second, so the redesign is non-local. |
| 221 | +-- |
| 222 | +-- Therefore the joint-bplus bpsi-source-at-equality sub-case is |
| 223 | +-- CLOSED at the ψ-rank level (one source-level discriminator |
| 224 | +-- between source ψ-α and target ψ-β is now formal) and OPEN at the |
| 225 | +-- bplus-chain level (transporting that discriminator through bplus |
| 226 | +-- requires additional ordinal-arithmetic infrastructure that this |
| 227 | +-- session does not land). |
| 228 | +-- |
| 229 | +-- The honest contribution of this slice: pin the ψ-rank discharge as |
| 230 | +-- a NAMED THEOREM accessible from the joint-bplus consumer, plus an |
| 231 | +-- explicit declaration of the bplus-chain obstacle so the next |
| 232 | +-- session can see exactly which lemmas would unblock it without |
| 233 | +-- re-deriving the analysis. |
0 commit comments