ordinal(buchholz): Slice 2-omega — ω branch of ω-rank-pow-succ replaced + dominance proved

Replaces the originally-proposed `ω-rank-pow-succ ω = olim (λ n →
ω^(suc(suc n)))` (equi-ordinal with `ω-rank-pow ω`, so unsound) with
`olim (λ n → ω-rank-pow ω ·ℕ n)`, denoting `ω^(ω+1)` — the next
additive-principal above `ω^ω`.

Proves `ω-rank-pow-<-succ-omega : ω-rank-pow ω <′ ω-rank-pow-succ ω`
by mirroring `Brouwer/OmegaPow.ω^-strict-mono-suc`: pick branch index
2 in the target limit, reduce to `osuc (ω-rank-pow ω) ≤′ (oz ⊕
ω-rank-pow ω) ⊕ ω-rank-pow ω`, chain `X≤′oz⊕X` with
`⊕-mono-<-right (ω-rank-pow-pos ω)`.

Cross-check (iii) from the obstruction note resolved: the proof goes
through `X≤′oz⊕X` which provides exactly the propositional
`X ≤′ oz ⊕ X` step the note flagged as the hazard.  Cross-checks (i)
and (ii) still stand without modification — the consumer (Slice 3)
uses the existing `additive-principal-ω-rank-pow {head-Ω target}` for
additive-principal closure, not any property of `ω-rank-pow-succ ω`
itself.

New lemmas (all pinned in `Ordinal/Buchholz/Smoke.agda` under the
existing Slice 2 `using` block):

  * ω-rank-pow-succ-omega    -- definitional sanity, ω branch
  * ω-rank-pow-<-succ-omega  -- per-marker strict dominance, ω branch
  * ω-rank-pow-<-succ        -- unified across both branches

The obstruction-note comment block in `RankPow.agda` is updated:
its "ω branch deferred" subsection moves to a "History note" form
recording the original sketch's failure mode, and the closure-plan
TODO list collapses from two entries to one (Slice 2-bplus, the full
WfCNF-carrier domination lemma — both per-marker dominances + the
HeadOmegaInversion option (b) lemmas are now landed, so Slice 2-bplus
no longer carries any inversion-via-rank-mono dependency).

`scripts/kernel-guard.sh`: PASS.  No postulates introduced.
--safe --without-K throughout.

https://claude.ai/code/session_013nLEeKZXpvHnrDZMgRm19S

Author: claude

proofs/agda/Ordinal/Buchholz/RankPow.agda

@@ -73,6 +73,8 @@ open import Ordinal.Brouwer.OmegaPow              using
   ; ω^_-pos
   ; ω^-strict-mono
   ; ω^-strict-mono-suc
