Skip to content

Commit dda085a

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
ordinal(buchholz): Slice 3 headline — rank-mono-<ᵇ-+1-via-head-Ω under strict-head premise
Closes the joint-bplus rank-mono case for `_<ᵇ-+1_` headline-level via Route A from RankPowSlice3's design note. The headline takes the strict-head premise `head-Ω x₁ <Ω head-Ω y₁` as an external hypothesis; the caller (the umbrella's case-split on `x₁ <ᵇ y₁`) decides where to source it: * x₁ = bOmega μ: `head-Ω-inv-bOmega` is strict, applies directly. * x₁ = bpsi ν α at strict `ν <Ω head-Ω y₁`: `head-Ω-inv-bpsi` upgraded via strictness witness (when not the `<ᵇ-ψΩ≤` constructor). * x₁ = bpsi ν α at equality `ν ≡ head-Ω y₁`: caller dispatches to `rank-mono-<ᵇ-ψΩ≤-lex` (rank-lex second-component) instead of this headline. * x₁ = bplus a b: `head-Ω (bplus a b) = head-Ω a` (definitional), recurse on the leftmost-leaf. ## What this lands New module `Ordinal.Buchholz.RankPowSlice3Headline`: * `rank-mono-<ᵇ-+1-via-head-Ω : ∀ {x₁ x₂ y₁ y₂} → WfCNF (bplus x₁ x₂) → WfCNF (bplus y₁ y₂) → NonBzero y₁ → head-Ω x₁ <Ω head-Ω y₁ → rank-pow (bplus x₁ x₂) <′ rank-pow (bplus y₁ y₂)` The proof composes the four Slice 3 prerequisites in a chain (no structural recursion; the recursion is already discharged by `rank-pow-dominated-by-head-Ω` on the source's WfCNF): 1. rank-pow source <′ ω-rank-pow-succ (head-Ω x₁) — Slice 2-bplus (`rank-pow-dominated-by-head-Ω`) + head-Ω-bplus. 2. ω-rank-pow-succ (head-Ω x₁) ≤′ ω-rank-pow (head-Ω y₁) — `ω-rank-pow-succ-≤-via-<Ω` (the strict-jump bridge). 3. ω-rank-pow (head-Ω y₁) ≤′ rank-pow y₁ — `head-Ω-lower-bound`. 4. rank-pow y₁ ≤′ rank-pow (bplus y₁ y₂) — `⊕-left-≤-sum`. All four compose via `≤′-trans` (recall `α <′ β = osuc α ≤′ β`). Wired into `proofs/agda/All.agda` adjacent to `RankPowSlice3`, pinned in `Ordinal/Buchholz/Smoke.agda` under its own `using` block. ## What this does NOT discharge The bpsi-source-at-equality (`ν = head-Ω y₁`) case still requires a rank-adm / rank-lex combination. This module makes the headline AVAILABLE for the strict-head cases; the umbrella's case-split is the remaining wiring (a separate follow-on slice). ## Build invariant * `Ordinal/Buchholz/Smoke.agda` exits 0 under `--safe --without-K`, zero postulates. * `RankPowSlice3Headline.agda` compiles standalone same flags. * `scripts/kernel-guard.sh` PASS. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 0826e52 commit dda085a

3 files changed

Lines changed: 170 additions & 0 deletions

File tree

‎proofs/agda/All.agda‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -138,6 +138,7 @@ open import Ordinal.Buchholz.HeadOmega
138138
open import Ordinal.Buchholz.HeadOmegaInversion
139139
open import Ordinal.Buchholz.RankPowDomination
140140
open import Ordinal.Buchholz.RankPowSlice3
141+
open import Ordinal.Buchholz.RankPowSlice3Headline
141142
open import Ordinal.Buchholz.RankMonoUmbrella
142143
open import Ordinal.Buchholz.RecursiveSurfaceOrder
143144
open import Ordinal.Buchholz.RecursiveSurfaceBudget

‎proofs/agda/Ordinal/Buchholz/RankPowSlice3Headline.agda‎

Lines changed: 155 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,155 @@
1+
{-# OPTIONS --safe --without-K #-}
2+
3+
-- Slice 3 headline of the head-Ω route — `rank-mono-<ᵇ-+1-via-head-Ω`.
4+
--
5+
-- Closes the joint-bplus rank-mono case for `_<ᵇ-+1_` UNDER A
6+
-- STRICT-HEAD PREMISE supplied externally. The premise
7+
-- `head-Ω x₁ <Ω head-Ω y₁` lets the chain go through cleanly via
8+
-- the Slice 3 prerequisites that landed in `RankPowSlice3`:
9+
--
10+
-- rank-pow (bplus x₁ x₂)
11+
-- <′ ω-rank-pow-succ (head-Ω x₁) -- rank-pow-dominated-by-head-Ω
12+
-- -- + head-Ω-bplus (= head-Ω x₁)
13+
-- ≤′ ω-rank-pow (head-Ω y₁) -- ω-rank-pow-succ-≤-via-<Ω
14+
-- -- (strict-head premise)
15+
-- ≤′ rank-pow y₁ -- head-Ω-lower-bound
16+
-- ≤′ rank-pow (bplus y₁ y₂) -- ⊕-left-≤-sum
17+
--
18+
-- The strict-head premise is the BURDEN this primitive bumps up to
19+
-- the caller (Route A from `RankPowSlice3`'s design note). The
20+
-- caller — typically an extended `_<ᵇ¹_` umbrella with a new
21+
-- joint-bplus constructor — derives it from:
22+
--
23+
-- * x₁ = bOmega μ: `head-Ω-inv-bOmega` gives `μ <Ω head-Ω y₁`
24+
-- directly (strict for all three `<ᵇ-Ω_`
25+
-- constructors).
26+
-- * x₁ = bpsi ν α: `head-Ω-inv-bpsi` gives only `ν ≤Ω head-Ω y₁`
27+
-- (non-strict; `<ᵇ-ψΩ≤` permits equal markers).
28+
-- The strict jump must come from rank-adm /
29+
-- rank-lex second-component info (Route A
30+
-- combination). When `ν = head-Ω y₁`, the
31+
-- caller dispatches to `rank-mono-<ᵇ-ψΩ≤-lex`
32+
-- instead of this headline; otherwise (strict
33+
-- ν <Ω head-Ω y₁) this headline applies.
34+
-- * x₁ = bplus a b: `head-Ω (bplus a b) = head-Ω a`; recurse on
35+
-- the leftmost-leaf shape.
36+
--
37+
-- ## What this lands
38+
--
39+
-- * `rank-mono-<ᵇ-+1-via-head-Ω` — the headline, parametric in
40+
-- the strict-head premise.
41+
--
42+
-- ## What this does NOT discharge
43+
--
44+
-- The bpsi-source-at-equality (`ν = head-Ω y₁`) case still requires
45+
-- a rank-adm / rank-lex combination. This module makes the headline
46+
-- AVAILABLE for the strict-head cases; the umbrella's case-split is
47+
-- where the caller decides which discharge to use.
48+
--
49+
-- ## Headlines (pin in `Ordinal/Buchholz/Smoke.agda`)
50+
--
51+
-- * `rank-mono-<ᵇ-+1-via-head-Ω`
52+
53+
module Ordinal.Buchholz.RankPowSlice3Headline where
54+
55+
open import Ordinal.Brouwer using (Ord; osuc)
56+
open import Ordinal.Brouwer.Phase13 using
57+
( _≤′_
58+
; _<′_
59+
; ≤′-trans
60+
; osuc-mono-≤′
61+
; ⊕-left-≤-sum
62+
)
63+
open import Ordinal.OmegaMarkers using (_<Ω_)
64+
open import Ordinal.Buchholz.Syntax using (BT; bplus)
65+
open import Ordinal.Buchholz.WellFormedCNF using
66+
( WfCNF
67+
; wf-cnf-bplus
68+
)
69+
open import Ordinal.Buchholz.HeadOmega using (head-Ω)
70+
open import Ordinal.Buchholz.RankPow using
71+
( rank-pow
72+
; ω-rank-pow
73+
; ω-rank-pow-succ
74+
)
75+
open import Ordinal.Buchholz.RankPowDomination using
76+
( rank-pow-dominated-by-head-Ω
77+
)
78+
open import Ordinal.Buchholz.RankPowSlice3 using
79+
( NonBzero
80+
; ω-rank-pow-succ-≤-via-<Ω
81+
; head-Ω-lower-bound
82+
)
83+
84+
----------------------------------------------------------------------
85+
-- The Slice 3 headline
86+
----------------------------------------------------------------------
87+
88+
-- For `bplus x₁ x₂ <ᵇ bplus y₁ y₂` from `x₁ <ᵇ y₁` (the `<ᵇ-+1`
89+
-- constructor's source-strict case), the rank-mono conclusion
90+
-- holds UNDER a strict-head premise on the source's and target's
91+
-- leading Ω-markers.
92+
--
93+
-- The strict-head premise `head-Ω x₁ <Ω head-Ω y₁` is what the
94+
-- caller's case-split on `x₁ <ᵇ y₁` provides. By head-Ω-bplus,
95+
-- `head-Ω (bplus x₁ x₂) = head-Ω x₁` (the source's leading marker
96+
-- — definitional), so the strict-head step buys exactly the room
97+
-- needed to fit the source under the target's `ω-rank-pow (head-Ω
98+
-- y₁)` lower bound.
99+
--
100+
-- The chain (composing the prerequisites; no structural recursion):
101+
-- 1. `rank-pow (bplus x₁ x₂) <′ ω-rank-pow-succ (head-Ω x₁)` —
102+
-- Slice 2-bplus (`rank-pow-dominated-by-head-Ω`); `head-Ω
103+
-- (bplus x₁ x₂) = head-Ω x₁` definitionally.
104+
-- 2. `ω-rank-pow-succ (head-Ω x₁) ≤′ ω-rank-pow (head-Ω y₁)` —
105+
-- strict-jump bridge (`ω-rank-pow-succ-≤-via-<Ω`) applied to
106+
-- the strict-head premise.
107+
-- 3. `ω-rank-pow (head-Ω y₁) ≤′ rank-pow y₁` — head-Ω lower
108+
-- bound (`head-Ω-lower-bound`) under WfCNF y₁ + NonBzero y₁.
109+
-- 4. `rank-pow y₁ ≤′ rank-pow (bplus y₁ y₂) = rank-pow y₁ ⊕
110+
-- rank-pow y₂` — `⊕-left-≤-sum`.
111+
--
112+
-- All four steps compose via `≤′-trans` (recall `α <′ β` is just
113+
-- `osuc α ≤′ β`, so the chain stays within `≤′` after the first
114+
-- step's `osuc` shift).
115+
116+
rank-mono-<ᵇ-+1-via-head-Ω : ∀ {x₁ x₂ y₁ y₂}
117+
→ WfCNF (bplus x₁ x₂)
118+
→ WfCNF (bplus y₁ y₂)
119+
→ NonBzero y₁
120+
→ head-Ω x₁ <Ω head-Ω y₁
121+
→ rank-pow (bplus x₁ x₂) <′ rank-pow (bplus y₁ y₂)
122+
rank-mono-<ᵇ-+1-via-head-Ω
123+
{x₁} {x₂} {y₁} {y₂}
124+
wf-src
125+
(wf-cnf-bplus wf-y₁ _ _ _)
126+
nz-y₁
127+
strict-head
128+
=
129+
-- Step 1: rank-pow source <′ ω-rank-pow-succ (head-Ω source) =
130+
-- (definitionally) ω-rank-pow-succ (head-Ω x₁) by head-Ω-bplus.
131+
-- Concretely: `α <′ β = osuc α ≤′ β`, so the conclusion is
132+
-- `osuc (rank-pow (bplus x₁ x₂)) ≤′ rank-pow (bplus y₁ y₂)`.
133+
--
134+
-- The chain in `≤′` form:
135+
-- osuc (rank-pow (bplus x₁ x₂))
136+
-- ≤′ ω-rank-pow-succ (head-Ω x₁) -- step 1 (rank-pow-dominated-...)
137+
-- ≤′ ω-rank-pow (head-Ω y₁) -- step 2 (ω-rank-pow-succ-≤-via-<Ω)
138+
-- ≤′ rank-pow y₁ -- step 3 (head-Ω-lower-bound)
139+
-- ≤′ rank-pow (bplus y₁ y₂) -- step 4 (⊕-left-≤-sum)
140+
≤′-trans
141+
{osuc (rank-pow (bplus x₁ x₂))}
142+
{ω-rank-pow (head-Ω y₁)}
143+
{rank-pow (bplus y₁ y₂)}
144+
(≤′-trans
145+
{osuc (rank-pow (bplus x₁ x₂))}
146+
{ω-rank-pow-succ (head-Ω x₁)}
147+
{ω-rank-pow (head-Ω y₁)}
148+
(rank-pow-dominated-by-head-Ω wf-src)
149+
(ω-rank-pow-succ-≤-via-<Ω strict-head))
150+
(≤′-trans
151+
{ω-rank-pow (head-Ω y₁)}
152+
{rank-pow y₁}
153+
{rank-pow (bplus y₁ y₂)}
154+
(head-Ω-lower-bound wf-y₁ nz-y₁)
155+
(⊕-left-≤-sum {rank-pow y₁} (rank-pow y₂)))

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

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -465,3 +465,17 @@ open import Ordinal.Buchholz.RankPowSlice3 using
465465
; ω-rank-pow-succ-≤-via-<Ω
466466
; head-Ω-lower-bound
467467
)
468+
469+
-- Slice 3 headline (own block per CLAUDE.md Working rules): closes
470+
-- the joint-bplus rank-mono case for `_<ᵇ-+1_` under a strict-head
471+
-- premise `head-Ω x₁ <Ω head-Ω y₁`. The premise is the burden
472+
-- this primitive bumps up to the caller (the umbrella's case-split
473+
-- on `x₁ <ᵇ y₁`); for x₁ = bOmega it discharges via
474+
-- `head-Ω-inv-bOmega` directly, for x₁ = bpsi at strict ν<Ω head-Ω y₁
475+
-- via `head-Ω-inv-bpsi` + `<Ω→` upgrade, for x₁ = bpsi at equality
476+
-- via rank-adm / rank-lex combination (Route A from the design
477+
-- note in `RankPowSlice3`). The Slice 3 closure is now headline-
478+
-- level; the umbrella's case-split is the remaining wiring.
479+
open import Ordinal.Buchholz.RankPowSlice3Headline using
480+
( rank-mono-<ᵇ-+1-via-head-Ω
481+
)

0 commit comments

Comments
 (0)