|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | + |
| 3 | +-- Deliberately-narrowed `_<ᵇ⁻_` umbrella covering the |
| 4 | +-- strict-head-closed slice (Slice 4, 2026-05-28). |
| 5 | +-- |
| 6 | +-- ## Where this sits |
| 7 | +-- |
| 8 | +-- `Ordinal.Buchholz.OrderRestricted._<ᵇ⁻_` is the WfCNF-restricted |
| 9 | +-- form of `_<ᵇ_` — a record bundling source-WfCNF, target-WfCNF, |
| 10 | +-- and an underlying `<ᵇ` derivation. The full umbrella |
| 11 | +-- `rank-pow-mono-<ᵇ⁻ : x <ᵇ⁻ y → rank-pow x <′ rank-pow y` over |
| 12 | +-- all 13 `_<ᵇ_` constructors is the open Slice 4 goal in |
| 13 | +-- `docs/echo-types/buchholz-rank-obstruction.adoc`. |
| 14 | +-- |
| 15 | +-- Status of the per-constructor closures, post-Slice-3 (after PR |
| 16 | +-- #141 / #142 / #143): |
| 17 | +-- |
| 18 | +-- * 10 constructors closed under `_<ᵇ⁰_` via |
| 19 | +-- `Ordinal.Buchholz.RankMonoUmbrella.rank-pow-mono-<ᵇ⁰`. |
| 20 | +-- * 11th constructor (`<ᵇ-+1` joint-bplus) closed under the |
| 21 | +-- STRICT-HEAD premise (`head-Ω x₁ <Ω head-Ω y₁`) via |
| 22 | +-- `Ordinal.Buchholz.RankMonoUmbrellaSlice3._<ᵇ¹_` / |
| 23 | +-- `rank-pow-mono-<ᵇ¹`. |
| 24 | +-- * `<ᵇ-ψΩ≤` (boundary) closed AT THE LEX-RANK LEVEL via |
| 25 | +-- `Ordinal.Buchholz.RankLex.rank-mono-<ᵇ-ψΩ≤-lex`, NOT at the |
| 26 | +-- rank-pow level (structurally impossible per `RankAdm.agda` |
| 27 | +-- §"<ᵇ-ψΩ≤-still-open"; only available as a lex-second-component |
| 28 | +-- witness, not as a `_<′_` over `Ord`). |
| 29 | +-- * `<ᵇ-+1` at `head-Ω x₁ ≡ head-Ω y₁` (the bpsi-source-at-equality |
| 30 | +-- sub-case) GATED on the rank-lex-jb pivot (`Ordinal.Buchholz. |
| 31 | +-- RankLexJointBplus`, PR #147 scaffold): the closure requires |
| 32 | +-- the (a)+(b)+(c) assembly documented there. |
| 33 | +-- |
| 34 | +-- This module ships the deliberately-narrowed umbrella covering |
| 35 | +-- ALL CASES THAT CLOSE AT THE RANK-POW LEVEL TODAY — i.e., the |
| 36 | +-- 10 inherited cases plus the strict-head `<ᵇ-+1` case. The |
| 37 | +-- two-case shortfall (`<ᵇ-ψΩ≤` and `<ᵇ-+1` at equal-head) is |
| 38 | +-- documented in-file with explicit pointers to where each |
| 39 | +-- shortfall closes (the lex-rank level / the rank-lex-jb pivot |
| 40 | +-- scaffold) so future sessions can extend the umbrella without |
| 41 | +-- re-deriving the analysis. |
| 42 | +-- |
| 43 | +-- ## What this slice lands |
| 44 | +-- |
| 45 | +-- 1. `_<ᵇ⁻ⁿ_` — the narrowed WfCNF-restricted relation: a record |
| 46 | +-- bundling source-WfCNF, target-WfCNF, and an underlying |
| 47 | +-- `_<ᵇ¹_` derivation (NOT `_<ᵇ_` — the narrowing is exactly |
| 48 | +-- the restriction to `_<ᵇ¹_`-expressible derivations). |
| 49 | +-- 2. `mk<ᵇ⁻ⁿ` — record constructor. |
| 50 | +-- 3. `<ᵇ⁻ⁿ-from-<ᵇ⁰` — embed `_<ᵇ⁰_` derivations under |
| 51 | +-- WfCNF endpoints. |
| 52 | +-- 4. `<ᵇ⁻ⁿ-+1-+` — embed the strict-head `_<ᵇ¹_-+1-+` |
| 53 | +-- constructor under WfCNF endpoints. |
| 54 | +-- 5. `rank-pow-mono-<ᵇ⁻ⁿ` — THE NARROWED UMBRELLA. Dispatches |
| 55 | +-- via `rank-pow-mono-<ᵇ¹`. |
| 56 | +-- |
| 57 | +-- ## What this slice deliberately DOES NOT close (honest scope) |
| 58 | +-- |
| 59 | +-- Two constructor-level shortfalls remain, BOTH documented in the |
| 60 | +-- preamble of this module (and re-stated at the end of the file as |
| 61 | +-- `<ᵇ⁻ⁿ-shortfall-{lex,equal-head}` matched-negative `⊤`-aliases |
| 62 | +-- for greppability): |
| 63 | +-- |
| 64 | +-- (i) `<ᵇ-ψΩ≤` (boundary). Closes at the LEX-RANK LEVEL via |
| 65 | +-- `RankLex.rank-mono-<ᵇ-ψΩ≤-lex`; the rank-pow-level closure |
| 66 | +-- is structurally impossible under the present rank shape |
| 67 | +-- (see `RankAdm.agda` §"<ᵇ-ψΩ≤-still-open" for the analysis |
| 68 | +-- + the two design follow-up options recorded there). |
| 69 | +-- (ii) `<ᵇ-+1` at `head-Ω x₁ ≡ head-Ω y₁`. Closes at the |
| 70 | +-- ψ-rank level via `RankLexSlice3.rank-adm-bpsi-strict-at- |
| 71 | +-- equality`; the bplus-chain-level extension is GATED on |
| 72 | +-- the rank-lex-jb pivot (`RankLexJointBplus`, PR #147 |
| 73 | +-- scaffold). The (a)+(b)+(c) assembly is the next-session |
| 74 | +-- task per that module's preamble. |
| 75 | +-- |
| 76 | +-- ## Headlines (pinned in `Ordinal/Buchholz/Smoke.agda`) |
| 77 | +-- |
| 78 | +-- * `_<ᵇ⁻ⁿ_` — the narrowed relation |
| 79 | +-- * `mk<ᵇ⁻ⁿ` — record constructor |
| 80 | +-- * `<ᵇ⁻ⁿ-from-<ᵇ⁰` — embedding 10 inherited cases |
| 81 | +-- * `<ᵇ⁻ⁿ-+1-+` — embedding strict-head joint-bplus |
| 82 | +-- * `rank-pow-mono-<ᵇ⁻ⁿ` — THE NARROWED UMBRELLA |
| 83 | + |
| 84 | +module Ordinal.Buchholz.RankMonoUmbrellaSlice4 where |
| 85 | + |
| 86 | +open import Data.Unit using (⊤; tt) |
| 87 | + |
| 88 | +open import Ordinal.OmegaMarkers using (_<Ω_) |
| 89 | +open import Ordinal.Brouwer.Phase13 using (_<′_) |
| 90 | +open import Ordinal.Buchholz.Syntax using (BT; bplus) |
| 91 | +open import Ordinal.Buchholz.WellFormedCNF using (WfCNF) |
| 92 | +open import Ordinal.Buchholz.HeadOmega using (head-Ω) |
| 93 | +open import Ordinal.Buchholz.RankPow using (rank-pow) |
| 94 | +open import Ordinal.Buchholz.RankPowSlice3 using (NonBzero) |
| 95 | +open import Ordinal.Buchholz.RankMonoUmbrella using |
| 96 | + ( _<ᵇ⁰_ |
| 97 | + ) |
| 98 | +open import Ordinal.Buchholz.RankMonoUmbrellaSlice3 using |
| 99 | + ( _<ᵇ¹_ |
| 100 | + ; <ᵇ¹-from-<ᵇ⁰ |
| 101 | + ; <ᵇ¹-+1-+ |
| 102 | + ; rank-pow-mono-<ᵇ¹ |
| 103 | + ) |
| 104 | + |
| 105 | +---------------------------------------------------------------------- |
| 106 | +-- The narrowed relation `_<ᵇ⁻ⁿ_` |
| 107 | +---------------------------------------------------------------------- |
| 108 | + |
| 109 | +-- Bundles WfCNF endpoints together with a `_<ᵇ¹_` derivation. The |
| 110 | +-- narrowing IS the restriction to `_<ᵇ¹_`-expressible derivations: |
| 111 | +-- consumers handing a `_<ᵇ⁻_` record over have already proved both |
| 112 | +-- endpoints WfCNF; the additional `<ᵇ¹` (vs `<ᵇ`) restriction is |
| 113 | +-- exactly what this slice scopes itself to. |
| 114 | +-- |
| 115 | +-- The WfCNF fields are kept even though `_<ᵇ¹_`'s `<ᵇ¹-+1-+` |
| 116 | +-- constructor already carries them, because the inherited |
| 117 | +-- `<ᵇ¹-from-<ᵇ⁰` constructor does NOT carry WfCNF witnesses (the |
| 118 | +-- `_<ᵇ⁰_` relation predates the WfCNF restriction). Bundling at |
| 119 | +-- the record level lets consumers treat the WfCNF data uniformly |
| 120 | +-- across both `_<ᵇ¹_` constructor cases. |
| 121 | + |
| 122 | +record _<ᵇ⁻ⁿ_ (x y : BT) : Set where |
| 123 | + constructor mk<ᵇ⁻ⁿ |
| 124 | + field |
| 125 | + wf-x : WfCNF x |
| 126 | + wf-y : WfCNF y |
| 127 | + <ᵇ¹-d : x <ᵇ¹ y |
| 128 | + |
| 129 | +open _<ᵇ⁻ⁿ_ public |
| 130 | + |
| 131 | +infix 4 _<ᵇ⁻ⁿ_ |
| 132 | + |
| 133 | +---------------------------------------------------------------------- |
| 134 | +-- Constructor-level embeddings |
| 135 | +---------------------------------------------------------------------- |
| 136 | + |
| 137 | +-- Embed any `_<ᵇ⁰_` derivation as a narrowed `_<ᵇ⁻ⁿ_` derivation, |
| 138 | +-- once both endpoints are WfCNF. Inherits all 10 of `_<ᵇ⁰_`'s |
| 139 | +-- closed constructors at the narrowed level. |
| 140 | + |
| 141 | +<ᵇ⁻ⁿ-from-<ᵇ⁰ : ∀ {x y} |
| 142 | + → WfCNF x → WfCNF y → x <ᵇ⁰ y → x <ᵇ⁻ⁿ y |
| 143 | +<ᵇ⁻ⁿ-from-<ᵇ⁰ wf-x wf-y p = mk<ᵇ⁻ⁿ wf-x wf-y (<ᵇ¹-from-<ᵇ⁰ p) |
| 144 | + |
| 145 | +-- Embed the strict-head joint-bplus case directly. The `_<ᵇ¹_-+1-+` |
| 146 | +-- constructor's WfCNF witnesses double as the record's `wf-x` / |
| 147 | +-- `wf-y` here; we keep them inline so the embedding is a single |
| 148 | +-- pass rather than requiring callers to destructure. |
| 149 | + |
| 150 | +<ᵇ⁻ⁿ-+1-+ : ∀ {x₁ x₂ y₁ y₂} |
| 151 | + → (wf-src : WfCNF (bplus x₁ x₂)) |
| 152 | + → (wf-tgt : WfCNF (bplus y₁ y₂)) |
| 153 | + → NonBzero y₁ |
| 154 | + → head-Ω x₁ <Ω head-Ω y₁ |
| 155 | + → bplus x₁ x₂ <ᵇ⁻ⁿ bplus y₁ y₂ |
| 156 | +<ᵇ⁻ⁿ-+1-+ wf-src wf-tgt nz-y₁ strict-head = |
| 157 | + mk<ᵇ⁻ⁿ wf-src wf-tgt (<ᵇ¹-+1-+ wf-src wf-tgt nz-y₁ strict-head) |
| 158 | + |
| 159 | +---------------------------------------------------------------------- |
| 160 | +-- THE NARROWED UMBRELLA |
| 161 | +---------------------------------------------------------------------- |
| 162 | + |
| 163 | +-- The headline. Forwards directly to `rank-pow-mono-<ᵇ¹` via the |
| 164 | +-- bundled `<ᵇ¹` derivation. The WfCNF fields are unused inside |
| 165 | +-- the proof but available to consumers reasoning about the |
| 166 | +-- endpoints. |
| 167 | + |
| 168 | +rank-pow-mono-<ᵇ⁻ⁿ : ∀ {x y} → x <ᵇ⁻ⁿ y → rank-pow x <′ rank-pow y |
| 169 | +rank-pow-mono-<ᵇ⁻ⁿ {x} {y} p = rank-pow-mono-<ᵇ¹ (<ᵇ¹-d p) |
| 170 | + |
| 171 | +---------------------------------------------------------------------- |
| 172 | +-- Matched-negative shortfall markers (greppable) |
| 173 | +---------------------------------------------------------------------- |
| 174 | + |
| 175 | +-- Pin the two `_<ᵇ_`-constructor-level shortfalls as `⊤`-aliases |
| 176 | +-- so `grep <ᵇ⁻ⁿ-shortfall` discovers them. Each name includes a |
| 177 | +-- block comment pointing at exactly where the closure lives in the |
| 178 | +-- repo (when one exists at a non-`rank-pow` level) or what would |
| 179 | +-- unblock it. |
| 180 | + |
| 181 | +-- `<ᵇ-ψΩ≤` shortfall. Closes at the LEX-RANK LEVEL via |
| 182 | +-- `Ordinal.Buchholz.RankLex.rank-mono-<ᵇ-ψΩ≤-lex`; the rank-pow |
| 183 | +-- level is structurally impossible per `RankAdm.agda` |
| 184 | +-- §"<ᵇ-ψΩ≤-still-open" — `ω-rank-pow ν ⊕ rank-pow α <′ ω-rank-pow ν` |
| 185 | +-- would force the absurd `ω-rank-pow ν <′ ω-rank-pow ν` via |
| 186 | +-- `⊕-left-≤-sum`. Consumers at the rank-pow level cannot dispatch |
| 187 | +-- this case; they must lift to the lex rank. |
| 188 | + |
| 189 | +<ᵇ⁻ⁿ-shortfall-lex : ⊤ |
| 190 | +<ᵇ⁻ⁿ-shortfall-lex = tt |
| 191 | + |
| 192 | +-- `<ᵇ-+1` at `head-Ω x₁ ≡ head-Ω y₁` shortfall. Closes at the |
| 193 | +-- ψ-rank level via `Ordinal.Buchholz.RankLexSlice3.rank-adm-bpsi- |
| 194 | +-- strict-at-equality`; the bplus-chain-level extension is GATED on |
| 195 | +-- the rank-lex-jb pivot scaffolded by |
| 196 | +-- `Ordinal.Buchholz.RankLexJointBplus` (PR #147). The (a)+(b)+(c) |
| 197 | +-- assembly documented in that module's preamble is the multi-PR |
| 198 | +-- closure path. |
| 199 | + |
| 200 | +<ᵇ⁻ⁿ-shortfall-equal-head : ⊤ |
| 201 | +<ᵇ⁻ⁿ-shortfall-equal-head = tt |
0 commit comments