echo-types: <ᵇ-+1 partial discharge via target-additive-principal parameter (Item 1)

Adds three new compositional primitives in `Ordinal.Buchholz.RankPow`
for the `<ᵇ-+1` constructor (`bplus x₁ x₂ <ᵇ bplus y₁ y₂` from
`x₁ <ᵇ y₁`):

* `rank-mono-<ᵇ-+1-via-target` — parametric in the target-side
  additive-principal closure.  Consumer supplies the closure witness
  at each call site (depending on `y₁`'s shape).
* `rank-mono-<ᵇ-+1-Ω-target` — convenience for `y₁ = bOmega μ`
  (target's left summand is an Ω-marker).  Uses
  `additive-principal-ω-rank-pow {μ}`.
* `rank-mono-<ᵇ-+1-ψ-target` — convenience for `y₁ = bpsi ν α`.
  Same closure via the provisional `rank-pow (bpsi ν _) = ω-rank-pow ν`.

## Why parametric

`rank-pow y₁` is additive principal exactly when `y₁` is atomic
(`bOmega` or `bpsi`).  For `y₁ = bplus z₁ z₂`, `rank-pow y₁ = rank-pow
z₁ ⊕ rank-pow z₂` is NOT additive principal in general; that
sub-case needs a coarser dominator function or richer rank shape.
The parametric primitive lets consumers handle atomic-`y₁` cases
cleanly while leaving the bplus-`y₁` sub-case explicitly deferred.

## Proof shape

For atomic-target case:

  rank x₂ ≤′ rank x₁ <′ rank y₁   (premise + WfCNF tail)
  ⇒ both <′ rank y₁
  ⇒ rank x₁ ⊕ rank x₂ <′ rank y₁   (additive-principal at y₁)
  ≤′ rank (bplus y₁ y₂)            (⊕-left-≤-sum)

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

proofs/agda/Ordinal/Buchholz/RankPow.agda

@@ -349,3 +349,72 @@ 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
+
+----------------------------------------------------------------------
+-- `<ᵇ-+1` via a caller-supplied target-additive-principal witness
+----------------------------------------------------------------------
+
+-- `bplus x₁ x₂ <ᵇ bplus y₁ y₂` from `x₁ <ᵇ y₁` is the `<ᵇ-+1`
+-- constructor.  The rank-mono conclusion `rank-pow (bplus x₁ x₂) <′
+-- rank-pow (bplus y₁ y₂)` requires `rank-pow y₁` to be additive
+-- principal (in the sense that `α, β <′ rank-pow y₁` forces
+-- `α ⊕ β <′ rank-pow y₁`).  For atomic `y₁ ∈ {bOmega μ, bpsi ν _}`,
+-- `rank-pow y₁ = ω-rank-pow _` IS additive principal and the consumer
+-- supplies `additive-principal-ω-rank-pow`.  For `y₁ = bplus z₁ z₂`,
+-- `rank-pow y₁` is not additive principal in general; that sub-case
+-- needs a coarser dominator function and is deferred.
+--
+-- The primitive below is parametric in the additive-principal
+-- witness, so the consumer pattern-matches on `y₁`'s constructor and
+-- supplies the appropriate witness at each call site.
+
+rank-mono-<ᵇ-+1-via-target : ∀ {x₁ x₂ y₁ y₂}
+  → (target-add : ∀ {α β}
+       → α <′ rank-pow y₁
+       → β <′ rank-pow y₁
+       → α ⊕ β <′ rank-pow y₁)
+  → rank-pow x₁ <′ rank-pow y₁          -- IH on `x₁ <ᵇ y₁`
+  → rank-pow x₂ ≤′ rank-pow x₁          -- WfCNF source tail bound
+  → rank-pow (bplus x₁ x₂) <′ rank-pow (bplus y₁ y₂)
+rank-mono-<ᵇ-+1-via-target {x₁} {x₂} {y₁} {y₂} target-add rx<ry rx₂≤rx₁ =
+  let
+    -- rank x₂ ≤′ rank x₁ <′ rank y₁ gives rank x₂ <′ rank y₁
+    rx₂<ry : rank-pow x₂ <′ rank-pow y₁
+    rx₂<ry = ≤′-trans
+               {osuc (rank-pow x₂)} {osuc (rank-pow x₁)} {rank-pow y₁}
+               rx₂≤rx₁
+               rx<ry
+
+    -- additive-principal closure on the target: both summands <′ y₁,
+    -- so their ⊕-sum is also <′ y₁.
+    sum<ry : rank-pow x₁ ⊕ rank-pow x₂ <′ rank-pow y₁
+    sum<ry = target-add rx<ry rx₂<ry
+
+    -- y₁ ≤′ y₁ ⊕ y₂ by left-≤-sum.
+    ry≤target : rank-pow y₁ ≤′ rank-pow (bplus y₁ y₂)
+    ry≤target = ⊕-left-≤-sum {rank-pow y₁} (rank-pow y₂)
+  in
+    ≤′-trans
+      {osuc (rank-pow x₁ ⊕ rank-pow x₂)} {rank-pow y₁} {rank-pow (bplus y₁ y₂)}
+      sum<ry
+      ry≤target
+
+-- Convenience: when the target's leading subterm is `bOmega μ`, the
+-- consumer can directly supply `additive-principal-ω-rank-pow {μ}`.
+-- Same for `bpsi ν _` via the provisional shape.
+
+rank-mono-<ᵇ-+1-Ω-target : ∀ {x₁ x₂ μ y₂}
+  → rank-pow x₁ <′ ω-rank-pow μ
+  → rank-pow x₂ ≤′ rank-pow x₁
+  → rank-pow (bplus x₁ x₂) <′ rank-pow (bplus (bOmega μ) y₂)
+rank-mono-<ᵇ-+1-Ω-target {x₁} {x₂} {μ} {y₂} =
+  rank-mono-<ᵇ-+1-via-target {x₁} {x₂} {bOmega μ} {y₂}
+    (additive-principal-ω-rank-pow {μ})
+
+rank-mono-<ᵇ-+1-ψ-target : ∀ {x₁ x₂ ν α y₂}
+  → rank-pow x₁ <′ ω-rank-pow ν
+  → rank-pow x₂ ≤′ rank-pow x₁
+  → rank-pow (bplus x₁ x₂) <′ rank-pow (bplus (bpsi ν α) y₂)
+rank-mono-<ᵇ-+1-ψ-target {x₁} {x₂} {ν} {α} {y₂} =
+  rank-mono-<ᵇ-+1-via-target {x₁} {x₂} {bpsi ν α} {y₂}
+    (additive-principal-ω-rank-pow {ν})

proofs/agda/Smoke.agda

@@ -486,6 +486,9 @@ open import Ordinal.Buchholz.RankPow using
   ; rank-mono-<ᵇ-ψ+
   ; rank-mono-<ᵇ-+Ω
   ; rank-mono-<ᵇ-+ψ
+  ; rank-mono-<ᵇ-+1-via-target
+  ; rank-mono-<ᵇ-+1-Ω-target
+  ; rank-mono-<ᵇ-+1-ψ-target
   )
 
 open import Ordinal.OmegaMarkers using