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

[hyperpolymath]

Summary

Advances the rank-lex-jb pivot's (a)+(b)+(c) assembly plan beyond the (a) primitive that PR #147 shipped. Three primitives added to `Ordinal.Buchholz.RankLexJointBplus` and pinned in `Ordinal/Buchholz/Smoke.agda`. Zero postulates, `--safe --without-K`, no funext.

Three primitives

Primitive	Type	Role
`rank-lex-jb-strict-first`	`rank-pow (bplus _ _) <′ rank-pow (bplus _ _) → rank-lex-jb _ <lex rank-lex-jb _`	Leg (b) primitive; one-line via `<lex-first`
`leftmost-α-strict-from-bpsi-source`	`α <ᵇ⁰ β → leftmost-α (bplus (bpsi ν α) x₂) <′ leftmost-α (bplus (bpsi ν β) y₂)`	Consumer helper composing `leftmost-α-{bplus,bpsi}` with `rank-pow-mono-<ᵇ⁰`
`rank-lex-jb-bpsi-at-equality`	`first-eq → α <ᵇ⁰ β → rank-lex-jb _ <lex rank-lex-jb _`	Named theorem closing the bpsi-source-at-equality sub-case at rank-lex-jb level, gated on first-eq hypothesis

Where this sits in the assembly

Per the PR #147 module preamble's `(a)+(b)+(c)` plan (see `RankLexJointBplus.agda` preamble):

• (a) equal-first lex-second leg — CLOSED in PR ordinal(buchholz): rank-lex-jb scaffold — parallel rank with richer bplus second component #147 (`rank-lex-jb-strict-second-at-equal-first`).
• (b) strict-first lex-first leg — primitive CLOSED here; consumer-side derivation of `rank-pow (bplus _ _) <′ rank-pow (bplus _ _)` remains the multi-PR ordinal-arithmetic challenge.
• (c) first-component trichotomy — STILL OPEN (Ord-valued decidability bridge in `Phase13` not yet attempted).
• 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 (preserved in module preambles)

• The trivial `<lex-first` shape of primitive (1) does not mean leg (b) is "done" — the consumer plumbing is the hard part. Both pre-identified unblock routes (additive-principal closure on a generic sum, strict-left-mono of `⊕`) are CHECKED-REFUTED in PR brouwer(arithmetic): checked refutations of strict-left-mono of _⊕_ and additive-principal closure on generic sums #146.
• Primitive (2) is `<ᵇ⁰`-parameterised, not `<ᵇ`-parameterised. Lifting to full `<ᵇ` requires the joint-bplus closure that this very pivot was designed to attack.
• Primitive (3) requires the first-eq hypothesis as input; consumer-side derivation is the gating obligation.

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.

Test plan

• All four Agda lanes typecheck locally.
• Three new primitives pinned in Buchholz Smoke.
• Foundation guardrail + kernel-guard pass.
• CI: `check` + `cold-check` + governance lanes green.
• Auto-merge on green.

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 58 issues detected

Severity	Count
🔴 Critical	17
🟠 High	22
🟡 Medium	19

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "No test directory or test files found",
    "type": "no_tests",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "flag",
    "rule_module": "honest_completion",
    "severity": "high",
    "deduction": 20
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_workflow",
    "file": "codeql.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action rpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in agda.yml",
    "type": "unknown",
    "file": "agda.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in agda.yml",
    "type": "unknown",
    "file": "agda.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in governance.yml",
    "type": "unknown",
    "file": "governance.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in hypatia-scan.yml",
    "type": "unknown",
    "file": "hypatia-scan.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in mirror.yml",
    "type": "unknown",
    "file": "mirror.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard.yml",
    "type": "unknown",
    "file": "scorecard.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence