Skip to content

Commit 9c970e1

Browse files
hyperpolymathhyperpolymath
authored
ordinal(buchholz): Slice 3 umbrella extension — _<ᵇ¹_ with joint-bplus + strict-head dispatch (#142)
## Summary - Extends `RankMonoUmbrella._<ᵇ⁰_` (10/13 closed constructors) into a new `_<ᵇ¹_` adding a `<ᵇ¹-+1-+` constructor for the joint-bplus case where the target's left summand is itself a `bplus` (excluded by `_<ᵇ⁰_`'s atomic-target restriction). - The umbrella `rank-pow-mono-<ᵇ¹` dispatches inherited cases to `rank-pow-mono-<ᵇ⁰` (via a thin `<ᵇ¹-from-<ᵇ⁰` embedding) and the new case to Slice 3 headline `rank-mono-<ᵇ-+1-via-head-Ω` from `RankPowSlice3Headline`. - Honest scope: bpsi-source-at-equality sub-case (ν = head-Ω y₁) is DOCUMENTED AS GATED pending a `<ᵇ-+1`-specific rank-lex primitive (the existing `RankLex.rank-mono-<ᵇ-ψΩ≤-lex` only discharges `<ᵇ-ψΩ≤`). ## Files - New: `proofs/agda/Ordinal/Buchholz/RankMonoUmbrellaSlice3.agda` (114 lines). - Wired: `proofs/agda/All.agda` (1 line, adjacent to `RankMonoUmbrella`). - Pinned: `proofs/agda/Ordinal/Buchholz/Smoke.agda` (own `using` block per CLAUDE.md "Working rules"). Headlines pinned: `_<ᵇ¹_`, `<ᵇ¹-from-<ᵇ⁰`, `<ᵇ¹-+1-+`, `rank-pow-mono-<ᵇ¹`. ## Discipline - `--safe --without-K` throughout; no postulates, no funext. - New module compiles standalone; `All.agda` + top-level `Smoke.agda` + `Ordinal/Buchholz/Smoke.agda` all exit 0. - `bash scripts/kernel-guard.sh` PASS. ## Test plan - [x] `agda -i proofs/agda proofs/agda/Ordinal/Buchholz/RankMonoUmbrellaSlice3.agda` exits 0 - [x] `agda -i proofs/agda proofs/agda/Ordinal/Buchholz/Smoke.agda` exits 0 - [x] `agda -i proofs/agda proofs/agda/Smoke.agda` exits 0 - [x] `agda -i proofs/agda proofs/agda/All.agda` exits 0 - [x] `bash scripts/kernel-guard.sh` PASS ## Forward path When a `<ᵇ-+1`-specific rank-lex primitive lands (Route A from `RankPowSlice3` design note), add a second constructor (e.g., `<ᵇ¹-+1-+-eq`) carrying the rank-lex witness for the equality sub-case and extend `rank-pow-mono-<ᵇ¹` to dispatch on it. The current ship covers the strict-head subset cleanly without overclaim.
2 parents 4b265d1 + 76c8a3d commit 9c970e1

3 files changed

Lines changed: 133 additions & 0 deletions

File tree

‎proofs/agda/All.agda‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -140,6 +140,7 @@ open import Ordinal.Buchholz.RankPowDomination
140140
open import Ordinal.Buchholz.RankPowSlice3
141141
open import Ordinal.Buchholz.RankPowSlice3Headline
142142
open import Ordinal.Buchholz.RankMonoUmbrella
143+
open import Ordinal.Buchholz.RankMonoUmbrellaSlice3
143144
open import Ordinal.Buchholz.RecursiveSurfaceOrder
144145
open import Ordinal.Buchholz.RecursiveSurfaceBudget
145146
open import Ordinal.Buchholz.SurfaceOrder

‎proofs/agda/Ordinal/Buchholz/RankMonoUmbrellaSlice3.agda‎

Lines changed: 114 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,114 @@
1+
{-# OPTIONS --safe --without-K #-}
2+
3+
-- The Slice-3 extension of the rank-soundness-ready umbrella.
4+
--
5+
-- `Ordinal.Buchholz.RankMonoUmbrella._<ᵇ⁰_` closes 10 of the 13
6+
-- constructors of `Ordinal.Buchholz.Order._<ᵇ_` via direct structural
7+
-- recursion. The bplus-target joint-bplus case (where the target's
8+
-- left summand is itself a `bplus`, NOT atomic — i.e., `<ᵇ-+1` with
9+
-- both `x₁` and `y₁` being `bplus`) is excluded from `_<ᵇ⁰_`
10+
-- because the `<ᵇ⁰-+1-Ω` / `<ᵇ⁰-+1-ψ` constructors restrict the
11+
-- target's left summand to be `bOmega μ` / `bpsi ν α`.
12+
--
13+
-- This slice extends the umbrella with a NEW joint-bplus constructor
14+
-- `<ᵇ¹-+1-+` and dispatches it via the Slice 3 headline
15+
-- `rank-mono-<ᵇ-+1-via-head-Ω` from `Ordinal.Buchholz.RankPowSlice3Headline`.
16+
-- That headline closes the bplus-target case UNDER A STRICT-HEAD
17+
-- PREMISE `head-Ω x₁ <Ω head-Ω y₁`. The new constructor bakes the
18+
-- premise (together with the required WfCNF / NonBzero side
19+
-- conditions) in.
20+
--
21+
-- ## What's in / what's out
22+
--
23+
-- IN (11 = 10 inherited + 1 new):
24+
--
25+
-- * `<ᵇ¹-from-<ᵇ⁰` — embedding of every `_<ᵇ⁰_` derivation as a
26+
-- `_<ᵇ¹_` derivation (single constructor; the umbrella below
27+
-- dispatches via `rank-pow-mono-<ᵇ⁰` directly).
28+
-- * `<ᵇ¹-+1-+` — the new joint-bplus constructor: requires
29+
-- `WfCNF (bplus x₁ x₂)`, `WfCNF (bplus y₁ y₂)`, `NonBzero y₁`,
30+
-- and the strict-head premise `head-Ω x₁ <Ω head-Ω y₁`.
31+
--
32+
-- OUT (deliberately deferred, see "Equality sub-case" below):
33+
--
34+
-- * Joint-bplus at `head-Ω x₁ ≡ head-Ω y₁` — the bpsi-source-at-
35+
-- equality sub-case where x₁'s leading marker matches y₁'s.
36+
-- The Slice 3 headline cannot fire (it needs strict `<Ω`); a
37+
-- rank-adm / rank-lex combination would close it but no such
38+
-- primitive currently exists for `<ᵇ-+1` (`rank-lex` only
39+
-- discharges `<ᵇ-ψΩ≤`). When that primitive lands, add a
40+
-- second constructor (e.g., `<ᵇ¹-+1-+-eq`) carrying the rank-lex
41+
-- witness and extend `rank-pow-mono-<ᵇ¹` to dispatch on it.
42+
--
43+
-- ## Why a thin embedding constructor
44+
--
45+
-- The natural shape would inline all 10 constructors of `_<ᵇ⁰_` into
46+
-- `_<ᵇ¹_`. That would duplicate `_<ᵇ⁰_`'s definition and force the
47+
-- umbrella's structural recursion to redo the dispatch for every
48+
-- inherited case. Embedding via `<ᵇ¹-from-<ᵇ⁰` keeps `_<ᵇ¹_`
49+
-- minimal (two constructors), preserves the existing umbrella as the
50+
-- inherited workhorse, and adds the new case as a single targeted
51+
-- extension.
52+
--
53+
-- ## Headlines (pinned in `Ordinal/Buchholz/Smoke.agda`)
54+
--
55+
-- * `_<ᵇ¹_` -- the extended relation
56+
-- * `<ᵇ¹-from-<ᵇ⁰` -- the embedding constructor
57+
-- * `<ᵇ¹-+1-+` -- the new joint-bplus constructor
58+
-- * `rank-pow-mono-<ᵇ¹` -- THE UMBRELLA (strict)
59+
60+
module Ordinal.Buchholz.RankMonoUmbrellaSlice3 where
61+
62+
open import Ordinal.OmegaMarkers using (_<Ω_)
63+
open import Ordinal.Buchholz.Syntax using (BT; bplus)
64+
open import Ordinal.Buchholz.WellFormedCNF using (WfCNF)
65+
open import Ordinal.Buchholz.HeadOmega using (head-Ω)
66+
open import Ordinal.Buchholz.RankPow using (rank-pow)
67+
open import Ordinal.Brouwer.Phase13 using (_<′_)
68+
open import Ordinal.Buchholz.RankPowSlice3 using (NonBzero)
69+
open import Ordinal.Buchholz.RankPowSlice3Headline using
70+
( rank-mono-<ᵇ-+1-via-head-Ω
71+
)
72+
open import Ordinal.Buchholz.RankMonoUmbrella using
73+
( _<ᵇ⁰_
74+
; rank-pow-mono-<ᵇ⁰
75+
)
76+
77+
----------------------------------------------------------------------
78+
-- The extended relation `_<ᵇ¹_`
79+
----------------------------------------------------------------------
80+
81+
-- Two constructors:
82+
--
83+
-- 1. `<ᵇ¹-from-<ᵇ⁰` — every `_<ᵇ⁰_` derivation is a `_<ᵇ¹_`
84+
-- derivation. Inherits all 10 closed constructors of `_<ᵇ⁰_`
85+
-- without duplication.
86+
-- 2. `<ᵇ¹-+1-+` — the new joint-bplus case with target's left
87+
-- summand itself a `bplus`. Carries the strict-head premise
88+
-- and WfCNF / NonBzero side conditions required by the
89+
-- Slice 3 headline.
90+
91+
data _<ᵇ¹_ : BT → BT → Set where
92+
<ᵇ¹-from-<ᵇ⁰ : ∀ {x y} → x <ᵇ⁰ y → x <ᵇ¹ y
93+
94+
<ᵇ¹-+1-+ : ∀ {x₁ x₂ y₁ y₂}
95+
→ WfCNF (bplus x₁ x₂)
96+
→ WfCNF (bplus y₁ y₂)
97+
→ NonBzero y₁
98+
→ head-Ω x₁ <Ω head-Ω y₁
99+
→ bplus x₁ x₂ <ᵇ¹ bplus y₁ y₂
100+
101+
infix 4 _<ᵇ¹_
102+
103+
----------------------------------------------------------------------
104+
-- The extended umbrella theorem
105+
----------------------------------------------------------------------
106+
107+
-- Direct structural recursion on `_<ᵇ¹_`. The inherited case
108+
-- forwards to `rank-pow-mono-<ᵇ⁰`; the new joint-bplus case forwards
109+
-- to the Slice 3 headline `rank-mono-<ᵇ-+1-via-head-Ω`.
110+
111+
rank-pow-mono-<ᵇ¹ : ∀ {x y} → x <ᵇ¹ y → rank-pow x <′ rank-pow y
112+
rank-pow-mono-<ᵇ¹ (<ᵇ¹-from-<ᵇ⁰ p) = rank-pow-mono-<ᵇ⁰ p
113+
rank-pow-mono-<ᵇ¹ (<ᵇ¹-+1-+ wf-src wf-tgt nz-y₁ strict-head) =
114+
rank-mono-<ᵇ-+1-via-head-Ω wf-src wf-tgt nz-y₁ strict-head

‎proofs/agda/Ordinal/Buchholz/Smoke.agda‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -479,3 +479,21 @@ open import Ordinal.Buchholz.RankPowSlice3 using
479479
open import Ordinal.Buchholz.RankPowSlice3Headline using
480480
( rank-mono-<ᵇ-+1-via-head-Ω
481481
)
482+
483+
-- Slice 3 umbrella extension (own block per CLAUDE.md Working
484+
-- rules): the new `_<ᵇ¹_` relation extends `_<ᵇ⁰_` with a
485+
-- joint-bplus constructor `<ᵇ¹-+1-+` carrying the strict-head
486+
-- premise `head-Ω x₁ <Ω head-Ω y₁` plus WfCNF / NonBzero side
487+
-- conditions. The umbrella `rank-pow-mono-<ᵇ¹` forwards the
488+
-- inherited cases to `rank-pow-mono-<ᵇ⁰` and the new case to
489+
-- the Slice 3 headline `rank-mono-<ᵇ-+1-via-head-Ω`. The
490+
-- bpsi-source-at-equality sub-case is documented as gated:
491+
-- it requires a `<ᵇ-+1`-specific rank-lex primitive not yet
492+
-- in the repo (the existing `RankLex.rank-mono-<ᵇ-ψΩ≤-lex`
493+
-- discharges `<ᵇ-ψΩ≤`, not `<ᵇ-+1`).
494+
open import Ordinal.Buchholz.RankMonoUmbrellaSlice3 using
495+
( _<ᵇ¹_
496+
; <ᵇ¹-from-<ᵇ⁰
497+
; <ᵇ¹-+1-+
498+
; rank-pow-mono-<ᵇ¹
499+
)

0 commit comments

Comments
 (0)