proof(Slice 3+4 Route A): (b) lex-first primitive + bpsi sub-case discharge

Extends `Ordinal.Buchholz.RankLexJointBplus` with three primitives
advancing the rank-lex-jb pivot's (a)+(b)+(c) assembly plan beyond
the (a) primitive that PR #147 shipped.  No structural commitments,
no funext, zero postulates, `--safe --without-K` throughout.

## Three primitives added

1. `rank-lex-jb-strict-first` (leg (b), trivial at primitive level)
   — given `rank-pow (bplus x₁ x₂) <′ rank-pow (bplus y₁ y₂)`,
   fires `<lex-first`.  One-line proof.  The load-bearing content
   is consumer-side derivation of the hypothesis, which remains
   the multi-PR ordinal-arithmetic challenge (both pre-identified
   unblock routes — additive-principal closure on a generic sum,
   strict-left-mono of `_⊕_` — CHECKED-REFUTED in PR #146).
   Shipping the primitive separates trivial lex-rank wiring from
   the structural ordinal-arithmetic blocker.

2. `leftmost-α-strict-from-bpsi-source` (consumer helper) — given
   `α <ᵇ⁰ β` on the ψ-arguments, derives `leftmost-α (bplus
   (bpsi ν α) x₂) <′ leftmost-α (bplus (bpsi ν β) y₂)`.  Composes
   `leftmost-α-bplus` + `leftmost-α-bpsi` (both definitional) with
   `RankMonoUmbrella.rank-pow-mono-<ᵇ⁰`.  Parameterised in
   `_<ᵇ⁰_` (10-constructor umbrella) — the bpsi sub-case requires
   no constructor `_<ᵇ⁰_` doesn't already have.

3. `rank-lex-jb-bpsi-at-equality` (named theorem) — composition
   of `rank-lex-jb-strict-second-at-equal-first` (PR #147, leg (a))
   with `leftmost-α-strict-from-bpsi-source`.  Given the
   FIRST-COMPONENT EQUALITY (consumer-derived, gating obligation)
   plus the source-side `α <ᵇ⁰ β`, fires `<lex-second` at equal
   first components with the leftmost-α strict witness.  Closes
   the bpsi-source-at-equality sub-case at the rank-lex-jb level,
   parallel to `RankLexSlice3.rank-lex-bpsi-strict-at-equality`'s
   role for `rank-lex`.

## Where this sits in the assembly

Per the PR #147 module preamble's `(a)+(b)+(c)` plan:
- (a) equal-first lex-second leg — CLOSED in PR #147.
- (b) strict-first lex-first leg — primitive CLOSED here;
  consumer-side derivation of `rank-pow (bplus _ _) <′ rank-pow
  (bplus _ _)` remains the multi-PR challenge.
- (c) first-component trichotomy — STILL OPEN (Ord-valued
  decidability bridge in `Phase13` not yet attempted; `with`-based
  case-analysis over `_<′_` / `_≡_` is the sketched alternative).
- Assembly into full `<ᵇ-+1`-at-equal-head headline = multi-PR
  follow-on, still gated on (c).

This slice records that every other discharge step composes
cleanly (the bpsi sub-case now ships as a named theorem under
the first-eq hypothesis); resolving the gating obligations
unblocks the headline mechanically.

## Honest scope notes (preserved in module)

- The trivial `<lex-first` shape of primitive (1) does not mean
  leg (b) is "done" — the consumer plumbing is the hard part.
- Primitive (2) is `_<ᵇ⁰_`-parameterised, not `_<ᵇ_`-parameterised.
  Lifting to full `_<ᵇ_` requires the joint-bplus closure that
  the rank-lex-jb pivot was designed to attack.
- Primitive (3) requires the first-eq hypothesis as input;
  consumer-side derivation is documented as still-gating per
  the file preamble.

## Local verification

- `agda -i proofs/agda proofs/agda/Ordinal/Buchholz/RankLexJointBplus.agda` — clean.
- `agda -i proofs/agda proofs/agda/Ordinal/Buchholz/Smoke.agda` — clean, exit 0.
- `agda -i proofs/agda proofs/agda/Smoke.agda` — clean, exit 0.
- `agda -i proofs/agda proofs/agda/All.agda` — clean, exit 0.
- `bash tools/check-guardrails.sh proofs/agda` — 160 modules pass.
- `sh scripts/kernel-guard.sh` — PASS.

All three primitives pinned in `Ordinal/Buchholz/Smoke.agda`
under the existing `RankLexJointBplus` `using` block.

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

Author: hyperpolymath

proofs/agda/Ordinal/Buchholz/RankLexJointBplus.agda

@@ -130,8 +130,13 @@ open import Ordinal.Buchholz.RankLex  using
   ( RankLex
   ; mkLex
   ; _<lex_
+  ; <lex-first
   ; <lex-second
   )
+open import Ordinal.Buchholz.RankMonoUmbrella using
+  ( _<ᵇ⁰_
+  ; rank-pow-mono-<ᵇ⁰
+  )
 
 ----------------------------------------------------------------------
 -- `leftmost-α : BT → Ord` — the leftmost-ψ-α-rank discriminator
@@ -273,3 +278,97 @@ rank-lex-jb-strict-second-at-equal-first {x₁} {x₂} {y₁} {y₂} first-eq st
     -- Local `sym` to avoid an extra stdlib import.
     sym-≡ : ∀ {ℓ} {A : Set ℓ} {a b : A} → a ≡ b → b ≡ a
     sym-≡ refl = refl
+
+----------------------------------------------------------------------
+-- Headline: `<lex-first` at strict first components (leg (b))
+----------------------------------------------------------------------
+
+-- The companion primitive to `rank-lex-jb-strict-second-at-equal-
+-- first`.  Trivial at the rank-lex-jb level: `<lex-first` fires
+-- directly on the supplied strict first-component witness.  The
+-- LOAD-BEARING content is the consumer-side derivation of the
+-- hypothesis `rank-pow (bplus x₁ x₂) <′ rank-pow (bplus y₁ y₂)`
+-- from a source `<ᵇ` derivation, which remains the multi-PR
+-- ordinal-arithmetic challenge documented in this module's
+-- preamble (both pre-identified unblock routes — additive-principal
+-- closure on a generic sum, strict-left-mono of `_⊕_` — are
+-- CHECKED-REFUTED in `Ordinal.Brouwer.{AdditivePrincipalGenericRefuted,
+-- StrictLeftMonoRefuted}` (PR #146, 2026-05-28)).  Shipping the
+-- primitive separates the trivial lex-rank wiring from the
+-- structural ordinal-arithmetic blocker — consumers that derive
+-- strict-first via a future bypass (or a restricted bplus-shape
+-- where rank-pow IS additive principal) fire `<lex-first` through
+-- this primitive without re-discovering the wiring.
+
+rank-lex-jb-strict-first :
+  ∀ {x₁ x₂ y₁ y₂}
+  → rank-pow (bplus x₁ x₂) <′ rank-pow (bplus y₁ y₂)
+  → rank-lex-jb (bplus x₁ x₂) <lex rank-lex-jb (bplus y₁ y₂)
+rank-lex-jb-strict-first strict = <lex-first strict
+
+----------------------------------------------------------------------
+-- Consumer helper: leftmost-α strict-mono from a bpsi-source `<ᵇ⁰`
+----------------------------------------------------------------------
+
+-- The bpsi-source-at-equality bplus-chain sub-case has
+-- `x₁ = bpsi ν α` and `y₁ = bpsi ν β` (same ν per the sub-case
+-- definition).  Given the source-side `α <ᵇ⁰ β` derivation, the
+-- leftmost-α discriminator on both bplus chains specialises:
+--
+--   leftmost-α (bplus (bpsi ν α) x₂) = leftmost-α (bpsi ν α)
+--                                    = rank-pow α
+--   leftmost-α (bplus (bpsi ν β) y₂) = rank-pow β
+--
+-- and `rank-pow α <′ rank-pow β` follows from
+-- `RankMonoUmbrella.rank-pow-mono-<ᵇ⁰` on the supplied `α <ᵇ⁰ β`.
+-- The reductions `leftmost-α-bplus` + `leftmost-α-bpsi` are
+-- definitional, so the helper is a one-step inhabitation: the
+-- supplied `<′` is already the goal's `<′` modulo definitional
+-- reduction on `leftmost-α`.
+--
+-- Honest scope: parameterised in `_<ᵇ⁰_`, not `_<ᵇ_`.  The
+-- 10-constructor `_<ᵇ⁰_` umbrella covers the bpsi sub-case (no
+-- `<ᵇ-+1` joint-bplus constructor in `_<ᵇ⁰_`), so consumers with
+-- a `_<ᵇ⁰_` derivation on the ψ-arguments compose directly.
+-- Lifting to the full `_<ᵇ_` would need the joint-bplus closure,
+-- which is the very problem this rank-lex-jb pivot was designed
+-- to attack.
+
+leftmost-α-strict-from-bpsi-source :
+  ∀ {ν α β x₂ y₂}
+  → α <ᵇ⁰ β
+  → leftmost-α (bplus (bpsi ν α) x₂) <′ leftmost-α (bplus (bpsi ν β) y₂)
+leftmost-α-strict-from-bpsi-source α<β = rank-pow-mono-<ᵇ⁰ α<β
+
+----------------------------------------------------------------------
+-- Named theorem: bpsi-source-at-equality sub-case at rank-lex-jb
+----------------------------------------------------------------------
+
+-- Composition of `rank-lex-jb-strict-second-at-equal-first` with
+-- `leftmost-α-strict-from-bpsi-source`.  Given:
+--
+--   * the FIRST-COMPONENT EQUALITY `rank-pow (bplus (bpsi ν α) x₂)
+--     ≡ rank-pow (bplus (bpsi ν β) y₂)` — consumer's input, gated
+--     on the structurally-blocked bplus-chain sum-bound work; AND
+--   * the source-side `α <ᵇ⁰ β` derivation on the ψ-arguments,
+--
+-- the headline fires `<lex-second` at equal first components with
+-- the leftmost-α strict witness.  This is the bpsi-source-at-
+-- equality sub-case CLOSED at the rank-lex-jb level (parallel to
+-- `RankLexSlice3.rank-lex-bpsi-strict-at-equality` for `rank-lex`).
+--
+-- The first-eq hypothesis remains the gating obligation; this
+-- theorem records that EVERY other discharge step composes
+-- cleanly, so resolving the structural blocker unblocks the named
+-- theorem mechanically.
+
+rank-lex-jb-bpsi-at-equality :
+  ∀ {ν α β x₂ y₂}
+  → rank-pow (bplus (bpsi ν α) x₂) ≡ rank-pow (bplus (bpsi ν β) y₂)
+  → α <ᵇ⁰ β
+  → rank-lex-jb (bplus (bpsi ν α) x₂) <lex rank-lex-jb (bplus (bpsi ν β) y₂)
+rank-lex-jb-bpsi-at-equality {ν} {α} {β} {x₂} {y₂} first-eq α<β =
+  rank-lex-jb-strict-second-at-equal-first
+    {x₁ = bpsi ν α} {x₂ = x₂} {y₁ = bpsi ν β} {y₂ = y₂}
+    first-eq
+    (leftmost-α-strict-from-bpsi-source {ν = ν} {α = α} {β = β} {x₂ = x₂} {y₂ = y₂} α<β)

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -536,6 +536,9 @@ open import Ordinal.Buchholz.RankLexJointBplus using
   ( leftmost-α
   ; rank-lex-jb
   ; rank-lex-jb-strict-second-at-equal-first
+  ; rank-lex-jb-strict-first
+  ; leftmost-α-strict-from-bpsi-source
+  ; rank-lex-jb-bpsi-at-equality
   )
 
 -- Slice 4 narrowing 2026-05-28 (own block per CLAUDE.md Working