proof(ordinal): ψ-below-Ω boundary room lemma ω-rank-pow-⊕-below-succ

The load-bearing ordinal fact for the equal-Ω boundary (the residual
Gate 1 case `bpsi ν α <ᵇ bOmega ν`): under the admissibility bound
`β <′ ω-rank-pow ν` (the `WfAdm` bpsi field with β = rank-pow α),

    ω-rank-pow ν ⊕ β  <′  ω-rank-pow-succ ν

i.e. the admissibility-rank of `ψ_ν(α)` (= `rank-adm (bpsi ν α)`) sits
strictly below `ω-rank-pow-succ ν`, the natural rank for `Ω_ν`. This
is the gap `ψ_ν(α) < Ω_ν` measured at the rank level: both summands
are `< ω-rank-pow-succ ν` (left by `ω-rank-pow-<-succ`, right by
admissibility + that jump), and `ω-rank-pow-succ ν` is additive
principal (`additive-principal-ω-rank-pow-succ`), so the sum stays
below.

This is the "room" the equal-ν discharge needs. Honest scope: it is
the LOCAL equal-marker fact, not a global rank — a global placement of
`bOmega ν` at `ω-rank-pow-succ ν` would still have to reconcile the
cross-index `<ᵇ-Ωψ` constructor (`bOmega μ <ᵇ bpsi (suc μ) bzero`),
where `ω-rank-pow-succ μ` meets `ω-rank-pow (suc μ)` and the strict
gap collapses. That cross-index reconciliation is the remaining open
design problem; this lemma is its first verified building block.

- `ω-rank-pow-⊕-below-succ` pinned in `Ordinal/Buchholz/Smoke.agda`.
- `Smoke.agda` + `All.agda` exit 0 under `--safe --without-K`; zero
  postulates, no escape pragmas, no funext.

https://claude.ai/code/session_017t53M7W7ubmXpwymveLcCE

Author: claude

proofs/agda/Ordinal/Buchholz/RankPowDomination.agda

@@ -240,6 +240,43 @@ additive-principal-ω-rank-pow-succ {ω} {α} {β} (kα , sα) (kβ , sβ) =
               step2)
             step3
 
+----------------------------------------------------------------------
+-- ψ-below-Ω boundary "room" lemma
+----------------------------------------------------------------------
+
+-- The load-bearing ordinal fact behind placing `Ω_ν` (= `bOmega ν`)
+-- strictly above every admissible `ψ_ν(α)` (= `bpsi ν α`) at the
+-- SAME leading marker ν.  When the ψ-argument is admissibility-bounded
+-- (`β <′ ω-rank-pow ν` — exactly the `WfAdm` bpsi field with
+-- β = rank-pow α), the admissibility-rank `ω-rank-pow ν ⊕ β`
+-- (= `rank-adm (bpsi ν α)`) sits strictly below `ω-rank-pow-succ ν`
+-- (the natural rank for `bOmega ν`).
+--
+-- This is the gap `ψ_ν(α) < Ω_ν` measured at the rank level: both
+-- summands are `< ω-rank-pow-succ ν` (the left by `ω-rank-pow-<-succ`,
+-- the right by admissibility composed with that same jump), and
+-- `ω-rank-pow-succ ν` is additive principal
+-- (`additive-principal-ω-rank-pow-succ`), so the sum stays below.
+--
+-- Honest scope: this is the LOCAL equal-marker boundary fact — the
+-- "room" the equal-Ω joint-bplus discharge needs.  A GLOBAL rank
+-- placing `bOmega ν` at `ω-rank-pow-succ ν` would still have to
+-- reconcile the cross-index `<ᵇ-Ωψ` constructor
+-- (`bOmega μ <ᵇ bpsi (suc μ) bzero`), where `ω-rank-pow-succ μ`
+-- meets `ω-rank-pow (suc μ)` and the strict gap collapses.  So this
+-- is a building block for the equal-ν discharge, not a finished
+-- global rank.
+
+ω-rank-pow-⊕-below-succ : ∀ {ν β}
+  → β <′ ω-rank-pow ν
+  → (ω-rank-pow ν ⊕ β) <′ ω-rank-pow-succ ν
+ω-rank-pow-⊕-below-succ {ν} {β} β<ν =
+  additive-principal-ω-rank-pow-succ {ν} {ω-rank-pow ν} {β}
+    (ω-rank-pow-<-succ ν)
+    (≤′-<′-trans {β} {ω-rank-pow ν} {ω-rank-pow-succ ν}
+      (<′→≤′ {β} {ω-rank-pow ν} β<ν)
+      (ω-rank-pow-<-succ ν))
+
 ----------------------------------------------------------------------
 -- bplus right-summand bound
 ----------------------------------------------------------------------

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -456,6 +456,7 @@ open import Ordinal.Buchholz.RankPowDomination using
   ; ω-rank-pow-succ-pos
   ; additive-principal-ω-rank-pow-succ
   ; rank-pow-dominated-by-head-Ω
+  ; ω-rank-pow-⊕-below-succ
   )
 
 -- Slice 3 prerequisites (own block per CLAUDE.md Working rules):