proof(ordinal): general head-Ω monotonicity head-Ω-mono (Gate 1 building block)

Adds the general leading-Ω monotonicity lemma over the whole `_<ᵇ_`
relation:

    head-Ω-mono : x <ᵇ y → head-Ω x ≤Ω head-Ω y

proved by structural recursion on the `_<ᵇ_` derivation (all 11
constructors). This generalises the two atomic inversions in this
module — `head-Ω-inv-bOmega` (bOmega source, strict) and
`head-Ω-inv-bpsi` (bpsi source, ≤) — to an arbitrary source shape,
including `bzero` (via the `fin 0`-minimum helper `fin0-min`) and
left-nested `bplus` chains (via the IH on `<ᵇ-{Ω+,ψ+,+Ω,+ψ,+1}`).

Why it matters (Gate 1 scoping): the joint-bplus `<ᵇ-+1` rank-mono
closure runs through CNF dominance —
`rank-pow (bplus x₁ x₂) <′ ω-rank-pow-succ (head-Ω x₁)` (the landed
`rank-pow-dominated-by-head-Ω`) composed with a leading-Ω bound on the
target. `head-Ω-mono` supplies that bound for the general (incl.
chain-headed) source, which the atomic inversions could not. The
non-strict `≤Ω` is exactly right: the `<ᵇ-ψΩ≤` boundary
(`bpsi ν α <ᵇ bOmega ν`) leaves the leading Ω-marker fixed, and that
equal-Ω boundary is the residual the rank-adm discrimination must
still cover.

- `head-Ω-mono` 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

@@ -63,10 +63,15 @@ module Ordinal.Buchholz.HeadOmegaInversion where
 
 open import Ordinal.OmegaMarkers   using
   ( OmegaIndex
+  ; fin
+  ; ω
   ; _<Ω_
   ; _≤Ω_
+  ; fin≤fin
+  ; fin≤ω
   ; <Ω→≤Ω
   )
+open import Data.Nat using (z≤n)
 open import Ordinal.Buchholz.Syntax using
   ( BT
   ; bzero
@@ -76,12 +81,18 @@ open import Ordinal.Buchholz.Syntax using
   )
 open import Ordinal.Buchholz.Order  using
   ( _<ᵇ_
+  ; <ᵇ-0-Ω
+  ; <ᵇ-0-+
+  ; <ᵇ-0-ψ
   ; <ᵇ-ΩΩ
   ; <ᵇ-Ωψ
   ; <ᵇ-ψΩ
   ; <ᵇ-ψΩ≤
   ; <ᵇ-Ω+
   ; <ᵇ-ψ+
+  ; <ᵇ-+Ω
+  ; <ᵇ-+ψ
+  ; <ᵇ-+1
   )
 open import Ordinal.Buchholz.HeadOmega using (head-Ω)
 
@@ -124,3 +135,45 @@ head-Ω-inv-bpsi : ∀ {ν α y} → bpsi ν α <ᵇ y → ν ≤Ω head-Ω y
 head-Ω-inv-bpsi (<ᵇ-ψΩ p)  = <Ω→≤Ω p
 head-Ω-inv-bpsi (<ᵇ-ψΩ≤ p) = p
 head-Ω-inv-bpsi (<ᵇ-ψ+ p)  = head-Ω-inv-bpsi p
+
+----------------------------------------------------------------------
+-- General head-Ω monotonicity over the whole `_<ᵇ_` relation
+----------------------------------------------------------------------
+
+-- `fin 0` is the minimum Ω-marker.  Used for the `bzero`-source
+-- cases, where `head-Ω bzero = fin 0`.
+fin0-min : ∀ ν → fin 0 ≤Ω ν
+fin0-min (fin n) = fin≤fin z≤n
+fin0-min ω       = fin≤ω
+
+-- The leading Ω-marker is monotone along ANY `_<ᵇ_` step:
+--
+--   x <ᵇ y  →  head-Ω x ≤Ω head-Ω y
+--
+-- This generalises the two atomic inversions above (which special-
+-- case a `bOmega`/`bpsi` source and additionally extract the
+-- *strict* bound where the constructor permits) to an arbitrary
+-- source shape, including `bzero` and left-nested `bplus` chains.
+-- The bound is necessarily non-strict: the `<ᵇ-ψΩ≤` constructor
+-- (`bpsi ν α <ᵇ bOmega ν`) and the analogous boundary steps leave
+-- the leading Ω-marker unchanged.
+--
+-- Proof: structural recursion on the `_<ᵇ_` derivation.  Every
+-- recursive call (`<ᵇ-Ω+`, `<ᵇ-ψ+`, `<ᵇ-+Ω`, `<ᵇ-+ψ`, `<ᵇ-+1`)
+-- descends to a structurally-smaller derivation; the `head-Ω`
+-- reductions on `bplus` (leftmost) and on the atomic constructors
+-- are definitional, so each goal lines up with `<Ω→≤Ω`, the
+-- carried `≤Ω` witness, `fin0-min`, or the IH.
+head-Ω-mono : ∀ {x y} → x <ᵇ y → head-Ω x ≤Ω head-Ω y
+head-Ω-mono (<ᵇ-0-Ω {μ})    = fin0-min μ
+head-Ω-mono (<ᵇ-0-ψ {ν})    = fin0-min ν
+head-Ω-mono (<ᵇ-0-+ {x})    = fin0-min (head-Ω x)
+head-Ω-mono (<ᵇ-ΩΩ p)       = <Ω→≤Ω p
+head-Ω-mono (<ᵇ-Ωψ p)       = <Ω→≤Ω p
+head-Ω-mono (<ᵇ-ψΩ p)       = <Ω→≤Ω p
+head-Ω-mono (<ᵇ-ψΩ≤ p)      = p
+head-Ω-mono (<ᵇ-Ω+ p)       = head-Ω-mono p
+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

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -431,9 +431,14 @@ open import Ordinal.Buchholz.RankPow using
 -- domination lemma's dependency-graph clean against future signature
 -- changes to `rank-pow-mono-≤ᵇ`.  Strict on the Ω-source, non-strict
 -- on the ψ-source (tracks the `<ᵇ-ψΩ≤` constructor).
+-- `head-Ω-mono` generalises the two atomic inversions to an
+-- arbitrary `_<ᵇ_` source shape (incl. bzero + left-nested bplus):
+-- `x <ᵇ y → head-Ω x ≤Ω head-Ω y`.  The non-strict leading-Ω bound
+-- that the joint-bplus (`<ᵇ-+1`) rank-mono closure consumes.
 open import Ordinal.Buchholz.HeadOmegaInversion using
   ( head-Ω-inv-bOmega
   ; head-Ω-inv-bpsi
+  ; head-Ω-mono
   )
 
 -- Lane 3 head-Ω Slice 2-bplus (own block per CLAUDE.md Working