proof(ordinal): head-Ω-strict-or-eq — the joint-bplus umbrella case-split

Adds the leading-Ω classifier that turns a `_<ᵇ_` step into the
actionable disjunction a `<ᵇ-+1` rank-mono umbrella dispatches on:

    head-Ω-strict-or-eq : x <ᵇ y
      → (head-Ω x <Ω head-Ω y) ⊎ (head-Ω x ≡ head-Ω y)

It is `≤Ω-split` (existing, OmegaMarkers) composed with `head-Ω-mono`
(landed last commit). The two branches are exactly the joint-bplus
case-split:

  * LEFT (strict): feeds `RankPowSlice3Headline.rank-mono-<ᵇ-+1-via-
    head-Ω` directly — the CNF-dominance chain
    `rank-pow (bplus x₁ x₂) <′ ω-rank-pow-succ (head-Ω x₁)
      ≤′ ω-rank-pow (head-Ω y₁) ≤′ rank-pow (bplus y₁ y₂)`
    already closes this half.
  * RIGHT (equal-Ω boundary, e.g. `bpsi ν α <ᵇ bOmega ν` via
    `<ᵇ-ψΩ≤`): rank-pow collapses the ψ/Ω distinction, so the
    discharge needs the lex/admissibility second component — the
    genuine residual that the rank-lex / rank-adm route owns.

This pins down Gate 1's frontier to exactly the equal-Ω boundary:
the strict half is now mechanically dischargeable via this classifier
+ the existing head-Ω headline.

- `head-Ω-strict-or-eq` 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/HeadOmegaInversion.agda

@@ -70,8 +70,11 @@ open import Ordinal.OmegaMarkers   using
   ; fin≤fin
   ; fin≤ω
   ; <Ω→≤Ω
+  ; ≤Ω-split
   )
 open import Data.Nat using (z≤n)
+open import Data.Sum.Base using (_⊎_)
+open import Relation.Binary.PropositionalEquality using (_≡_)
 open import Ordinal.Buchholz.Syntax using
   ( BT
   ; bzero
@@ -177,3 +180,27 @@ head-Ω-mono (<ᵇ-ψ+ p)       = head-Ω-mono p
 head-Ω-mono (<ᵇ-+Ω p)       = head-Ω-mono p
 head-Ω-mono (<ᵇ-+ψ p)       = head-Ω-mono p
 head-Ω-mono (<ᵇ-+1 p)       = head-Ω-mono p
+
+----------------------------------------------------------------------
+-- Leading-Ω classification along a `_<ᵇ_` step
+----------------------------------------------------------------------
+
+-- Combining `head-Ω-mono` with `≤Ω-split`: every `x <ᵇ y` either
+-- strictly raises the leading Ω-marker, or leaves it equal.
+--
+--   * LEFT  (`head-Ω x <Ω head-Ω y`): the strict-head case the
+--     joint-bplus headline `RankPowSlice3Headline.rank-mono-<ᵇ-+1-
+--     via-head-Ω` consumes directly — the CNF-dominance chain has
+--     the room it needs.
+--   * RIGHT (`head-Ω x ≡ head-Ω y`): the equal-marker boundary
+--     (e.g. `bpsi ν α <ᵇ bOmega ν` via `<ᵇ-ψΩ≤`), where rank-pow
+--     collapses the ψ/Ω distinction and the discharge must come
+--     from the lex / admissibility second component instead.
+--
+-- This is the exact case-split a `<ᵇ-+1` rank-mono umbrella performs
+-- on its source derivation: feed LEFT to the head-Ω headline, route
+-- RIGHT to the boundary discharge.
+head-Ω-strict-or-eq : ∀ {x y}
+  → x <ᵇ y
+  → (head-Ω x <Ω head-Ω y) ⊎ (head-Ω x ≡ head-Ω y)
+head-Ω-strict-or-eq p = ≤Ω-split (head-Ω-mono p)

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -439,6 +439,7 @@ open import Ordinal.Buchholz.HeadOmegaInversion using
   ( head-Ω-inv-bOmega
   ; head-Ω-inv-bpsi
   ; head-Ω-mono
+  ; head-Ω-strict-or-eq
   )
 
 -- Lane 3 head-Ω Slice 2-bplus (own block per CLAUDE.md Working