+  ; _·ℕ_
+  ; X≤′oz⊕X
   )
 open import Ordinal.Buchholz.Syntax               using
   ( BT
@@ -429,31 +431,32 @@ rank-mono-<ᵇ-+1-ψ-target {x₁} {x₂} {ν} {α} {y₂} =
 -- `ω-rank-pow-succ : OmegaIndex → Ord` consumed by the planned (but
 -- not yet landed) `<ᵇ-+1` joint-bplus head-Ω domination route.
 --
--- ## Scope of this slice
+-- ## Scope of this slice (as updated by Slice 2-omega closure)
 --
 -- Lands:
 --   * `ω-rank-pow-succ : OmegaIndex → Ord`
 --   * `ω-rank-pow-succ-fin` — definitional sanity, fin branch
---   * `ω-rank-pow-<-succ-fin` — per-marker strict dominance at fin
+--   * `ω-rank-pow-succ-omega` — definitional sanity, ω branch
+--   * `ω-rank-pow-<-succ-fin`   — per-marker strict dominance, fin
+--   * `ω-rank-pow-<-succ-omega` — per-marker strict dominance, ω
+--   * `ω-rank-pow-<-succ`       — unified across both branches
 --   * `rank-pow-bOmega-via-head-Ω`,
 --     `rank-pow-bpsi-via-head-Ω` — atomic-rank `refl`-shape primitives
 --     factoring `rank-pow` through `head-Ω` for the two non-bplus,
 --     non-bzero `BT` constructors.  Useful at consumer-recursion
 --     sites that want to rewrite source-rank into head-Ω form
 --     without unfolding `rank-pow` and `head-Ω` separately.
 --
--- Deferred (with concrete obstructions documented inline below):
+-- Still deferred:
 --   * The headline domination lemma
 --     `rank-pow-dominated-by-head-Ω : (t : BT) → NonBzero t →
 --       WfCNF t → rank-pow t <′ ω-rank-pow-succ (head-Ω t)`
---     in its full generality.  The fin branch is structurally clean
---     (every WfCNF clause discharges via additive-principal at
---     ω^(suc(suc n)) and the existing per-constructor rank-mono
---     primitives), but the **ω branch of `head-Ω` cannot strictly
---     dominate under the originally-proposed `ω-rank-pow-succ ω` shape**.
---     See the obstruction note immediately below.
+--     in its full generality.  Both per-marker dominances now hold;
+--     the structural recursion on the WfCNF carrier (the bplus case
+--     in particular) is Slice 2-bplus.  See the `TODO(slice-2-bplus)`
+--     marker further down.
 --
--- ## Obstruction note for the ω branch
+-- ## History note: the original ω-branch obstruction
 --
 -- The originally proposed shape (per CLAUDE.md § "Session arc
 -- 2026-05-27 late evening" — Slice 2 sketch) was:
@@ -470,40 +473,77 @@ rank-mono-<ᵇ-+1-ψ-target {x₁} {x₂} {ν} {α} {y₂} =
 -- ≤′ ω^(suc(suc k)) ·ℕ j` obligation that is again a limit-vs-osuc
 -- comparison, recursing indefinitely.
 --
--- A follow-on slice must replace the ω branch with a genuinely
--- strictly-larger ordinal (the natural candidate is `ω^(ω+1)`, the
--- next additive-principal above `ω^ω`).  In Brouwer notation this
--- would be `olim (λ n → (ω-rank-pow ω) ·ℕ n)`; the proof obligation
--- shifts but does not vanish — `(ω-rank-pow ω) ·ℕ n` is itself a
--- nested limit, and the strict-dominance proof needs the equivalent of
--- the existing `additive-principal-ω-rank-pow` ω-branch closure
--- (lines 238–255 above) lifted one ω-power.
+-- Slice 2-omega (this slice) replaces the ω branch with the
+-- documented candidate `olim (λ n → ω-rank-pow ω ·ℕ n)`, denoting
+-- `ω^(ω+1) = ω^ω · ω` — the next additive-principal above `ω^ω`.
+-- The strict-dominance proof at the ω branch mirrors
+-- `Brouwer/OmegaPow.ω^-strict-mono-suc` (line 204): pick branch
+-- index 2 in the target limit, reduce to a `osuc (ω-rank-pow ω) ≤′
+-- (oz ⊕ ω-rank-pow ω) ⊕ ω-rank-pow ω` obligation, chain
+-- `X≤′oz⊕X` with `⊕-mono-<-right (ω-rank-pow-pos ω)`.
 --
--- Choosing not to make that replacement in this slice keeps the
--- abstraction minimal and avoids committing to a shape that the
--- consumer (Slice 3, `rank-mono-<ᵇ-+1-via-head-Ω`) might want to
--- specialise differently.  The ω branch of `ω-rank-pow-succ` below
--- therefore reuses the **original** CLAUDE.md proposal verbatim, so
--- the abstraction is in place for follow-on slices to inspect and
--- (if needed) override before any consumer pulls on the ω case.
+-- Sanity check (iii) from the original obstruction note — that the
+-- leading `oz ⊕` in `(ω-rank-pow ω) ·ℕ 1` is NOT definitionally
+-- `ω-rank-pow ω` — was the hazard to verify; the proof goes through
+-- via `X≤′oz⊕X` which proves exactly the propositional `X ≤′ oz ⊕ X`
+-- the obstruction note flagged as needed.  Cross-checks (i) and (ii)
+-- from that note still stand: the consumer (Slice 3) uses the existing
+-- `additive-principal-ω-rank-pow {head-Ω target}` for additive-principal
+-- closure, not any property of `ω-rank-pow-succ ω` itself.
 
 ω-rank-pow-succ : OmegaIndex → Ord
 ω-rank-pow-succ (fin n) = ω^ (suc (suc n))
-ω-rank-pow-succ ω       = olim (λ n → ω^ (suc (suc n)))
+ω-rank-pow-succ ω       = olim (λ n → ω-rank-pow ω ·ℕ n)
 
 -- Definitional sanity at the fin branch.  Mirrors `ω-rank-pow-fin`.
 ω-rank-pow-succ-fin : ∀ n → ω-rank-pow-succ (fin n) ≡ ω^ (suc (suc n))
 ω-rank-pow-succ-fin _ = refl
 
+-- Definitional sanity at the ω branch (post Slice 2-omega).  Mirrors
+-- `ω-rank-pow-succ-fin`.  Records the shape change from the
+-- originally-proposed `olim (λ n → ω^(suc(suc n)))` to
+-- `olim (λ n → ω-rank-pow ω ·ℕ n)`, which denotes `ω^(ω+1)` and is
+-- strictly above `ω-rank-pow ω = ω^ω`.
+ω-rank-pow-succ-omega : ω-rank-pow-succ ω ≡ olim (λ n → ω-rank-pow ω ·ℕ n)
+ω-rank-pow-succ-omega = refl
+
 -- Per-marker strict dominance at the fin branch.  For each `fin n`,
 -- `ω-rank-pow (fin n) = ω^(suc n)` is strictly below
 -- `ω-rank-pow-succ (fin n) = ω^(suc(suc n))` via the one-step
--- strict-mono of the ω-power ladder.  The ω branch is deferred per the
--- obstruction note above.
+-- strict-mono of the ω-power ladder.
 ω-rank-pow-<-succ-fin : ∀ n
   → ω-rank-pow (fin n) <′ ω-rank-pow-succ (fin n)
 ω-rank-pow-<-succ-fin n = ω^-strict-mono-suc (suc n)
 
+-- Per-marker strict dominance at the ω branch.  Mirrors the
+-- `ω^-strict-mono-suc` proof at line 204 of `Brouwer/OmegaPow.agda`:
+-- pick branch index 2 in the target limit; reduce the obligation to
+-- `osuc (ω-rank-pow ω) ≤′ (oz ⊕ ω-rank-pow ω) ⊕ ω-rank-pow ω`; chain
+-- `X≤′oz⊕X` (the `osuc/osuc` clause of `_≤′_` makes this fill the
+-- LHS step) with `⊕-mono-<-right (ω-rank-pow-pos ω)` (after right-unit
+-- `α ⊕ oz = α` reduction).  Closes Slice 2-omega per the obstruction
+-- note above.
+ω-rank-pow-<-succ-omega : ω-rank-pow ω <′ ω-rank-pow-succ ω
+ω-rank-pow-<-succ-omega = 2 , step
+  where
+  step : osuc (ω-rank-pow ω) ≤′ (oz ⊕ ω-rank-pow ω) ⊕ ω-rank-pow ω
+  step =
+    ≤′-trans
+      {osuc (ω-rank-pow ω)}
+      {osuc (oz ⊕ ω-rank-pow ω)}
+      {(oz ⊕ ω-rank-pow ω) ⊕ ω-rank-pow ω}
+      (X≤′oz⊕X {ω-rank-pow ω})
+      (⊕-mono-<-right {oz ⊕ ω-rank-pow ω} {oz} {ω-rank-pow ω}
+        (ω-rank-pow-pos ω))
+
+-- Unified strict-dominance lemma across both Ω-marker branches.
+-- Consumers wanting the per-branch versions still have them under
+-- `-fin` / `-omega`; the unified form is convenient when the branch is
+-- abstracted as `μ : OmegaIndex`.
+ω-rank-pow-<-succ : ∀ μ → ω-rank-pow μ <′ ω-rank-pow-succ μ
+ω-rank-pow-<-succ (fin n) = ω-rank-pow-<-succ-fin n
+ω-rank-pow-<-succ ω       = ω-rank-pow-<-succ-omega
+
 -- Atomic-rank-pow `refl`-shape primitives.  For non-bplus, non-bzero
 -- BT constructors, `rank-pow` reduces to `ω-rank-pow` of the
 -- corresponding `head-Ω` value.  Both equations are `refl`; provided
@@ -524,49 +564,25 @@ rank-pow-bpsi-via-head-Ω _ _ = refl
 -- Where this lands in the head-Ω closure plan
 ----------------------------------------------------------------------
 --
--- The abstraction landed here (`ω-rank-pow-succ` + the fin-branch
--- dominance + the atomic factoring) is the smallest useful first cut.
--- The two open follow-ons are:
---
--- Slice 2-omega.  Replace the ω branch of `ω-rank-pow-succ` with a
--- genuinely strictly-dominating shape and prove `ω-rank-pow ω <′
--- (new-shape)`.  Candidate: `ω^(ω+1)` encoded as
--- `olim (λ n → (ω-rank-pow ω) ·ℕ n)`.  Cross-checks before committing:
--- (i) the new shape closes under ordinal addition strictly above
--- `ω-rank-pow ω` (so additive-principal-style closure lifts);
--- (ii) the consumer (Slice 3) does not need the additive-principal
--- *of `ω-rank-pow-succ ω` itself* — it needs additive-principal of
--- `ω-rank-pow (head-Ω target)`, which already lands via the existing
--- `additive-principal-ω-rank-pow {ω}` (lines 238–255);
--- (iii) sanity-check the indexing.  The candidate's branches are
--- `(ω-rank-pow ω) ·ℕ n = (… (oz ⊕ ω-rank-pow ω) … ⊕ ω-rank-pow ω)`
--- — the leading `oz ⊕` is NOT definitionally `ω-rank-pow ω` under
--- Brouwer's right-recursing `_⊕_`.  As an ordinal denotation the
--- supremum is `ω^ω · ω = ω^(ω+1)` and is strictly above `ω^ω`, so
--- the lemma *should* go through, but the proof needs the
--- propositional `oz ⊕ X ≤′ X` (or a path-algebra equivalent) at the
--- right step — this is exactly the same hazard ("same ordinal under
--- different ℕ-indexing") that disqualified the original
--- `olim (λ n → ω^(suc(suc n)))` shape.  Verify with a thin spike
--- before committing the body.
+-- The abstractions landed here (`ω-rank-pow-succ` + both per-marker
+-- dominances + the atomic factoring) close everything Slice 2 promised
+-- *except* the full domination lemma over the WfCNF carrier.  One
+-- follow-on remains.
 --
--- TODO(slice-2-bplus).  Once the ω branch closes, prove the full
--- lemma
+-- TODO(slice-2-bplus).  Prove the full lemma
 --   rank-pow-dominated-by-head-Ω : (t : BT) → NonBzero t → WfCNF t
 --                                → rank-pow t <′ ω-rank-pow-succ (head-Ω t)
--- by structural recursion on the WfCNF carrier.  The bplus case
--- needs a `rank-pow-mono-≤ᵇ : x ≤ᵇ y → rank-pow x ≤′ rank-pow y`
--- companion for the original `_<ᵇ_` — landing-site below this
--- comment block — because the WfCNF tail bound is `_≤ᵇ_`, not
--- `_≤ᵇ⁰_`.  The existing `rank-pow-mono-≤ᵇ⁰` in `RankMonoUmbrella`
--- covers the `<ᵇ⁰` carrier only.  A direct `_≤ᵇ_`-mono primitive
--- would need either (a) bridging `_≤ᵇ_` to `_≤ᵇ⁰_` (which is
--- exactly the open Slice 4 problem — full rank-mono umbrella over
--- the original `_<ᵇ_`), or (b) a head-Ω inversion lemma
--- `bOmega ν <ᵇ x → ν <Ω head-Ω x` (and ψ-analogue) that does not
--- transitively depend on rank-mono.  Option (b) is the cleaner
--- path; it parallels the existing per-constructor rank-mono
--- primitives without going through the umbrella, and keeps
--- `rank-pow-dominated-by-head-Ω` independent of
--- `rank-pow-mono-≤ᵇ` so that a future signature change to one
--- does not silently break the other.
+-- by structural recursion on the WfCNF carrier.  Both per-marker
+-- dominances now hold (`ω-rank-pow-<-succ`), so the bOmega / bpsi
+-- atomic cases discharge directly via the atomic factoring lemmas
+-- (`rank-pow-bOmega-via-head-Ω`, `rank-pow-bpsi-via-head-Ω`).  The
+-- remaining bplus case needs a `rank-pow-mono-≤ᵇ : x ≤ᵇ y → rank-pow
+-- x ≤′ rank-pow y` companion for the original `_<ᵇ_` (the WfCNF tail
+-- bound is `_≤ᵇ_`, not `_≤ᵇ⁰_`).  The existing `rank-pow-mono-≤ᵇ⁰`
+-- in `RankMonoUmbrella` covers the `<ᵇ⁰` carrier only.  Option (b)
+-- of the original two paths — head-Ω inversion that does not
+-- transitively depend on rank-mono — landed separately as
+-- `Ordinal.Buchholz.HeadOmegaInversion` (the lemmas
+-- `head-Ω-inv-bOmega` and `head-Ω-inv-bpsi`).  Slice 2-bplus consumes
+-- those plus the per-marker dominances above; no further dependency
+-- on rank-mono is introduced.

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -414,7 +414,10 @@ open import Ordinal.Buchholz.HeadOmega using
 open import Ordinal.Buchholz.RankPow using
   ( ω-rank-pow-succ
   ; ω-rank-pow-succ-fin
+  ; ω-rank-pow-succ-omega
   ; ω-rank-pow-<-succ-fin
+  ; ω-rank-pow-<-succ-omega
+  ; ω-rank-pow-<-succ
   ; rank-pow-bOmega-via-head-Ω
   ; rank-pow-bpsi-via-head-Ω
   )