proof(Slice 3+4 Route A): (c) trichotomy + consumer-side first-eq derivation

Follow-on to PR #165's (b) primitive.  Adds the (c) trichotomy
data type and the consumer-side first-eq derivation tools that
the (a)+(b)+(c) assembly plan calls for, plus a named theorem
fully closing the bpsi-source-at-equal-head sub-case at the
rank-lex-jb level GIVEN only a tail-rank-equality discharge.
Zero postulates, `--safe --without-K`, no funext.

## Two consumer-side first-eq derivation tools

The DEFINITIONAL fact underlying the closure: `rank-pow (bplus
x y) = rank-pow x ⊕ rank-pow y` (`RankPow.rank-pow-bplus`, `refl`).
So first-eq REDUCES to a conjunction of summand-level equalities
via `cong₂ _⊕_`.

1. `rank-pow-bplus-eq-from-summands` — generic `cong₂ _⊕_` helper:
   from two summand-equalities derive bplus-eq.

2. `first-eq-from-bpsi-source-at-equal-head` — specialised for
   bpsi-source-at-equal-head: left summands are `bpsi ν α` and
   `bpsi ν β` (same ν, ANY α and β), so left-rank equality is
   DEFINITIONAL (`refl`).  Reduces consumer-side first-eq to the
   tail-rank-equality `rank-pow x₂ ≡ rank-pow y₂`.

## (c) Trichotomy data type + dispatchers

Brouwer ordinals are NOT decidably ordered in general
(`Ord` carries `olim f` over arbitrary ℕ → Ord functions), so a
universal trichotomy on `rank-pow (bplus _ _)` is unattainable
under `--safe --without-K` without postulates.  The TRACTABLE
narrowing is a STRUCTURAL trichotomy data type that records the
strict / equal cases the consumer can derive:

* `BplusFirstTri x₁ x₂ y₁ y₂` — two constructors:
  - `bplus-tri-strict : rank-pow (bplus x₁ x₂) <′ rank-pow (bplus y₁ y₂)`
  - `bplus-tri-equal  : rank-pow (bplus x₁ x₂) ≡ rank-pow (bplus y₁ y₂)`

* `bplus-tri-from-strict` / `bplus-tri-from-equal` — wrapper
  constructors that lift consumer-derived witnesses into the
  trichotomy.

