proof(ordinal): doubled-ladder bplus-on-left rank2-mono primitives (+Ω, +ψ, +1) — all 12 constructors (#207)

## What

Closes the per-constructor `rank2`-monotonicity family for the
**bplus-on-left** constructors of the core `_<ᵇ_` — with these, **all 12
constructors** now have a `rank2`-mono primitive. Two commits:

**1. Ω-block additive principality + `<ᵇ-+Ω`**
(`RankDoubledLadderAddPrincipal.agda`)

```agda
additive-principal-base            : ∀ {B α β} → α <′ olim (λ k → B ·ℕ k)
                                     → β <′ olim (λ k → B ·ℕ k) → α ⊕ β <′ olim (λ k → B ·ℕ k)
additive-principal-ω-rank-pow-succ : ∀ {μ α β} → α <′ ω-rank-pow-succ μ
                                     → β <′ ω-rank-pow-succ μ → α ⊕ β <′ ω-rank-pow-succ μ
rank2-mono-+Ω : rank2 x <′ rank2 (bOmega μ) → rank2 y <′ rank2 (bOmega μ)
              → rank2 (bplus x y) <′ rank2 (bOmega μ)
```

The bplus-on-left constructors compare a **sum** `rank2 x ⊕ rank2 y`
against the target, so the target must absorb the sum.
`RankPow.additive-principal-ω-rank-pow` already covers the ψ-block
target; this adds the Ω-block target — fin via the clean ω-power
`ω^(suc(suc n))`, ω via `additive-principal-base` (the original proof
re-stated over an arbitrary base, since it uses only `·ℕ-add-≤ {B}` +
`⊕`-monotonicities) instantiated at `ω-rank-pow ω`.

**2. `<ᵇ-+ψ`, `<ᵇ-+1`** (`RankDoubledLadderMonoPlus2.agda`)

```agda
rank2-mono-+ψ : rank2 x <′ ω-rank-pow (double ν) → rank2 y <′ ω-rank-pow (double ν)
              → rank2 (bplus x y) <′ rank2 (bpsi ν α)
rank2-mono-+1 : rank2 (bplus x₁ x₂) <′ rank2 y₁
              → rank2 (bplus x₁ x₂) <′ rank2 (bplus y₁ y₂)
```

`+ψ` uses the ψ-block additive principality; `+1` (joint-bplus) is pure
`⊕`-left-weakening once the source sum is below the target head.

All primitives stated relation-agnostically (premises = recursive/tail
bounds), per the established RankPow discipline.

## Progress

**12 of 12** core `_<ᵇ_` constructors now have a `rank2`-mono primitive.
Remaining capstone: the umbrella `rank2-mono : WfAdm x → WfAdm y → x <ᵇ
y → rank2 x <′ rank2 y` (structural recursion discharging each
primitive's premises, with a `rank2-mono-≤` tail companion for `y ≤ᵇ
x`), then the `wf-<′`-transport headline `wf-<ᵇ`.

## Verification

- `agda -i proofs/agda proofs/agda/All.agda` exits 0 under `--safe
--without-K`.
- Headlines pinned in the Buchholz `Smoke.agda` (own blocks).
- Zero postulates / escape pragmas.

https://claude.ai/code/session_017t53M7W7ubmXpwymveLcCE

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

proofs/agda/All.agda

@@ -155,6 +155,8 @@ open import Ordinal.Buchholz.RankPowSlice3Headline
 open import Ordinal.Buchholz.RankDoubledLadder
 open import Ordinal.Buchholz.RankDoubledLadderMono
 open import Ordinal.Buchholz.RankDoubledLadderMonoPlus
+open import Ordinal.Buchholz.RankDoubledLadderAddPrincipal
+open import Ordinal.Buchholz.RankDoubledLadderMonoPlus2
 open import Ordinal.Buchholz.RankMonoUmbrella
 open import Ordinal.Buchholz.RankMonoUmbrellaSlice3
 open import Ordinal.Buchholz.RankMonoUmbrellaSlice4

proofs/agda/Ordinal/Buchholz/RankDoubledLadderAddPrincipal.agda

@@ -0,0 +1,136 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+-- Doubled-ladder rank monotonicity — additive-principality of the
+-- Ω-block target + the `<ᵇ-+Ω` primitive (2026-06-14).
+--
+-- ## Why this exists
+--
+-- The bplus-ON-LEFT constructors (`<ᵇ-+Ω`, `<ᵇ-+ψ`, `<ᵇ-+1`) compare
+-- a SUM `rank2 x ⊕ rank2 y` against the target rank.  Closing them
+-- needs the target to ABSORB the sum — i.e. additive principality of
+-- the target rank.  This slice supplies that for the Ω-block target
+-- `ω-rank-pow-succ (double μ) = rank2 (bOmega μ)`, and uses it to
+-- discharge the first of the three, `<ᵇ-+Ω`.
+--
+-- `RankPow.additive-principal-ω-rank-pow` already gives additive
+-- principality for the ψ-block target `ω-rank-pow μ`.  The Ω-block
+-- target `ω-rank-pow-succ μ` needs its own proof:
+--
+--   * fin branch — `ω-rank-pow-succ (fin n) = ω^(suc (suc n))` is a
+--     clean ω-power, so the existing `OmegaPow.additive-principal`
+--     (additive principality of `ω^(suc k)`) applies at `k = suc n`.
+--   * ω branch — `ω-rank-pow-succ ω = olim (λ n → ω-rank-pow ω ·ℕ n)`
+--     (= ω^(ω+1)) has the SAME limit shape `olim (λ k → B ·ℕ k)` that
+--     `OmegaPow.additive-principal` exploits, only with base
+--     `B = ω-rank-pow ω` instead of `ω^ n`.  The proof there is
+--     generic in the base (it uses only `·ℕ-add-≤ {B}` and the `⊕`
+--     monotonicities), so this module re-states it once as
+--     `additive-principal-base` over an arbitrary base and instantiates
+--     at `B = ω-rank-pow ω`.
+--
+-- ## Honest scope
+--
+-- Lands `additive-principal-base`, `additive-principal-ω-rank-pow-succ`,
+-- and the `<ᵇ-+Ω` rank2-mono primitive `rank2-mono-+Ω`.  The two
+-- remaining bplus-on-left cases (`<ᵇ-+ψ`, `<ᵇ-+1`) have NON-ω-power
+-- targets (a ψ-block sum / a bplus sum) and need the tail-ordering
+-- machinery (`y ≤ᵇ x` → rank bound) — deferred to the umbrella slice.
+--
+-- ## Headlines (pin in `Ordinal/Buchholz/Smoke.agda`)
+--
+--   * `additive-principal-ω-rank-pow-succ`
+--   * `rank2-mono-+Ω`
+
+module Ordinal.Buchholz.RankDoubledLadderAddPrincipal where
+
+open import Data.Nat                       using (ℕ; suc; _+_)
+open import Data.Product.Base              using (_,_)
+
+open import Ordinal.Brouwer               using (Ord; osuc; olim)
+open import Ordinal.Brouwer.Phase13       using
+  ( _<′_
+  ; _≤′_
+  ; ≤′-trans
+  ; ≤′-self-osuc
+  ; ⊕-mono-≤-left
+  ; ⊕-mono-<-right
+  )
+open import Ordinal.Brouwer.Arithmetic    using (_⊕_)
+open import Ordinal.Brouwer.OmegaPow       using (_·ℕ_; ·ℕ-add-≤; additive-principal)
+open import Ordinal.OmegaMarkers          using (OmegaIndex; fin; ω)
+open import Ordinal.Buchholz.Syntax       using (BT; bOmega; bplus)
+open import Ordinal.Buchholz.RankPow       using (ω-rank-pow; ω-rank-pow-succ)
+open import Ordinal.Buchholz.RankDoubledLadder using (rank2; double)
+
+----------------------------------------------------------------------
+-- Base-generic additive principality of `olim (λ k → B ·ℕ k)`
+----------------------------------------------------------------------
+
+-- A re-statement of `OmegaPow.additive-principal` over an ARBITRARY
+-- base `B`.  The original proof at `OmegaPow.agda:361` uses only
+-- `·ℕ-add-≤ {B}` and the `⊕`-monotonicities — nothing specific to
+-- `B = ω^ n` — so it transfers verbatim with `ω^ n ↦ B`.  Needed for
+-- the ω-marker Ω-block target `ω-rank-pow-succ ω =
+-- olim (λ n → ω-rank-pow ω ·ℕ n)`.
+additive-principal-base : ∀ {B α β}
+  → α <′ olim (λ k → B ·ℕ k)
+  → β <′ olim (λ k → B ·ℕ k)
+  → α ⊕ β <′ olim (λ k → B ·ℕ k)
+additive-principal-base {B} {α} {β} (kα , sα) (kβ , sβ) = kβ + kα , proof
+  where
+  α≤′kα : α ≤′ B ·ℕ kα
+  α≤′kα = ≤′-trans {α} {osuc α} {B ·ℕ kα} (≤′-self-osuc α) sα
+
+  step1 : α ⊕ β ≤′ (B ·ℕ kα) ⊕ β
+  step1 = ⊕-mono-≤-left {α} {B ·ℕ kα} {β} α≤′kα
+
+  step2 : osuc ((B ·ℕ kα) ⊕ β) ≤′ (B ·ℕ kα) ⊕ (B ·ℕ kβ)
+  step2 = ⊕-mono-<-right {B ·ℕ kα} {β} {B ·ℕ kβ} sβ
+
+  step3 : (B ·ℕ kα) ⊕ (B ·ℕ kβ) ≤′ B ·ℕ (kβ + kα)
+  step3 = ·ℕ-add-≤ {B} kα kβ
+
+  proof : osuc (α ⊕ β) ≤′ B ·ℕ (kβ + kα)
+  proof =
+    ≤′-trans
+      {osuc (α ⊕ β)} {(B ·ℕ kα) ⊕ (B ·ℕ kβ)} {B ·ℕ (kβ + kα)}
+      (≤′-trans
+        {osuc (α ⊕ β)} {osuc ((B ·ℕ kα) ⊕ β)} {(B ·ℕ kα) ⊕ (B ·ℕ kβ)}
+        step1 step2)
+      step3
+
+----------------------------------------------------------------------
+-- Additive principality of the Ω-block target `ω-rank-pow-succ μ`
+----------------------------------------------------------------------
+
+-- The Ω-block analogue of `RankPow.additive-principal-ω-rank-pow`.
+-- fin: reuse `OmegaPow.additive-principal` at the doubled successor
+-- exponent; ω: instantiate `additive-principal-base` at the base
+-- `ω-rank-pow ω`.
+additive-principal-ω-rank-pow-succ : ∀ {μ α β}
+  → α <′ ω-rank-pow-succ μ
+  → β <′ ω-rank-pow-succ μ
+  → α ⊕ β <′ ω-rank-pow-succ μ
+additive-principal-ω-rank-pow-succ {fin n} pα pβ =
+  additive-principal {suc n} pα pβ
+additive-principal-ω-rank-pow-succ {ω}     pα pβ =
+  additive-principal-base {ω-rank-pow ω} pα pβ
+
+----------------------------------------------------------------------
+-- The `<ᵇ-+Ω` rank2-mono primitive
+----------------------------------------------------------------------
+
+-- `<ᵇ-+Ω : x <ᵇ bOmega μ → bplus x y <ᵇ bOmega μ`.  The whole sum
+-- `rank2 x ⊕ rank2 y` lands below the Ω-block target when BOTH
+-- summands do — the left bound is the IH on the sub-derivation
+-- `x <ᵇ bOmega μ`, the right bound is the tail bound (from `y ≤ᵇ x`,
+-- supplied by the umbrella consumer).  Stated relation-agnostically:
+-- both bounds are premises.
+rank2-mono-+Ω : ∀ {x y μ}
+  → rank2 x <′ rank2 (bOmega μ)
+  → rank2 y <′ rank2 (bOmega μ)
+  → rank2 (bplus x y) <′ rank2 (bOmega μ)
+rank2-mono-+Ω {x} {y} {μ} px py =
+  additive-principal-ω-rank-pow-succ {double μ} px py

proofs/agda/Ordinal/Buchholz/RankDoubledLadderMonoPlus2.agda

@@ -0,0 +1,89 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+-- Doubled-ladder rank monotonicity — the last two bplus-on-left
+-- primitives `<ᵇ-+ψ`, `<ᵇ-+1` (2026-06-14).
+--
+-- ## Why this exists
+--
+-- With `<ᵇ-+Ω` closed (`RankDoubledLadderAddPrincipal`), the two
+-- remaining bplus-on-left constructors of the core `_<ᵇ_` are:
+--
+--   * `<ᵇ-+ψ : x <ᵇ bpsi ν α → bplus x y <ᵇ bpsi ν α`
+--   * `<ᵇ-+1 : x₁ <ᵇ y₁ → bplus x₁ x₂ <ᵇ bplus y₁ y₂`
+--
+-- Both ship as relation-agnostic `rank2`-mono primitives — the same
+-- discipline as the rest of the family.  The genuinely-hard content
+-- (discharging the premise bounds from the WfCNF tail order `y ≤ᵇ x`
+-- and the sub-derivations) lives in the umbrella that consumes these;
+-- the primitives themselves are pure `⊕`-arithmetic:
+--
+--   * `<ᵇ-+ψ` — the ψ-block leading power `ω-rank-pow (double ν)` is
+--     additive principal (`RankPow.additive-principal-ω-rank-pow`), so
+--     if BOTH source summands rank below it, their sum does too, and
+--     the target ψ-rank only ADDS its argument on the right.
+--   * `<ᵇ-+1` — if the WHOLE source sum ranks below the target's HEAD
+--     `rank2 y₁`, then it ranks below the target sum (the target's tail
+--     only adds).
+--
+-- ## Completion
+--
+-- With these two, ALL 12 core `_<ᵇ_` constructors have a `rank2`-mono
+-- primitive.  The follow-on is the umbrella
+-- `rank2-mono : WfAdm x → WfAdm y → x <ᵇ y → rank2 x <′ rank2 y`
+-- (structural recursion that discharges each primitive's premises,
+-- needing a `rank2-mono-≤` tail-bound companion for `y ≤ᵇ x`) and the
+-- `wf-<′`-transport headline `wf-<ᵇ`.
+--
+-- ## Headlines (pin in `Ordinal/Buchholz/Smoke.agda`)
+--
+--   * `rank2-mono-+ψ`
+--   * `rank2-mono-+1`
+
+module Ordinal.Buchholz.RankDoubledLadderMonoPlus2 where
+
+open import Ordinal.Brouwer.Phase13       using (_<′_; ⊕-left-≤-sum)
+open import Ordinal.Brouwer.Arithmetic    using (_⊕_)
+open import Ordinal.Buchholz.Syntax       using (BT; bpsi; bplus)
+open import Ordinal.Buchholz.RankPow       using (ω-rank-pow; additive-principal-ω-rank-pow)
+open import Ordinal.Buchholz.RankDoubledLadder using (rank2; double)
+open import Ordinal.Buchholz.RankDoubledLadderMono using (<′-≤′-trans)
+
+----------------------------------------------------------------------
+-- `<ᵇ-+ψ` — bplus source against a ψ target
+----------------------------------------------------------------------
+
+-- `<ᵇ-+ψ : x <ᵇ bpsi ν α → bplus x y <ᵇ bpsi ν α`.  The ψ-block
+-- leading power `ω-rank-pow (double ν)` is additive principal, so
+-- both source summands ranking below it makes the sum rank below it;
+-- the target ψ-rank `ω-rank-pow (double ν) ⊕ rank2 α` then only adds.
+-- Premises (supplied by the umbrella): the left bound is the IH on
+-- `x <ᵇ bpsi ν α`, the right is the tail bound from `y ≤ᵇ x`.
+rank2-mono-+ψ : ∀ {x y ν α}
+  → rank2 x <′ ω-rank-pow (double ν)
+  → rank2 y <′ ω-rank-pow (double ν)
+  → rank2 (bplus x y) <′ rank2 (bpsi ν α)
+rank2-mono-+ψ {x} {y} {ν} {α} px py =
+  <′-≤′-trans {rank2 x ⊕ rank2 y} {ω-rank-pow (double ν)}
+              {ω-rank-pow (double ν) ⊕ rank2 α}
+    (additive-principal-ω-rank-pow {double ν} px py)
+    (⊕-left-≤-sum {ω-rank-pow (double ν)} (rank2 α))
+
+----------------------------------------------------------------------
+-- `<ᵇ-+1` — joint bplus
+----------------------------------------------------------------------
+
+-- `<ᵇ-+1 : x₁ <ᵇ y₁ → bplus x₁ x₂ <ᵇ bplus y₁ y₂`.  If the WHOLE
+-- source sum ranks below the target's HEAD `rank2 y₁`, it ranks below
+-- the target sum (the target tail `rank2 y₂` only adds on the right).
+-- The premise — source sum below target head — is what the umbrella
+-- derives from `x₁ <ᵇ y₁` plus the tail order `x₂ ≤ᵇ x₁`; this is the
+-- joint-bplus discharge the doubled ladder was ultimately built for.
+rank2-mono-+1 : ∀ {x₁ x₂ y₁ y₂}
+  → rank2 (bplus x₁ x₂) <′ rank2 y₁
+  → rank2 (bplus x₁ x₂) <′ rank2 (bplus y₁ y₂)
+rank2-mono-+1 {x₁} {x₂} {y₁} {y₂} p =
+  <′-≤′-trans {rank2 x₁ ⊕ rank2 x₂} {rank2 y₁} {rank2 y₁ ⊕ rank2 y₂}
+    p
+    (⊕-left-≤-sum {rank2 y₁} (rank2 y₂))

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -496,6 +496,21 @@ open import Ordinal.Buchholz.RankDoubledLadderMonoPlus using
   ; rank2-mono-ψ+
   )
 
+-- Doubled-ladder Ω-block additive principality + the `<ᵇ-+Ω`
+-- primitive (own block per CLAUDE.md Working rules).
+open import Ordinal.Buchholz.RankDoubledLadderAddPrincipal using
+  ( additive-principal-ω-rank-pow-succ
+  ; rank2-mono-+Ω
+  )
+
+-- Doubled-ladder last two bplus-on-left primitives `<ᵇ-+ψ`, `<ᵇ-+1`
+-- (own block per CLAUDE.md Working rules) — completes all 12
+-- core `_<ᵇ_` constructors' rank2-mono primitives.
+open import Ordinal.Buchholz.RankDoubledLadderMonoPlus2 using
+  ( rank2-mono-+ψ
+  ; rank2-mono-+1
+  )
+
 -- Slice 3 prerequisites (own block per CLAUDE.md Working rules):
 -- the left-spine NonBzero predicate, the strict-jump bridge from
 -- `μ <Ω ν` to `ω-rank-pow-succ μ ≤′ ω-rank-pow ν`, and the head-Ω