ordinal(buchholz): Slice 3 lex-rank companion — bpsi-source-at-equality ψ-rank discharge

[hyperpolymath]

Summary

Lands Ordinal.Buchholz.RankLexSlice3 as the companion module to the
existing RankPowSlice3Headline (PR #141). Closes the ψ-rank-level
discharge of the bpsi-source-at-equality sub-case of <ᵇ-+1
joint-bplus — the case the head-Ω route leaves open.

What this slice closes

Three primitives, all pinned in Ordinal/Buchholz/Smoke.agda under
their own using block per CLAUDE.md Working rules:

• rank-adm-bpsi-strict-at-equality — wrapper around
  RankAdm.rank-mono-<ᵇ⁺-ψα-from-pow named for the joint-bplus
  consumer: rank-pow α <′ rank-pow β → rank-adm (bpsi ν α) <′ rank-adm (bpsi ν β). Discharges the ψ-rank strict step at the
  equality marker.
• rank-lex-bpsi-strict-at-equality — same content lifted to
  the existing RankLex._<lex_ order via <lex-second. Lex-rank-
  level mirror for consumers that compose against rank-lex.
• rank-adm-bplus-decompose-left — definitional refl
  pinning rank-adm (bplus x y) ≡ rank-adm x ⊕ rank-adm y for
  downstream chain composition.

Honest scope

The task's bplus-chain-level conclusion rank-pow (bplus x₁ x₂) <′ rank-pow (bplus y₁ y₂) does NOT close from this slice's
primitives — and that's a structural fact, not a missing-lemma gap:

• rank-pow (bpsi ν α) = ω-rank-pow ν = rank-pow (bpsi ν β) by
  definition, so no strict step exists at the rank-pow level at
  the equality marker.
• Promoting to rank-adm yields a clean strict step on the left
  summand (this slice's rank-adm-bpsi-strict-at-equality), but
  lifting through the bplus sum requires either additive-principal
  closure on rank-adm y₁ (not available — generic sum, not an
  ω-power) or strict-left-mono of _⊕_ (a non-theorem; documented
  counterexample in Phase13).

The clean follow-on (deferred): a parallel rank rank-lex-jb : BT → RankLex whose bplus case carries the leftmost-ψ-α info in the
second component. This requires reshaping the existing rank-lex
(whose <ᵇ-ψΩ≤ boundary discharge depends on the oz-second
bplus case) and is a non-local design slice.

Discipline

• --safe --without-K throughout
• Zero postulates, no funext, no TERMINATING pragma
• All headlines pinned in Ordinal/Buchholz/Smoke.agda
• Module wired into proofs/agda/All.agda adjacent to RankLex
• Design note inline documents the bplus-chain obstacle in
  sufficient detail that the next session can see which lemmas
  would unblock the full chain without re-deriving the analysis

Test plan

• agda proofs/agda/Ordinal/Buchholz/RankLexSlice3.agda exits 0
• agda proofs/agda/Ordinal/Buchholz/Smoke.agda exits 0
• agda proofs/agda/All.agda exits 0
• agda proofs/agda/Smoke.agda exits 0
• No postulate / TERMINATING / trustMe / REWRITE / NO_POSITIVITY / type-in-type in the new module
• CI green on PR

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 74 issues detected

Severity	Count
🔴 Critical	17
🟠 High	36
🟡 Medium	21

⚠️ 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": "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"
  },
  {
    "reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
    "type": "agda_postulate",
    "file": "/home/runner/work/echo-types/echo-types/tutorial/provenance_debugging/ProvenanceDebugging.agda",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence