proof(Path-3 prototype): same-left joint-bplus rank-mono extension (#167)

## Summary

Mechanises the **Path-3 alternative** identified in PR #166's closing
note: enrich the SOURCE RULE rather than the rank function. New module
\`Ordinal.Buchholz.RankMonoSameLeft\` introduces a \`<ᵇ⁰\`-grounded
same-left joint-bplus constructor and closes its rank-pow obligation in
**one line**, bypassing the rank-lex-jb pivot's first-eq derivation
entirely for the same-literal-left sub-case. Zero postulates, \`--safe
--without-K\`, no funext.

## The structural insight tested

PR #166's closing note flagged Path-3 as a possible reframing:

> The source rule may need enrichment, not the rank function.
> For a valid \`<ᵇ-+1\`-at-equal-head derivation under WfCNF, rank-mono
soundness *requires* tail-rank-strict. Path-3 alternative: enrich the
source side instead — promote \`_<ᵇ_\` to carry a \`<ᵇ⁺-+2\`-style
same-left constructor with both head-eq and tail-strict premises baked
in.

This PR mechanises that intuition concretely. **Result: WORKS.**

## Headlines

| Name | Role |
|---|---|
| \`_<ᵇ⁺²_\` | Extended relation: \`<ᵇ⁺²-from-<ᵇ⁰\` embeds 10 closed
cases + \`<ᵇ⁺²-same-left\` adds the source-rule enrichment |
| \`rank-pow-mono-<ᵇ⁺²\` | Two-case structural recursion: each case ONE
LINE |
| \`rank-pow-mono-same-left\` | Direct lemma showing the same-left case
without routing through embedding |

## Path-3 vs rank-lex-jb (complementary, not subsuming)

| Sub-case | Path | Closure |
|---|---|---|
| Same LITERAL left (\`bplus x s\` vs \`bplus x t\`) | **Path-3 (this
PR)** | One-line via \`rank-pow-bplus-right-mono\` |
| Same head-Ω, different left syntax (\`bpsi ν α\` vs \`bOmega ν\`) |
rank-lex-jb (#147+#165+#166) | Multi-step: leftmost-α + first-eq +
\`<lex-second\` |

The same-left case is UNREACHABLE in K-free \`_<ᵇ_\` (would require
\`<ᵇ-irrefl\` violation via \`<ᵇ-+1 (x <ᵇ x)\`); reachable only in the
extended \`_<ᵇ⁺_\` of \`Ordinal.Buchholz.OrderExtended\` via \`<ᵇ⁺-+2\`.
This prototype narrows the tail premise to \`_<ᵇ⁰_\` to keep the closure
inductively grounded.

The K-restriction does NOT bite at constructor formation (only at
pattern-match elimination), so the same-binder \`<ᵇ⁺²-same-left\`
constructor is fine under \`--safe --without-K\`.

## Honest scope

- Does NOT prove well-foundedness of \`_<ᵇ⁺²_\` — separate from
rank-mono; would need a Brouwer-rank embedding (the rank function here
provides the seed).
- Does NOT subsume rank-lex-jb for the cross-head case — Path-3 and
rank-lex-jb are complementary.
- Does NOT extend the tail premise to \`_<ᵇ¹_\` — composes mechanically
via \`rank-pow-mono-<ᵇ¹\` but kept out of the prototype for minimality.
- Does NOT wrap in WfCNF endpoints (à la \`_<ᵇ⁻ⁿ_\` from Slice 4) — left
for downstream consumers.

## Implication confirmed

PR #166's #3 implication holds mechanically: enriching the source rule
is structurally simpler than the rank-function enrichment for this
scenario. The one-line closure here contrasts with the multi-PR
rank-lex-jb assembly chain. This suggests the **future bplus-chain
rank-mono umbrella may want to be designed as a UNION of source-rule
extensions** (Path-3 style for cleanly-decomposable cases) rather than a
single enriched rank function (rank-lex-jb style for cross-head cases).

## Local verification

- \`agda -i proofs/agda
proofs/agda/Ordinal/Buchholz/RankMonoSameLeft.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\` — **161 modules** pass
(one new).
- \`sh scripts/kernel-guard.sh\` — PASS.

Five new names pinned in \`Ordinal/Buchholz/Smoke.agda\` under a new
\`RankMonoSameLeft\` \`using\` block.

## Test plan

- [x] Module typechecks under \`--safe --without-K\` with zero
postulates.
- [x] Full suite + Smoke remain green with the new module wired in.
- [x] Foundation guardrail + kernel-guard pass with 161 modules.
- [ ] 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>

Author: hyperpolymath

proofs/agda/All.agda

@@ -149,6 +149,7 @@ open import Ordinal.Buchholz.RankPowSlice3Headline
 open import Ordinal.Buchholz.RankMonoUmbrella
 open import Ordinal.Buchholz.RankMonoUmbrellaSlice3
 open import Ordinal.Buchholz.RankMonoUmbrellaSlice4
+open import Ordinal.Buchholz.RankMonoSameLeft
 open import Ordinal.Buchholz.RecursiveSurfaceOrder
 open import Ordinal.Buchholz.RecursiveSurfaceBudget
 open import Ordinal.Buchholz.SurfaceOrder

proofs/agda/Ordinal/Buchholz/RankMonoSameLeft.agda

@@ -0,0 +1,173 @@
+{-# 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>
+
+-- Path-3 PROTOTYPE — same-left joint-bplus extension (2026-05-30).
+--
+-- ## Context
+--
+-- Slice 3+4 Route A's rank-lex-jb pivot (PRs #147 / #165 / #166)
+-- attacks the joint-bplus `<ᵇ-+1`-at-equal-head case by enriching
+-- the RANK FUNCTION (carrying `leftmost-α` as a second component)
+-- to discriminate where rank-pow alone collapses.  The (a)+(b)+(c)
+-- assembly identified a key insight in PR #166's note: the
+-- consumer-side first-eq derivation reduces to TAIL-RANK-EQUALITY
+-- under WfCNF (`first-eq-from-bpsi-source-at-equal-head`), and the
+-- same residual obligation also gates the ψ-rank-level closure
+-- (`RankLexSlice3.rank-adm-bpsi-strict-at-equality`).
+--
+-- ## Path-3 ALTERNATIVE — enrich the SOURCE rule, not the rank
+--
+-- The K-free `_<ᵇ_`'s `<ᵇ-+1` constructor carries only `x₁ <ᵇ y₁`
+-- as premise; nothing on `x₂ vs y₂`.  For the same-LITERAL-left
+-- sub-case (`bplus x y₂ <ᵇ bplus x z₂` when `y₂ <ᵇ z₂`),
+-- `<ᵇ-irrefl` makes the only viable `<ᵇ-+1` instantiation
+-- (`x <ᵇ x`) impossible — so this case is UNREACHABLE in K-free
+-- `_<ᵇ_`.  The extended `_<ᵇ⁺_` of `Ordinal.Buchholz.OrderExtended`
+-- adds `<ᵇ⁺-+2 : x₁ ≡ y₁ → x₂ <ᵇ y₂ → bplus x₁ x₂ <ᵇ⁺ bplus y₁ y₂`
+-- to fill this gap (mod a K-elimination on the shared `x₁ ≡ y₁`).
+--
+-- This PROTOTYPE narrows the extended `<ᵇ⁺-+2` to `<ᵇ⁰` on the
+-- tail premise (the closed 10-constructor umbrella), then shows
+-- rank-pow closure FOR THE SAME-LEFT JOINT-BPLUS CASE WITHOUT
+-- routing through rank-lex-jb at all.  Path-3's claim: enriching
+-- the source-rule with same-left + tail-`<ᵇ⁰` discharges this
+-- case at the rank-pow level via `rank-pow-bplus-right-mono`,
+-- bypassing the rank-lex-jb pivot's first-eq derivation
+-- obligation entirely.
+--
+-- ## Scope of this prototype
+--
+-- * Extends only `_<ᵇ⁰_` (10-constructor closure), not `_<ᵇ¹_`
+--   (which adds strict-head joint-bplus) — keeps the prototype
+--   minimal and the closure inductively grounded.
+-- * Does NOT prove well-foundedness of the extended relation —
+--   that would need a separate proof; orthogonal to the
+--   rank-mono question.
+-- * Does NOT subsume rank-lex-jb for the cross-head case
+--   (`bpsi ν α` vs `bOmega ν` etc.) — that case has different
+--   left-summand SYNTAX, only equal rank-pow.  Rank-lex-jb
+--   handles those; this prototype handles same-left-syntax.
+--
+-- ## What this prototype demonstrates
+--
+-- The Path-3 implication from PR #166's closing note:
+-- "the source rule may need enrichment, not the rank function".
+-- A `<ᵇ⁰`-grounded same-left source rule closes its rank-pow
+-- obligation in ONE LINE via `rank-pow-bplus-right-mono`,
+-- contrasted with the multi-PR rank-lex-jb assembly's chain
+-- through first-eq + leftmost-α-strict + `<lex-second`.  When
+-- the same-left literal-equality holds, Path-3 is structurally
+-- simpler than the rank-lex-jb route.
+--
+-- Honest caveat: this does NOT close the RANK-EQUAL-HEAD-
+-- SYNTAX-DIFFERENT case (e.g., `bpsi ν α` vs `bOmega ν`); the
+-- rank-lex-jb pivot is still load-bearing for that scenario.
+-- Path-3 covers a strictly different sub-case.
+
+module Ordinal.Buchholz.RankMonoSameLeft where
+
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+
+open import Ordinal.Brouwer.Phase13 using (_<′_)
+open import Ordinal.Buchholz.Syntax using (BT; bplus)
+open import Ordinal.Buchholz.RankPow using
+  ( rank-pow
+  ; rank-pow-bplus-right-mono
+  )
+open import Ordinal.Buchholz.RankMonoUmbrella using
+  ( _<ᵇ⁰_
+  ; rank-pow-mono-<ᵇ⁰
+  )
+
+----------------------------------------------------------------------
+-- The extended relation `_<ᵇ⁺²_`
+----------------------------------------------------------------------
+
+-- Two constructors:
+--
+--   1. `<ᵇ⁺²-from-<ᵇ⁰` — embed every `<ᵇ⁰` derivation into the
+--      extension.  Keeps the prototype additive over the closed
+--      umbrella's 10 cases.
+--   2. `<ᵇ⁺²-same-left` — the SOURCE-RULE ENRICHMENT: when the
+--      left summand is LITERALLY equal on both sides and the
+--      right summand satisfies `<ᵇ⁰`, the bplus chain is in the
+--      relation.  Crucially, the SAME `x` appears on both sides
+--      under one binder — this is the K-eliminated case that
+--      `_<ᵇ_` deliberately omits.  In `--safe --without-K` the
+--      shared binder is supplied syntactically (Agda accepts
+--      this in `data` constructors; the K-restriction bites only
+--      at pattern-match elimination, not at constructor
+--      formation).
+
+data _<ᵇ⁺²_ : BT → BT → Set where
+  <ᵇ⁺²-from-<ᵇ⁰ : ∀ {x y}
+    → x <ᵇ⁰ y
+    → x <ᵇ⁺² y
+
+  <ᵇ⁺²-same-left : ∀ {x y₂ z₂}
+    → y₂ <ᵇ⁰ z₂
+    → bplus x y₂ <ᵇ⁺² bplus x z₂
+
+infix 4 _<ᵇ⁺²_
+
+----------------------------------------------------------------------
+-- Rank-pow monotonicity for `_<ᵇ⁺²_`
+----------------------------------------------------------------------
+
+-- Direct structural recursion.  The inherited case forwards to the
+-- closed umbrella's `rank-pow-mono-<ᵇ⁰`.  The same-left case fires
+-- `rank-pow-bplus-right-mono` (which IS `⊕-mono-<-right`
+-- specialised to rank-pow) on the tail's rank-pow strict witness.
+
+rank-pow-mono-<ᵇ⁺² : ∀ {x y} → x <ᵇ⁺² y → rank-pow x <′ rank-pow y
+rank-pow-mono-<ᵇ⁺² (<ᵇ⁺²-from-<ᵇ⁰ p) = rank-pow-mono-<ᵇ⁰ p
+rank-pow-mono-<ᵇ⁺² (<ᵇ⁺²-same-left {x = x} {y₂ = y₂} {z₂ = z₂} p) =
+  rank-pow-bplus-right-mono {x = x} {y = y₂} {z = z₂}
+    (rank-pow-mono-<ᵇ⁰ p)
+
+----------------------------------------------------------------------
+-- Convenience constructor — direct same-left rank-mono
+----------------------------------------------------------------------
+
+-- The same-left case stated as a direct rank-mono lemma, without
+-- routing through the extended-relation embedding.  Demonstrates
+-- the one-line closure that motivated this Path-3 prototype.
+
+rank-pow-mono-same-left :
+  ∀ {x y₂ z₂}
+  → y₂ <ᵇ⁰ z₂
+  → rank-pow (bplus x y₂) <′ rank-pow (bplus x z₂)
+rank-pow-mono-same-left {x = x} {y₂ = y₂} {z₂ = z₂} p =
+  rank-pow-bplus-right-mono {x = x} {y = y₂} {z = z₂}
+    (rank-pow-mono-<ᵇ⁰ p)
+
+----------------------------------------------------------------------
+-- What this prototype shows
+----------------------------------------------------------------------
+
+-- Path-3 verdict (witnessed mechanically): the SAME-LITERAL-LEFT
+-- joint-bplus case at the rank-pow level discharges in ONE LINE
+-- via existing `rank-pow-bplus-right-mono` once the source rule
+-- carries a `<ᵇ⁰`-grounded tail premise.  The rank-lex-jb pivot's
+-- machinery (first-eq derivation, leftmost-α discriminator,
+-- `<lex-second` discharge, tail-rank-equality consumer
+-- obligation) is NOT NEEDED for this sub-case.
+--
+-- The implication identified in PR #166's note holds: enriching
+-- the source rule is structurally simpler than the rank-function
+-- enrichment for this scenario.  For the cross-head case
+-- (`bpsi ν α` vs `bOmega ν` etc.), rank-lex-jb's leftmost-α
+-- discriminator remains load-bearing; Path-3 is complementary,
+-- not subsuming.
+--
+-- Future work that this prototype unblocks:
+--   * Lifting the tail premise from `_<ᵇ⁰_` to `_<ᵇ¹_` (allowing
+--     strict-head joint-bplus tails) — composes mechanically via
+--     `rank-pow-mono-<ᵇ¹`.
+--   * Wrapping the extension in WfCNF endpoints (mirroring
+--     `_<ᵇ⁻ⁿ_` from RankMonoUmbrellaSlice4) for downstream
+--     consumers that need the canonical-form invariant.
+--   * Well-foundedness of `_<ᵇ⁺²_` — separate from rank-mono;
+--     would need a Brouwer-rank embedding (the rank function
+--     here provides the seed).

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -568,3 +568,20 @@ open import Ordinal.Buchholz.RankMonoUmbrellaSlice4 using
   ; <ᵇ⁻ⁿ-+1-+
   ; rank-pow-mono-<ᵇ⁻ⁿ
   )
+
+-- Path-3 prototype 2026-05-30 (own block per CLAUDE.md Working
+-- rules): same-left joint-bplus rank-mono extension.  Bypasses
+-- the rank-lex-jb pivot's first-eq derivation obligation for the
+-- LITERAL-same-left sub-case by enriching the source rule
+-- (`<ᵇ⁺²-same-left`) rather than the rank function.  One-line
+-- closure via `rank-pow-bplus-right-mono` once the tail premise
+-- is grounded in `_<ᵇ⁰_`.  Complementary to rank-lex-jb, which
+-- remains load-bearing for the cross-head case (`bpsi ν α` vs
+-- `bOmega ν`, syntactically different but rank-equal).
+open import Ordinal.Buchholz.RankMonoSameLeft using
+  ( _<ᵇ⁺²_
+  ; <ᵇ⁺²-from-<ᵇ⁰
+  ; <ᵇ⁺²-same-left
+  ; rank-pow-mono-<ᵇ⁺²
+  ; rank-pow-mono-same-left
+  )