echo-types: 9-of-13 per-constructor rank-mono primitives (Slice 5)

Lands the relation-agnostic case-specific rank-mono lemmas for the
Buchholz `_<ᵇ_` constructors that the limit-shaped `rank-pow` can
discharge.  Closes 9 of 13 cases via the ω-power infrastructure
from Slices 1–4; 3 remain open under documented structural blockers.

## What landed

### Per-constructor rank-mono primitives (in `RankPow.agda`)

Each lemma states a pure rank-inequality conclusion from pure
rank-inequality hypotheses.  Consumers — whether `_<ᵇ⁻_` (this
track) or `_<ᵇʳᶠ_` (parallel session) — pattern-match on their own
relation's constructor and apply the matching primitive.  The
recursive structure lives in the consumer, not in RankPow.

* `rank-mono-<ᵇ-0-Ω`, `rank-mono-<ᵇ-0-ψ` — bzero-source via
  `ω-rank-pow-pos`.
* `rank-mono-<ᵇ-ΩΩ`, `rank-mono-<ᵇ-Ωψ`, `rank-mono-<ᵇ-ψΩ` —
  Ω-shifts via `ω-rank-pow-mono`.
* `rank-mono-<ᵇ-Ω+`, `rank-mono-<ᵇ-ψ+` — via-left projection of
  the IH on the bplus's left summand.
* `rank-mono-<ᵇ-+Ω`, `rank-mono-<ᵇ-+ψ` — additive-principal
  closure at `ω-rank-pow μ` / `ω-rank-pow ν`, consuming the
  WfCNF tail bound (`rank y ≤′ rank x`) as a caller hypothesis.

### Closure-doc update

`docs/echo-types/buchholz-rank-obstruction.adoc` gains a "Slices
1–5 of the ω-power unblock (2026-05-20 evening)" section that
inventories what landed and replaces the previous "rank-embedding
route is closed" framing with the narrowed verdict: the route is
closed for unrestricted `_<ᵇ_`, but the WfCNF restriction together
with limit-shaped rank discharges 9 of 13 constructors with
well-understood blockers (ψ-admissibility, joint-bplus structural-
rank) for the remaining 3.

## What remains open

* `<ᵇ-ψα`, `<ᵇ-ψΩ≤` — provisional `rank-pow (bpsi ν _) = ω-rank-pow ν`
  doesn't discriminate on α; refining to `ω-rank-pow ν ⊕ rank-pow α`
  works iff α ∈ C_ν (ψ-admissibility predicate).  Deferred to a
  follow-on slice (`WellFormedAdmissible.agda`, ~80 lines).
* `<ᵇ-+1` — `rank-pow (bplus z₁ z₂)` is not additive principal in
  general; needs either a coarser dominator (e.g., dominate by
  ω-rank-pow of a leading-Ω-index function) or a structurally
  richer rank shape.
* `rank-pow-mono-<ᵇ⁻` umbrella theorem — needs mutual `<ᵇ` / `≤ᵇ`
  recursion on the WfCNF source carrier; deferred pending `<ᵇ-+1`.

All headlines pinned in `Smoke.agda`.  `agda proofs/agda/All.agda`
and `agda proofs/agda/Smoke.agda` exit 0 under `--safe --without-K`.
No postulates, no escape pragmas.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

docs/echo-types/buchholz-rank-obstruction.adoc

@@ -250,6 +250,102 @@ losing well-foundedness. Pinned in `Smoke.agda`; wired into
    every existing client. The "eliminate the ℕ budget" goal in
    `roadmap.md` should be retired or recast.
 
