|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | + |
| 3 | +-- Slice 3 prerequisites for the `<ᵇ-+1` joint-bplus headline |
| 4 | +-- `rank-mono-<ᵇ-+1-via-head-Ω`. Three primitives land here: |
| 5 | +-- |
| 6 | +-- * `NonBzero` — left-spine non-bzero predicate (rules out the |
| 7 | +-- degenerate `bplus bzero bzero` chains that WfCNF technically |
| 8 | +-- allows but CNF normalisation excludes). |
| 9 | +-- * `ω-rank-pow-succ-≤-via-<Ω` — strict-jump bridge from |
| 10 | +-- `μ <Ω ν` to `ω-rank-pow-succ μ ≤′ ω-rank-pow ν`. Closes the |
| 11 | +-- gap between Slice 2-bplus's upper bound on the source's rank |
| 12 | +-- (`rank-pow t <′ ω-rank-pow-succ (head-Ω t)`) and the lower |
| 13 | +-- bound on the target's rank. |
| 14 | +-- * `head-Ω-lower-bound` — head-Ω LOWER bound under WfCNF + |
| 15 | +-- NonBzero. Dual of `rank-pow-dominated-by-head-Ω` (which is |
| 16 | +-- the corresponding upper). |
| 17 | +-- |
| 18 | +-- ## What this does NOT close |
| 19 | +-- |
| 20 | +-- The Slice 3 HEADLINE `rank-mono-<ᵇ-+1-via-head-Ω` itself requires |
| 21 | +-- a STRICT-jump on `head-Ω x₁ <Ω head-Ω y₁` from `x₁ <ᵇ y₁`. The |
| 22 | +-- existing `head-Ω-inv-bpsi` only gives `≤Ω` (via the `<ᵇ-ψΩ≤` |
| 23 | +-- constructor — bpsi can be `<ᵇ` an Ω at equal marker), so the |
| 24 | +-- ψ-source bpsi sub-case `bpsi ν α <ᵇ y₁` at `ν = head-Ω y₁` does |
| 25 | +-- NOT close under the head-Ω route alone. The strict jump there |
| 26 | +-- must come from `α`'s rank (rank-adm refinement on the second |
| 27 | +-- component, or a rank-lex combination). Documented at the bottom |
| 28 | +-- of this file as the open follow-on. |
| 29 | +-- |
| 30 | +-- ## Headlines (pin in `Ordinal/Buchholz/Smoke.agda`) |
| 31 | +-- |
| 32 | +-- * `NonBzero` (data type) |
| 33 | +-- * `nz-bOmega`, `nz-bpsi`, `nz-bplus` (constructors) |
| 34 | +-- * `ω-rank-pow-succ-≤-via-<Ω` |
| 35 | +-- * `head-Ω-lower-bound` |
| 36 | + |
| 37 | +module Ordinal.Buchholz.RankPowSlice3 where |
| 38 | + |
| 39 | +open import Data.Nat.Base using (suc; s≤s) |
| 40 | + |
| 41 | +open import Ordinal.Brouwer.Arithmetic using (_⊕_) |
| 42 | +open import Ordinal.Brouwer.Phase13 using |
| 43 | + ( _≤′_ |
| 44 | + ; ≤′-refl |
| 45 | + ; ≤′-trans |
| 46 | + ; f-in-lim′ |
| 47 | + ; ⊕-left-≤-sum |
| 48 | + ) |
| 49 | +open import Ordinal.Brouwer.OmegaPow using |
| 50 | + ( ω^_ |
| 51 | + ; ω^-mono-≤ |
| 52 | + ) |
| 53 | +open import Ordinal.OmegaMarkers using |
| 54 | + ( fin |
| 55 | + ; ω |
| 56 | + ; _<Ω_ |
| 57 | + ; fin<fin |
| 58 | + ; fin<ω |
| 59 | + ) |
| 60 | +open import Ordinal.Buchholz.Syntax using |
| 61 | + ( BT |
| 62 | + ; bzero |
| 63 | + ; bOmega |
| 64 | + ; bplus |
| 65 | + ; bpsi |
| 66 | + ) |
| 67 | +open import Ordinal.Buchholz.WellFormedCNF using |
| 68 | + ( WfCNF |
| 69 | + ; wf-cnf-bomega |
| 70 | + ; wf-cnf-bpsi |
| 71 | + ; wf-cnf-bplus |
| 72 | + ) |
| 73 | +open import Ordinal.Buchholz.HeadOmega using (head-Ω) |
| 74 | +open import Ordinal.Buchholz.RankPow using |
| 75 | + ( rank-pow |
| 76 | + ; ω-rank-pow |
| 77 | + ; ω-rank-pow-succ |
| 78 | + ) |
| 79 | + |
| 80 | +---------------------------------------------------------------------- |
| 81 | +-- NonBzero: left-spine non-bzero predicate |
| 82 | +---------------------------------------------------------------------- |
| 83 | + |
| 84 | +-- WfCNF allows the degenerate `bplus bzero bzero` (the right |
| 85 | +-- summand bzero is ≤ᵇ the left bzero via `<ᵇ`-reflexivity on the |
| 86 | +-- bzero atomic), so the head-Ω lower bound needs an extra |
| 87 | +-- discriminator to exclude that case. `NonBzero` walks the |
| 88 | +-- leftmost spine and demands at least one non-bzero atomic head |
| 89 | +-- — which is exactly what makes `head-Ω t` informative (else |
| 90 | +-- `head-Ω t = head-Ω bzero = fin 0` is a default whose rank |
| 91 | +-- `ω-rank-pow (fin 0) = ω^1 = ω` is NOT below `rank-pow t = oz`). |
| 92 | +-- |
| 93 | +-- `NonBzero` is monotone in the leftmost-spine constructor: |
| 94 | +-- `bplus x y` is NonBzero iff `x` is. This matches `head-Ω`'s |
| 95 | +-- own leftmost-spine recursion. |
| 96 | + |
| 97 | +data NonBzero : BT → Set where |
| 98 | + nz-bOmega : ∀ {μ} → NonBzero (bOmega μ) |
| 99 | + nz-bpsi : ∀ {ν α} → NonBzero (bpsi ν α) |
| 100 | + nz-bplus : ∀ {x y} → NonBzero x → NonBzero (bplus x y) |
| 101 | + |
| 102 | +---------------------------------------------------------------------- |
| 103 | +-- Strict-jump bridge |
| 104 | +---------------------------------------------------------------------- |
| 105 | + |
| 106 | +-- The "next ω-power up" target `ω-rank-pow-succ μ` is below the |
| 107 | +-- NEXT marker's `ω-rank-pow ν` whenever `μ <Ω ν`. Two cases on |
| 108 | +-- the `<Ω` derivation: |
| 109 | +-- |
| 110 | +-- * `fin m <Ω fin n` from `m < n` (= `suc m ≤ n`): |
| 111 | +-- `ω-rank-pow-succ (fin m) = ω^(suc(suc m))`, |
| 112 | +-- `ω-rank-pow (fin n) = ω^(suc n)`. `s≤s p : suc(suc m) ≤ |
| 113 | +-- suc n`, `ω^-mono-≤ (s≤s p)` discharges. |
| 114 | +-- * `fin m <Ω ω`: |
| 115 | +-- `ω-rank-pow-succ (fin m) = ω^(suc(suc m))`, |
| 116 | +-- `ω-rank-pow ω = olim (λ k → ω^(suc k))`. Pick branch |
| 117 | +-- `suc m` in the limit: `f-in-lim′ (λ k → ω^(suc k)) (suc m)` |
| 118 | +-- gives `ω^(suc(suc m)) ≤′ olim ...`. |
| 119 | +-- * `ω <Ω _`: impossible (ω is top of `OmegaIndex`; no `_<Ω_` |
| 120 | +-- constructor takes ω on the left). |
| 121 | + |
| 122 | +ω-rank-pow-succ-≤-via-<Ω : ∀ {μ ν} → μ <Ω ν → ω-rank-pow-succ μ ≤′ ω-rank-pow ν |
| 123 | +ω-rank-pow-succ-≤-via-<Ω {fin m} {fin n} (fin<fin p) = ω^-mono-≤ (s≤s p) |
| 124 | +ω-rank-pow-succ-≤-via-<Ω {fin m} {ω} fin<ω = |
| 125 | + f-in-lim′ (λ k → ω^ (suc k)) (suc m) |
| 126 | + |
| 127 | +---------------------------------------------------------------------- |
| 128 | +-- head-Ω LOWER bound under WfCNF + NonBzero |
| 129 | +---------------------------------------------------------------------- |
| 130 | + |
| 131 | +-- For any WfCNF + NonBzero term `t`, the leading marker's |
| 132 | +-- `ω-rank-pow` is BELOW the full `rank-pow t`. Dual of |
| 133 | +-- `rank-pow-dominated-by-head-Ω : rank-pow t <′ ω-rank-pow-succ |
| 134 | +-- (head-Ω t)` (the same form with `succ` and `<′` for the upper). |
| 135 | +-- |
| 136 | +-- Structural recursion on the WfCNF derivation, with NonBzero |
| 137 | +-- supplying the leftmost-spine non-degeneracy: |
| 138 | +-- |
| 139 | +-- * `bOmega ν`: head-Ω = ν, rank-pow = ω-rank-pow ν. `≤′-refl`. |
| 140 | +-- * `bpsi ν α`: head-Ω = ν, rank-pow = ω-rank-pow ν (provisional |
| 141 | +-- shape from `RankPow.agda`). `≤′-refl`. |
| 142 | +-- * `bplus x y`: head-Ω = head-Ω x, rank-pow = rank-pow x ⊕ |
| 143 | +-- rank-pow y. IH on x (with `NonBzero x` extracted from |
| 144 | +-- `nz-bplus nzx`) gives `ω-rank-pow (head-Ω x) ≤′ rank-pow x`; |
| 145 | +-- chain through `⊕-left-≤-sum (rank-pow y) : rank-pow x ≤′ |
| 146 | +-- rank-pow x ⊕ rank-pow y` via `≤′-trans`. |
| 147 | +-- |
| 148 | +-- Termination: structural recursion on the `WfCNF` carrier (each |
| 149 | +-- recursive call passes `wfx`, a strictly-smaller sub-derivation). |
| 150 | +-- No funext, no postulates, no rank-mono dependency. |
| 151 | + |
| 152 | +head-Ω-lower-bound : ∀ {t} → WfCNF t → NonBzero t → |
| 153 | + ω-rank-pow (head-Ω t) ≤′ rank-pow t |
| 154 | +head-Ω-lower-bound {bOmega μ} (wf-cnf-bomega _) nz-bOmega = |
| 155 | + ≤′-refl {ω-rank-pow μ} |
| 156 | +head-Ω-lower-bound {bpsi ν α} (wf-cnf-bpsi _ _) nz-bpsi = |
| 157 | + ≤′-refl {ω-rank-pow ν} |
| 158 | +head-Ω-lower-bound {bplus x y} (wf-cnf-bplus wfx _ _ _) (nz-bplus nzx) = |
| 159 | + ≤′-trans {ω-rank-pow (head-Ω x)} {rank-pow x} {rank-pow x ⊕ rank-pow y} |
| 160 | + (head-Ω-lower-bound wfx nzx) |
| 161 | + (⊕-left-≤-sum {rank-pow x} (rank-pow y)) |
| 162 | + |
| 163 | +---------------------------------------------------------------------- |
| 164 | +-- Slice 3 design note (informal) |
| 165 | +---------------------------------------------------------------------- |
| 166 | + |
| 167 | +-- The intended Slice 3 headline: |
| 168 | +-- |
| 169 | +-- rank-mono-<ᵇ-+1-via-head-Ω : ∀ {x₁ x₂ y₁ y₂} |
| 170 | +-- → WfCNF (bplus x₁ x₂) → NonBzero x₁ |
| 171 | +-- → WfCNF (bplus y₁ y₂) → NonBzero y₁ |
| 172 | +-- → x₁ <ᵇ y₁ |
| 173 | +-- → rank-pow (bplus x₁ x₂) <′ rank-pow (bplus y₁ y₂) |
| 174 | +-- |
| 175 | +-- Strategy (chain): |
| 176 | +-- |
| 177 | +-- rank-pow (bplus x₁ x₂) |
| 178 | +-- <′ ω-rank-pow-succ (head-Ω x₁) -- by rank-pow-dominated-by-head-Ω |
| 179 | +-- -- + head-Ω-bplus |
| 180 | +-- ≤′ ω-rank-pow (head-Ω y₁) -- by ω-rank-pow-succ-≤-via-<Ω |
| 181 | +-- -- + STRICT-JUMP head-Ω x₁ <Ω head-Ω y₁ |
| 182 | +-- ≤′ rank-pow y₁ -- by head-Ω-lower-bound |
| 183 | +-- ≤′ rank-pow (bplus y₁ y₂) -- by ⊕-left-≤-sum |
| 184 | +-- |
| 185 | +-- The STRICT-JUMP step is the pinch. By cases on x₁ (NonBzero |
| 186 | +-- guarantees not bzero): |
| 187 | +-- |
| 188 | +-- * x₁ = bOmega μ: `head-Ω-inv-bOmega : bOmega μ <ᵇ y₁ → |
| 189 | +-- μ <Ω head-Ω y₁` is STRICT. Closes directly. |
| 190 | +-- * x₁ = bpsi ν α: `head-Ω-inv-bpsi : bpsi ν α <ᵇ y₁ → |
| 191 | +-- ν ≤Ω head-Ω y₁` is NON-STRICT (tracks `<ᵇ-ψΩ≤` which |
| 192 | +-- permits equal markers between ψ-source and Ω-target). |
| 193 | +-- When `ν = head-Ω y₁`, the strict jump must come from α's |
| 194 | +-- rank — which lives in the rank-adm refinement, NOT the |
| 195 | +-- head-Ω route. |
| 196 | +-- * x₁ = bplus a b: `head-Ω (bplus a b) = head-Ω a`; needs |
| 197 | +-- recursive inversion on the leading-leaf shape. When the |
| 198 | +-- leading leaf is bOmega, closes via the bOmega case. When |
| 199 | +-- bpsi, hits the same pinch as above. |
| 200 | +-- |
| 201 | +-- The Slice 3 closure path under design: |
| 202 | +-- |
| 203 | +-- (A) Combine the head-Ω route with rank-lex (`Ordinal.Buchholz. |
| 204 | +-- RankLex`) for the bpsi-source-at-equality sub-case. The |
| 205 | +-- rank-lex second component carries α-rank information that |
| 206 | +-- discharges the equality case via `<ᵇ-+ψ` / `<ᵇ-ψα`-style |
| 207 | +-- admissibility, mirroring the `<ᵇ-ψΩ≤` boundary closure |
| 208 | +-- (RankLex.agda, 2026-05-27). |
| 209 | +-- |
| 210 | +-- (B) Refine `head-Ω-inv-bpsi` to split on the source constructor: |
| 211 | +-- report `<Ω` (strict) for `<ᵇ-ψΩ` and `<ᵇ-ψ+`, `≤Ω` |
| 212 | +-- (non-strict) only for `<ᵇ-ψΩ≤`. Then chain the equality |
| 213 | +-- case through admissibility separately. |
| 214 | +-- |
| 215 | +-- Both routes preserve the head-Ω discipline (no rank-mono |
| 216 | +-- dependency in the inversion family — option (b) from |
| 217 | +-- `RankPow.agda`'s Slice 2-bplus follow-on plan). Route (A) is |
| 218 | +-- cleaner: it composes existing landed primitives rather than |
| 219 | +-- refining an inversion lemma. Implementation is a follow-on |
| 220 | +-- slice. |
0 commit comments