* `dispatch-trichotomy-to-<lex` — the assembly headline: consumes
  a trichotomy + a leftmost-α strict witness and produces a `<lex`
  judgment at rank-lex-jb level.  Strict case → `<lex-first` via
  `rank-lex-jb-strict-first` (PR #165); equal case → `<lex-second`
  via `rank-lex-jb-strict-second-at-equal-first` (PR #147).

This IS the (a)+(b)+(c) assembly's RECIPE at the rank-lex-jb
level: every reachable case dispatches mechanically given the
consumer-side strict-or-equal-first witness.  The residual
gating across the assembly is the consumer-side derivation of
the leftmost-α strict witness in the equal case AND tail-rank-
equality discharge.

## Named theorem: bpsi-source-at-equal-head fully discharged

`rank-lex-jb-bpsi-equal-head-from-tail-eq` composes the two
consumer-side derivations into a closure:

  Inputs:
    * `rank-pow x₂ ≡ rank-pow y₂` (tail-rank-eq, consumer gate)
    * `α <ᵇ⁰ β` (source-side strict ψ-arg, 10-constructor umbrella)
  Output:
    rank-lex-jb (bplus (bpsi ν α) x₂) <lex rank-lex-jb (bplus (bpsi ν β) y₂)

The tail-rank-equality gate is THE SAME structural obligation
that the ψ-rank-level closure (`RankLexSlice3.rank-adm-bpsi-
strict-at-equality`) carries.  Resolving that one structural
blocker unblocks BOTH the ψ-rank-level and the bplus-chain-
level closures mechanically.

## Honest scope (preserved in module)

- The Brouwer-arithmetic blocker (strict-left-mono of `_⊕_` +
  additive-principal closure on generic sums, both CHECKED-
  REFUTED in PR #146) means strict-first via strict-left-rank
  is structurally unreachable at the bplus-chain level.  Strict-
  first via strict-head-Ω already lands in PR #141 / `<ᵇ¹-+1-+`.
- Equal-first beyond the bpsi-source-at-equal-head case is the
  open multi-PR research; the trichotomy data type leaves room
  for future dispatchers without committing to any specific
  closure path.
- `dispatch-trichotomy-to-<lex` shows the assembly composes
  mechanically — the structural ordinal-arithmetic obligation
  is the SOLE remaining gating, and it's pushed to the precise
  consumer call site rather than scattered across the proof.

## 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 eleven new names 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

@@ -114,7 +114,7 @@
 
 module Ordinal.Buchholz.RankLexJointBplus where
 
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst; cong; cong₂)
 
 open import Ordinal.Brouwer           using (Ord; oz)
 open import Ordinal.Brouwer.Phase13   using (_<′_)
@@ -125,7 +125,8 @@ open import Ordinal.Buchholz.Syntax   using
   ; bplus
   ; bpsi
   )
-open import Ordinal.Buchholz.RankPow  using (rank-pow)
+open import Ordinal.Brouwer.Arithmetic using (_⊕_)
+open import Ordinal.Buchholz.RankPow  using (rank-pow; rank-pow-bplus; ω-rank-pow)
 open import Ordinal.Buchholz.RankLex  using
   ( RankLex
   ; mkLex
@@ -372,3 +373,168 @@ rank-lex-jb-bpsi-at-equality {ν} {α} {β} {x₂} {y₂} first-eq α<β =
     {x₁ = bpsi ν α} {x₂ = x₂} {y₁ = bpsi ν β} {y₂ = y₂}
     first-eq
     (leftmost-α-strict-from-bpsi-source {ν = ν} {α = α} {β = β} {x₂ = x₂} {y₂ = y₂} α<β)
+
+----------------------------------------------------------------------
+-- Consumer-side first-eq derivation
+----------------------------------------------------------------------
+
+-- The HARD half of the (a) primitive's consumer plumbing: deriving
+-- the `first-eq : rank-pow (bplus x₁ x₂) ≡ rank-pow (bplus y₁ y₂)`
+-- hypothesis at the bplus-chain rank-pow level.
+--
+-- The DEFINITIONAL fact underlying the closure: `rank-pow (bplus
+-- x y) = rank-pow x ⊕ rank-pow y` (`RankPow.rank-pow-bplus`,
+-- definitional `refl`).  So first-eq REDUCES to a conjunction of
+-- summand-level equalities via `cong₂ _⊕_`:
+--
+--   rank-pow x₁ ≡ rank-pow y₁  ∧  rank-pow x₂ ≡ rank-pow y₂
+--   ⇒ rank-pow (bplus x₁ x₂) ≡ rank-pow (bplus y₁ y₂)
+--
+-- The bpsi-source-at-equal-head sub-case has `x₁ = bpsi ν α` and
+-- `y₁ = bpsi ν β` (same ν).  At the rank-pow level both reduce
+-- DEFINITIONALLY to `ω-rank-pow ν`, so the left summand's equality
+-- is `refl` and the consumer's residual obligation collapses to
+-- `rank-pow x₂ ≡ rank-pow y₂` on the right summand.  Under WfCNF
+-- this is the same `rank-pow x₂ ≡ rank-pow y₂` discharge that
+-- already gates the lex-rank-level discharge of the same sub-case
+-- via `RankLexSlice3.rank-adm-bpsi-strict-at-equality`; the rank-
+-- pow-level closure has the same shape modulo the consumer-side
+-- ordinal-arithmetic gating, which means the bpsi sub-case at the
+-- bplus-chain level FOLLOWS the same closure ladder as the ψ-rank
+-- level once that ladder closes.
+
+-- Generic summand-equalities composer: bplus-first-eq from summand-
+-- first-eqs.
+rank-pow-bplus-eq-from-summands :
+  ∀ {x₁ x₂ y₁ y₂}
+  → rank-pow x₁ ≡ rank-pow y₁
+  → rank-pow x₂ ≡ rank-pow y₂
+  → rank-pow (bplus x₁ x₂) ≡ rank-pow (bplus y₁ y₂)
+rank-pow-bplus-eq-from-summands eq1 eq2 = cong₂ _⊕_ eq1 eq2
+
+-- Specialised first-eq derivation for the bpsi-source-at-equal-head
+-- sub-case: left summands are `bpsi ν α` and `bpsi ν β` (same ν, ANY
+-- α and β); left-rank equality is definitional (`refl` since both
+-- evaluate to `ω-rank-pow ν`).  Reduces consumer-side first-eq to
+-- the tail-rank-equality `rank-pow x₂ ≡ rank-pow y₂`.
+first-eq-from-bpsi-source-at-equal-head :
+  ∀ {ν α β x₂ y₂}
+  → rank-pow x₂ ≡ rank-pow y₂
+  → rank-pow (bplus (bpsi ν α) x₂) ≡ rank-pow (bplus (bpsi ν β) y₂)
+first-eq-from-bpsi-source-at-equal-head {ν} {α} {β} {x₂} {y₂} tail-eq =
+  rank-pow-bplus-eq-from-summands {x₁ = bpsi ν α} {x₂ = x₂}
+                                   {y₁ = bpsi ν β} {y₂ = y₂}
+    refl tail-eq
+
+----------------------------------------------------------------------
+-- (c) Trichotomy data type for the bplus-chain first-component
+----------------------------------------------------------------------
+
+-- Brouwer ordinals are NOT decidably ordered in general (`Ord`
+-- includes `olim f` carrying arbitrary functions ℕ → Ord), so a
+-- universal trichotomy on `rank-pow (bplus _ _)` values is
+-- unattainable under `--safe --without-K` without postulates.
+-- The TRACTABLE narrowing is a STRUCTURAL trichotomy: a data type
+-- that records which of the strict / equal cases applies WHEN the
+-- consumer has discharged the corresponding rank-arithmetic
+-- obligation.  Dispatchers below populate the strict / equal
+-- constructors from rank-evidence the consumer derives via the
+-- closed `<ᵇ⁰` / `<ᵇ¹` / `<ᵇ⁻ⁿ` umbrellas or the bpsi-source
+-- definitional collapse.
+
+data BplusFirstTri (x₁ x₂ y₁ y₂ : BT) : Set where
+  bplus-tri-strict :
+      rank-pow (bplus x₁ x₂) <′ rank-pow (bplus y₁ y₂)
+    → BplusFirstTri x₁ x₂ y₁ y₂
+  bplus-tri-equal  :
+      rank-pow (bplus x₁ x₂) ≡ rank-pow (bplus y₁ y₂)
+    → BplusFirstTri x₁ x₂ y₁ y₂
+
+-- Strict dispatcher: any consumer-derived strict witness on the
+-- bplus-chain rank-pow lifts into `bplus-tri-strict`.  The closed
+-- `<ᵇ⁰` umbrella's `rank-pow-mono-<ᵇ⁰` and the `<ᵇ¹` umbrella's
+-- `rank-pow-mono-<ᵇ¹` (which dispatches the strict-head-Ω joint-
+-- bplus case `<ᵇ¹-+1-+`) are the canonical producers of this
+-- witness; see also `RankMonoUmbrellaSlice4.rank-pow-mono-<ᵇ⁻ⁿ`
+-- for the WfCNF-bundled form.
+
+bplus-tri-from-strict :
+  ∀ {x₁ x₂ y₁ y₂}
+  → rank-pow (bplus x₁ x₂) <′ rank-pow (bplus y₁ y₂)
+  → BplusFirstTri x₁ x₂ y₁ y₂
+bplus-tri-from-strict strict = bplus-tri-strict strict
+
+-- Equal dispatcher: any consumer-derived first-eq lifts into
+-- `bplus-tri-equal`.  The bpsi-source-at-equal-head derivation
+-- `first-eq-from-bpsi-source-at-equal-head` is the canonical
+-- producer of this witness; the rank-equal closure under more
+-- general bplus shapes is the multi-PR ordinal-arithmetic
+-- challenge documented in this module's preamble.
+
+bplus-tri-from-equal :
+  ∀ {x₁ x₂ y₁ y₂}
+  → rank-pow (bplus x₁ x₂) ≡ rank-pow (bplus y₁ y₂)
+  → BplusFirstTri x₁ x₂ y₁ y₂
+bplus-tri-from-equal eq = bplus-tri-equal eq
+
+-- Trichotomy → rank-lex-jb dispatcher: the assembly that consumes
+-- whichever case the trichotomy yields and discharges to a `<lex`
+-- judgment at rank-lex-jb level.  The strict case fires `<lex-first`
+-- via `rank-lex-jb-strict-first`; the equal case fires `<lex-second`
+-- via `rank-lex-jb-strict-second-at-equal-first` provided the
+-- consumer can supply the leftmost-α strict witness.
+--
+-- This is the (a)+(b)+(c) assembly's RECIPE at the rank-lex-jb
+-- level: every reachable case dispatches mechanically given the
+-- consumer-side strict-or-equal-first witness.  The remaining
+-- gating obligation across the whole assembly is the
+-- consumer-side derivation of the leftmost-α strict witness in
+-- the equal case (when the consumer cannot supply it, the equal
+-- case is structurally dischargeable only if the rank-lex-jb is
+-- LITERALLY EQUAL on both sides — which by `<lex` irreflexivity
+-- contradicts a source-level strict inequality).
+
+dispatch-trichotomy-to-<lex :
+  ∀ {x₁ x₂ y₁ y₂}
+  → BplusFirstTri x₁ x₂ y₁ y₂
+  → leftmost-α (bplus x₁ x₂) <′ leftmost-α (bplus y₁ y₂)
+  → rank-lex-jb (bplus x₁ x₂) <lex rank-lex-jb (bplus y₁ y₂)
+dispatch-trichotomy-to-<lex {x₁} {x₂} {y₁} {y₂} (bplus-tri-strict strict) _      =
+  rank-lex-jb-strict-first {x₁ = x₁} {x₂ = x₂} {y₁ = y₁} {y₂ = y₂} strict
+dispatch-trichotomy-to-<lex {x₁} {x₂} {y₁} {y₂} (bplus-tri-equal eq)      l-strict =
+  rank-lex-jb-strict-second-at-equal-first {x₁ = x₁} {x₂ = x₂} {y₁ = y₁} {y₂ = y₂} eq l-strict
+
+----------------------------------------------------------------------
+-- Named theorem: bpsi-source-at-equal-head fully closed at rank-lex-jb
+----------------------------------------------------------------------
+
+-- The composition of the trichotomy with the bpsi-source first-eq
+-- derivation and the leftmost-α strict witness from PR #147's (a)
+-- machinery.  Inputs:
+--
+--   * `tail-eq : rank-pow x₂ ≡ rank-pow y₂`  — the consumer's
+--     RESIDUAL rank-arithmetic obligation; gating depends on the
+--     source-level relationship between x₂ and y₂ under WfCNF.
+--   * `α <ᵇ⁰ β`                              — the source-side
+--     strict inequality on the ψ-arguments, supplied by the
+--     consumer via the 10-constructor `_<ᵇ⁰_` umbrella.
+--
+-- Output: `<lex` discharge at rank-lex-jb level for the bpsi-source
+-- bplus chain.  This closes the bpsi-source-at-equal-head sub-case
+-- at the bplus-chain rank-lex-jb level GIVEN the consumer's
+-- tail-rank-equality discharge — which is the SAME gating
+-- obligation that the ψ-rank-level closure (`rank-adm-bpsi-strict-
+-- at-equality`) carries.  Resolving the structural blocker on
+-- tail-rank-equality unblocks BOTH levels mechanically.
+
+rank-lex-jb-bpsi-equal-head-from-tail-eq :
+  ∀ {ν α β x₂ y₂}
+  → rank-pow x₂ ≡ rank-pow y₂
+  → α <ᵇ⁰ β
+  → rank-lex-jb (bplus (bpsi ν α) x₂) <lex rank-lex-jb (bplus (bpsi ν β) y₂)
+rank-lex-jb-bpsi-equal-head-from-tail-eq {ν} {α} {β} {x₂} {y₂} tail-eq α<β =
+  rank-lex-jb-bpsi-at-equality
+    {ν = ν} {α = α} {β = β} {x₂ = x₂} {y₂ = y₂}
+    (first-eq-from-bpsi-source-at-equal-head
+      {ν = ν} {α = α} {β = β} {x₂ = x₂} {y₂ = y₂} tail-eq)
+    α<β

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -539,6 +539,15 @@ open import Ordinal.Buchholz.RankLexJointBplus using
   ; rank-lex-jb-strict-first
   ; leftmost-α-strict-from-bpsi-source
   ; rank-lex-jb-bpsi-at-equality
+  ; rank-pow-bplus-eq-from-summands
+  ; first-eq-from-bpsi-source-at-equal-head
+  ; BplusFirstTri
+  ; bplus-tri-strict
+  ; bplus-tri-equal
+  ; bplus-tri-from-strict
+  ; bplus-tri-from-equal
+  ; dispatch-trichotomy-to-<lex
+  ; rank-lex-jb-bpsi-equal-head-from-tail-eq
   )
 
 -- Slice 4 narrowing 2026-05-28 (own block per CLAUDE.md Working