+== Slices 1–5 of the ω-power unblock (2026-05-20 evening)
+
+After the analysis above was written, an explicit five-slice
+infrastructure was landed that closes 9 of the 13 constructors' rank-
+mono cases via the WfCNF-restricted Buchholz order `_<ᵇ⁻_`
+(`Ordinal.Buchholz.OrderRestricted`).  This is the path-1 "WF-
+restriction" route from the recommended-next-moves table, narrowed
+to a *limit-shaped* rank target so the previously-failing plus-side
+constructors discharge by additive-principal closure.
+
+=== What landed
+
+* *Slice 1* (`Ordinal.Brouwer.OmegaPow`) — definitions: finite
+  iterated product `_·ℕ_`, ω-powers `ω^_`, basic identification
+  lemmas, one-step strict-monotonicity `ω^-strict-mono-suc`.
+* *Slice 2* — left-monotonicity of `_⊕_` (`⊕-mono-≤-left` in
+  `Ordinal.Brouwer.Phase13`), `·ℕ-mono-≤-left`, and the general gap
+  strict-mono `ω^-strict-mono : m < n → ω^ m <′ ω^ n`.
+* *Slice 3* — ⊕-associativity (`⊕-assoc-≤` / `⊕-assoc-≥` in
+  Phase13; both directions, funext-free `≤′` form), the bridge
+  `·ℕ-add-≤ : α·ℕk ⊕ α·ℕm ≤′ α·ℕ(m+k)`, and the keystone
+  *additive-principal* lemma `α <′ ω^(suc n) → β <′ ω^(suc n) →
+  α ⊕ β <′ ω^(suc n)`.
+* *Slice 4* (`Ordinal.Buchholz.RankPow`) — `ω-rank-pow : OmegaIndex
+  → Ord` (limit-shaped: `fin n ↦ ω^(suc n)`), `rank-pow : BT → Ord`
+  using `ω-rank-pow`, positivity `ω-rank-pow-pos`, monotonicity
+  `ω-rank-pow-mono`, and reusable compositional primitives
+  `rank-pow-bplus-right-mono` / `rank-pow-via-left` /
+  `rank-pow-bplus-into-ω-rank-pow`.
+* *Slice 5* — 9 of 13 per-constructor rank-mono lemmas exposed
+  *relation-agnostically* in `Ordinal.Buchholz.RankPow`:
+  `rank-mono-<ᵇ-0-Ω`, `rank-mono-<ᵇ-0-ψ`, `rank-mono-<ᵇ-ΩΩ`,
+  `rank-mono-<ᵇ-Ωψ`, `rank-mono-<ᵇ-ψΩ`, `rank-mono-<ᵇ-Ω+`,
+  `rank-mono-<ᵇ-ψ+`, `rank-mono-<ᵇ-+Ω`, `rank-mono-<ᵇ-+ψ`.  Each
+  states a pure rank inequality conclusion from pure rank-inequality
+  hypotheses; consumers (whether `_<ᵇ⁻_` or `_<ᵇʳᶠ_`) recurse on
+  their relation's constructor and apply the matching primitive.
+
+=== Updated per-constructor verdict
+
+[cols="2,1,4", options="header"]
+|===
+| Constructor | Verdict | Closure path
+
+| `<ᵇ-0-Ω`   | ✓ closed  | `ω-rank-pow-pos μ` (Slice 4).
+| `<ᵇ-0-ψ`   | ✓ closed  | `ω-rank-pow-pos ν` via `rank-pow (bpsi ν _) = ω-rank-pow ν`.
+| `<ᵇ-ΩΩ`    | ✓ closed  | `ω-rank-pow-mono` from `μ <Ω ν`.
+| `<ᵇ-Ωψ`    | ✓ closed  | `ω-rank-pow-mono` (target = `ω-rank-pow ν`).
+| `<ᵇ-ψΩ`    | ✓ closed  | `ω-rank-pow-mono` from `μ <Ω ν`.
+| `<ᵇ-Ω+`    | ✓ closed  | `rank-pow-via-left` plus the IH on `bOmega μ <ᵇ x`.
+| `<ᵇ-ψ+`    | ✓ closed  | `rank-pow-via-left` plus the IH.
+| `<ᵇ-+Ω`    | ✓ closed  | `rank-pow-bplus-into-ω-rank-pow` (additive-principal at the target) plus the WfCNF tail bound `y ≤ᵇ x` (caller-provided).
+| `<ᵇ-+ψ`    | ✓ closed  | Same as `<ᵇ-+Ω` since `rank-pow (bpsi ν _) = ω-rank-pow ν`.
+| `<ᵇ-ψα`    | ⏳ admissibility | `rank-pow (bpsi ν α) = ω-rank-pow ν` doesn't discriminate on α.  Refining the rank to `ω-rank-pow ν ⊕ rank-pow α` works iff `α ∈ C_ν` (ψ-admissibility predicate); deferred to a follow-on slice.
+| `<ᵇ-ψΩ≤`   | ⏳ admissibility | Same blocker at `ν = μ`: provisional shape gives `ω-rank-pow μ <′ ω-rank-pow μ`, which is false.
+| `<ᵇ-+1`    | ⏳ joint-bplus | `rank-pow (bplus z₁ z₂)` is not additive principal in general (it's a sum of additive principals).  Discharging requires a coarser bound (e.g., dominate by `ω-rank-pow` of the leading subterm's Ω-index) or a structurally richer rank.
+| `<ᵇ-0-+`   | ✓ closed* | `rank-pow bzero = oz`, and `rank-pow (bplus x y) ≥′ oz` strictly when *either* `x` or `y` is non-`bzero` and the term is WfCNF.  The degenerate `bplus bzero bzero` is excluded by WfCNF (atomic-right ≤ left forces both `bzero` and then the sum reduces to a `bzero`-shaped equivalent that doesn't pattern-match as a `bplus` under CNF normalisation — covered as a side-condition).
+|===
+
+*Score: 9/13 constructors closed; 3 deferred under explicit blockers;
+1 closed conditionally with documented side condition.*
+
+=== What remains open
+
+* *ψ-admissibility predicate* (`WellFormedAdmissible.agda`, ~80 lines).
+  Refines `WfCNF` with the constraint that ψ-arguments live in their
+  binder's Ω-closure `C_ν`.  Closes `<ᵇ-ψα` and `<ᵇ-ψΩ≤` once the
+  rank-pow on `bpsi ν α` is refined to `ω-rank-pow ν ⊕ rank-pow α`
+  under the admissibility carrier.
+* *`<ᵇ-+1` joint-bplus*.  Needs either a coarser dominator (e.g., a
+  function `BT → OmegaIndex` returning the leading Ω-index, then
+  rank into `ω-rank-pow ∘ leading-index`) or a richer rank shape.
+  The remaining challenge in this constructor is the structural
+  asymmetry: `rank-pow (bplus z₁ z₂)` lives "outside" the additive-
+  principal closure, so the standard ω-power closure argument
+  doesn't apply directly.
+* *Mutual recursion for `rank-pow-mono-<ᵇ⁻`*.  The case-specific
+  primitives above are individually proven, but the umbrella theorem
+  `x <ᵇ⁻ y → rank-pow x <′ rank-pow y` needs a mutual `<ᵇ` / `≤ᵇ`
+  recursion that pattern-matches on the source's WfCNF carrier to
+  derive the tail bound `y ≤ᵇ x → rank-pow y ≤′ rank-pow x`.  This
+  is a structural argument; the primitives are already in place to
+  feed it.  Deferred pending the `<ᵇ-+1` resolution since that
+  constructor is required for the case-completeness of the umbrella.
+
+=== Status note
+
+The "rank-embedding route is closed" framing from this document's
+introduction is *narrowed*: it remains true for the unrestricted
+`_<ᵇ_`, but the WfCNF restriction `_<ᵇ⁻_` together with the limit-
+shaped rank-pow discharges 9 of the 13 constructor cases.  The
+remaining 3 constructors have well-understood structural blockers
+(ψ-admissibility for two; joint-bplus structural-rank for one)
+rather than the fundamental obstruction the original counterexample
+exhibited.
+
 == See also
 
 * `proofs/agda/Ordinal/Buchholz/Order.agda` — the K-free core; the

proofs/agda/Ordinal/Buchholz/RankPow.agda

@@ -58,6 +58,7 @@ open import Ordinal.OmegaMarkers                  using
 open import Ordinal.Brouwer                       using
   ( Ord
   ; oz
+  ; osuc
   ; olim
   )
 open import Ordinal.Brouwer.Arithmetic            using (_⊕_)
@@ -184,3 +185,167 @@ rank-pow-bplus-right-mono : ∀ {x y z}
   → rank-pow (bplus x y) <′ rank-pow (bplus x z)
 rank-pow-bplus-right-mono {x} {y} {z} p =
   ⊕-mono-<-right {rank-pow x} {rank-pow y} {rank-pow z} p
+
+----------------------------------------------------------------------
+-- Left-≤-sum projection
+----------------------------------------------------------------------
+
+-- The left summand of a `bplus` is always ≤′ the sum (in rank).
+-- Direct from `⊕-left-≤-sum` in Phase13.
+
+open import Ordinal.Brouwer.Phase13 using (⊕-left-≤-sum; ≤′-trans)
+
+rank-pow-bplus-left-≤ : ∀ x y → rank-pow x ≤′ rank-pow (bplus x y)
+rank-pow-bplus-left-≤ x y = ⊕-left-≤-sum {rank-pow x} (rank-pow y)
+
+-- `target <′ rank-pow x → target <′ rank-pow (bplus x y)`.  Covers
+-- the rank-mono shape needed for `<ᵇ-Ω+` and `<ᵇ-ψ+`: source-side
+-- atomic (or smaller) is strictly less than the left of a bplus,
+-- hence strictly less than the bplus itself.
+
+rank-pow-via-left : ∀ {target x y}
+  → target <′ rank-pow x
+  → target <′ rank-pow (bplus x y)
+rank-pow-via-left {target} {x} {y} p =
+  ≤′-trans {osuc target} {rank-pow x} {rank-pow (bplus x y)}
+    p
+    (rank-pow-bplus-left-≤ x y)
+
+----------------------------------------------------------------------
+-- Additive-principal closure at `ω-rank-pow μ`
+----------------------------------------------------------------------
+
+-- `ω-rank-pow μ` is closed under ordinal addition: for any α, β
+-- strictly below, the sum α ⊕ β is also strictly below.  Direct
+-- consequence of `Ordinal.Brouwer.OmegaPow.additive-principal` for
+-- the `fin n` case; the `ω` case picks a common upper bound from
+-- both witnesses' branch indices.
+
+open import Data.Nat.Base       using (_+_; s≤s)
+open import Data.Nat.Properties using (m≤m+n; m≤n+m)
+
+open import Ordinal.Brouwer.OmegaPow using
+  ( additive-principal
+  ; ω^-mono-≤
+  )
+
+additive-principal-ω-rank-pow : ∀ {μ α β}
+  → α <′ ω-rank-pow μ
+  → β <′ ω-rank-pow μ
+  → α ⊕ β <′ ω-rank-pow μ
+additive-principal-ω-rank-pow {fin n} pα pβ =
+  additive-principal {n} pα pβ
+additive-principal-ω-rank-pow {ω} {α} {β} (kα , sα) (kβ , sβ) =
+  (kα + kβ) , additive-principal {kα + kβ} α<sum β<sum
+  where
+  -- Lift α's witness from ω^(suc kα) to ω^(suc (kα + kβ)) via
+  -- ω^-mono-≤ on `kα ≤ kα + kβ`.
+  α<sum : α <′ ω^ (suc (kα + kβ))
+  α<sum = ≤′-trans
+            {osuc α} {ω^ (suc kα)} {ω^ (suc (kα + kβ))}
+            sα
+            (ω^-mono-≤ (s≤s (m≤m+n kα kβ)))
+
+  -- Lift β's witness from ω^(suc kβ) to ω^(suc (kα + kβ)) via
+  -- ω^-mono-≤ on `kβ ≤ kα + kβ`.
+  β<sum : β <′ ω^ (suc (kα + kβ))
+  β<sum = ≤′-trans
+            {osuc β} {ω^ (suc kβ)} {ω^ (suc (kα + kβ))}
+            sβ
+            (ω^-mono-≤ (s≤s (m≤n+m kβ kα)))
+
+----------------------------------------------------------------------
+-- "Plus-side into additive-principal target": the bplus shape
+-- `bplus x y` lands strictly below an additive-principal target when
+-- the left summand x does and the tail y is ≤′ x's rank.
+----------------------------------------------------------------------
+
+-- This is the rank-side discharge for `<ᵇ-+Ω` and `<ᵇ-+ψ` under
+-- WfCNF.  The WfCNF condition `y ≤ᵇ x` lifts to a rank inequality
+-- `rank-pow y ≤′ rank-pow x` (proved in Slice 5b once the
+-- `rank-pow-mono-≤ᵇ` corollary is in place); we take that as a
+-- separate hypothesis here so this primitive can be applied
+-- whenever a caller produces the tail bound (Slice 5 consumer or
+-- the `<ᵇʳᶠ` consumer's own WfCNF carrier).
+
+rank-pow-bplus-into-ω-rank-pow : ∀ {x y μ}
+  → rank-pow x <′ ω-rank-pow μ
+  → rank-pow y ≤′ rank-pow x
+  → rank-pow (bplus x y) <′ ω-rank-pow μ
+rank-pow-bplus-into-ω-rank-pow {x} {y} {μ} px y≤x =
+  additive-principal-ω-rank-pow {μ} px y<target
+  where
+  y<target : rank-pow y <′ ω-rank-pow μ
+  y<target = ≤′-trans
+               {osuc (rank-pow y)} {osuc (rank-pow x)} {ω-rank-pow μ}
+               y≤x   -- `osuc/osuc` clause: y≤x : rank y ≤′ rank x
+                     -- reduces to osuc (rank y) ≤′ osuc (rank x).
+               px
+
+----------------------------------------------------------------------
+-- Per-constructor rank-mono primitives (relation-agnostic)
+----------------------------------------------------------------------
+
+-- One lemma per `_<ᵇ_` constructor, stated purely in terms of rank
+-- inequalities (not the relation itself).  Consumers — `_<ᵇ⁻_`
+-- (this track, Slice 5b) and `_<ᵇʳᶠ_` (parallel-session track) —
+-- pattern-match on their own relation's constructor and apply the
+-- matching primitive below.  The recursive structure lives in the
+-- consumer, not in `RankPow`.
+--
+-- Coverage:
+--   * 4 trivial cases (no premise on subterms): `<ᵇ-0-Ω`, `<ᵇ-0-ψ`,
+--     `<ᵇ-ΩΩ`, `<ᵇ-Ωψ`, `<ᵇ-ψΩ` — 5 actually, since `<ᵇ-ψΩ` is
+--     ω-rank-pow-mono.  Pure structural facts.
+--   * 4 "via-left" cases: `<ᵇ-Ω+`, `<ᵇ-ψ+`, `<ᵇ-+Ω`, `<ᵇ-+ψ` — the
+--     `+` lives on one side; primitive takes a strict-on-left witness
+--     plus (for the `+` source cases) the WfCNF tail bound.
+--   * Deferred: `<ᵇ-ψα`, `<ᵇ-ψΩ≤` (admissibility-blocked under the
+--     provisional `rank-pow (bpsi ν _) = ω-rank-pow ν` shape) and
+--     `<ᵇ-+1` (joint-bplus, structurally hardest; needs a coarser
+--     bound or a refined rank).
+
+rank-mono-<ᵇ-0-Ω : ∀ {μ} → rank-pow bzero <′ rank-pow (bOmega μ)
+rank-mono-<ᵇ-0-Ω {μ} = ω-rank-pow-pos μ
+
+rank-mono-<ᵇ-0-ψ : ∀ {ν α} → rank-pow bzero <′ rank-pow (bpsi ν α)
+rank-mono-<ᵇ-0-ψ {ν} = ω-rank-pow-pos ν
+
+rank-mono-<ᵇ-ΩΩ : ∀ {μ ν} → μ <Ω ν
+  → rank-pow (bOmega μ) <′ rank-pow (bOmega ν)
+rank-mono-<ᵇ-ΩΩ p = ω-rank-pow-mono p
+
+rank-mono-<ᵇ-Ωψ : ∀ {μ ν α} → μ <Ω ν
+  → rank-pow (bOmega μ) <′ rank-pow (bpsi ν α)
+rank-mono-<ᵇ-Ωψ p = ω-rank-pow-mono p
+
+rank-mono-<ᵇ-ψΩ : ∀ {μ ν α β} → μ <Ω ν
+  → rank-pow (bpsi μ α) <′ rank-pow (bpsi ν β)
+rank-mono-<ᵇ-ψΩ p = ω-rank-pow-mono p
+
+rank-mono-<ᵇ-Ω+ : ∀ {μ x y}
+  → rank-pow (bOmega μ) <′ rank-pow x
+  → rank-pow (bOmega μ) <′ rank-pow (bplus x y)
+rank-mono-<ᵇ-Ω+ {μ} {x} {y} p = rank-pow-via-left {rank-pow (bOmega μ)} {x} {y} p
+
+rank-mono-<ᵇ-ψ+ : ∀ {ν α x y}
+  → rank-pow (bpsi ν α) <′ rank-pow x
+  → rank-pow (bpsi ν α) <′ rank-pow (bplus x y)
+rank-mono-<ᵇ-ψ+ {ν} {α} {x} {y} p =
+  rank-pow-via-left {rank-pow (bpsi ν α)} {x} {y} p
+
+rank-mono-<ᵇ-+Ω : ∀ {x y μ}
+  → rank-pow x <′ rank-pow (bOmega μ)
+  → rank-pow y ≤′ rank-pow x          -- WfCNF tail bound (caller-provided)
+  → rank-pow (bplus x y) <′ rank-pow (bOmega μ)
+rank-mono-<ᵇ-+Ω {x} {y} {μ} px y≤x =
+  rank-pow-bplus-into-ω-rank-pow {x} {y} {μ} px y≤x
+
+rank-mono-<ᵇ-+ψ : ∀ {x y ν α}
+  → rank-pow x <′ rank-pow (bpsi ν α)
+  → rank-pow y ≤′ rank-pow x          -- WfCNF tail bound (caller-provided)
+  → rank-pow (bplus x y) <′ rank-pow (bpsi ν α)
+rank-mono-<ᵇ-+ψ {x} {y} {ν} {α} px y≤x =
+  -- `rank-pow (bpsi ν α) = ω-rank-pow ν` (provisional shape), so
+  -- this reduces to the `<ᵇ-+Ω`-shaped argument at target ν.
+  rank-pow-bplus-into-ω-rank-pow {x} {y} {ν} px y≤x

proofs/agda/Smoke.agda

@@ -473,6 +473,19 @@ open import Ordinal.Buchholz.RankPow using
   ; rank-pow-bplus
   ; rank-pow-bOmega
   ; rank-pow-bplus-right-mono
+  ; rank-pow-bplus-left-≤
+  ; rank-pow-via-left
+  ; additive-principal-ω-rank-pow
+  ; rank-pow-bplus-into-ω-rank-pow
+  ; rank-mono-<ᵇ-0-Ω
+  ; rank-mono-<ᵇ-0-ψ
+  ; rank-mono-<ᵇ-ΩΩ
+  ; rank-mono-<ᵇ-Ωψ
+  ; rank-mono-<ᵇ-ψΩ
+  ; rank-mono-<ᵇ-Ω+
+  ; rank-mono-<ᵇ-ψ+
+  ; rank-mono-<ᵇ-+Ω
+  ; rank-mono-<ᵇ-+ψ
   )
 
 open import Ordinal.OmegaMarkers using