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

hyperpolymath · claude · web-flow · commit 930000b95ffb · 2026-05-30T14:00:14.000Z
## Summary Follow-on to PR #165's (b) primitive. Adds the **(c) trichotomy** data type and the **consumer-side first-eq derivation** tools 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. ## What lands ### Consumer-side first-eq derivation (2 primitives) 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-equalities via \`cong₂ _⊕_\`. | Name | Role | |---|---| | \`rank-pow-bplus-eq-from-summands\` | Generic \`cong₂ _⊕_\` helper | | \`first-eq-from-bpsi-source-at-equal-head\` | Specialised: bpsi-source at equal head (left-rank-eq is \`refl\`); reduces consumer-side first-eq to **tail-rank-equality only** | ### (c) Trichotomy data type + dispatchers (5 primitives) 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. | Name | Role | |---|---| | \`BplusFirstTri x₁ x₂ y₁ y₂\` | Data type with two constructors: \`bplus-tri-strict\` (rank-strict) and \`bplus-tri-equal\` (rank-equal) | | \`bplus-tri-from-strict\` / \`bplus-tri-from-equal\` | Wrapper constructors lifting consumer-derived witnesses into the trichotomy | | \`dispatch-trichotomy-to-<lex\` | Assembly headline: consumes a trichotomy + leftmost-α strict witness, produces \`<lex\` at rank-lex-jb level. Strict → \`<lex-first\` via (b) primitive (#165); equal → \`<lex-second\` via (a) primitive (#147). | ### Named theorem: bpsi-source-at-equal-head fully discharged (1) | Name | Type | |---|---| | \`rank-lex-jb-bpsi-equal-head-from-tail-eq\` | \`rank-pow x₂ ≡ rank-pow y₂ → α <ᵇ⁰ β → 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 - 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 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. ## (a)+(b)+(c) assembly status after this PR Per PR #147's preamble plan: | Leg | Status | |---|---| | (a) equal-first lex-second | CLOSED in #147 | | (b) strict-first lex-first primitive | CLOSED in #165 (one-liner via \`<lex-first\`) | | (c) first-component trichotomy | CLOSED HERE as a structural data type + dispatchers | | Consumer-side first-eq derivation | CLOSED HERE for the bpsi-source-at-equal-head case (parameterised on tail-rank-eq) | | Full assembly headline | \`rank-lex-jb-bpsi-equal-head-from-tail-eq\` named theorem closes the bpsi sub-case given **only** tail-rank-eq | The bplus-chain-level rank-mono umbrella over **all** 13 \`_<ᵇ_\` constructors is still gated on (i) tail-rank-equality discharge (structural ordinal-arithmetic work) AND (ii) the equal-first dispatch beyond the bpsi-source case (open research). Per the SLICE 4 narrowing (\`RankMonoUmbrellaSlice4\`), the \`<ᵇ⁻ⁿ-shortfall-equal-head\` matched-negative remains. ## 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\`. ## Test plan - [x] All Agda lanes typecheck locally. - [x] New names pinned in Buchholz Smoke. - [x] Foundation guardrail + kernel-guard pass. - [ ] CI: \`check\` + \`cold-check\` + governance lanes green. - [ ] Auto-merge on green. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
diff --git a/proofs/agda/Ordinal/Buchholz/RankLexJointBplus.agda b/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)
+    α<β
diff --git a/proofs/agda/Ordinal/Buchholz/Smoke.agda b/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
