Earn-back: ledger item B (Buchholz) — K-attributed part

[hyperpolymath]

Summary

Earns back the K-attributed part of proof-debt ledger item B
(Buchholz order). Item B held that the two same-binder sub-cases
(bpsi ν α <ᵇ bpsi ν β with α <ᵇ β; bplus x y₂ <ᵇ bplus x z₂
with y₂ <ᵇ z₂) were "not constructible pending a K-free
reformulation".

• Reconfirmed the obstruction on Agda 2.8 (the Order.agda
  comment cited 2.6.3): the naive <ᵇ-irrefl matching x <ᵇ x
  forces the shared-binder deletion ν =?= ν, rejected --without-K.
• New module Ordinal.Buchholz.OrderExtendedDirect (_<ᵇᵈ_)
  carries both same-binder constructors and proves, --safe --without-K, zero postulates / zero escape pragmas:
  • <ᵇ-irrefl via generalised <ᵇ⇒≢ (distinct indices) discharged
    by cong-projection injectivity + the K-free conflict rule —
    refl is never matched, so the deletion rule is never invoked;
  • <ᵇ-trans (full extended transitivity);
  • embed : Order._<ᵇ_ ⇒ _<ᵇᵈ_ — conservativity (faithful strict
    extension, not a redefinition).
• Wired into All.agda, pinned in Smoke.agda; full + smoke build
  green locally (Agda 2.8, stdlib v2.3).

Scope (rigorous, not over-claimed)

• This is not [CLOSED-NEG]: the K-free reformulation did not
  resist — it succeeded.
• WF of the direct relation is out of scope: a termination-checker
  matter (Routes A/B of buchholz-extended-wf.md), orthogonal to K,
  still delivered via the ExtendedOrder._<ᵇ⁺_ measure, which stays
  load-bearing. Trichotomy/totality out of scope.
• No paper / conservativity / abstract claim moves — item B is off
  the paper critical path. Logged as retraction follow-up
  F-2026-05-18b; ledger row B / recommended-order / Status updated.

Notes

• Base: earn-back/f4-f2-2026-05-18 (PR Earn-back: Gates F4 + F2 PASSED (retraction follow-up F-2026-05-18a) #50, unmerged) — the
  earn-back ledger + F-2026-05-18a live there; this work edits those
  files so it must stack on Earn-back: Gates F4 + F2 PASSED (retraction follow-up F-2026-05-18a) #50, not main.
• MAP.adoc: not on main (introduced by open PR docs: canonical echo-types Master Map (discoverability SoT) #54). To avoid an
  add/add duplication, the item-B status line is not copied; the
  exact one-line replacement is recorded in docs/retractions.adoc
  (F-2026-05-18b) as a tracked follow-up to apply in/after docs: canonical echo-types Master Map (discoverability SoT) #54.

🤖 Generated with Claude Code

[hyperpolymath]

Auto-closed by a stacked-base merge — recovered (metadata only).

This PR was closed (not merged) when its stacked base
earn-back/f4-f2-2026-05-18 was deleted on the squash-merge of #50.
GitHub closes (rather than retargets) a child whose base branch is
deleted, and a closed PR with a missing base can't be reopened or
retargeted directly.

Recovered non-destructively: recreated the deleted base ref at its
pre-merge tip (36854a8), reopened this PR, retargeted base → main,
then removed the temporary ref. No commits were rewritten, nothing
was merged or rebased. The head branch
earn-back/buchholz-item-b-2026-05-18 (0ca5a68, 1 commit, 5 files)
is intact; its content is not on main.

Left for the owning session (deliberately not done here): main now
contains the squashed #47/#49/#50, so this needs a rebase onto current
main and conflict resolution before it can land — that's a content
decision for whoever drove the earn-back chain, not a cross-session
edit I should make.

— restored so the item-B (Buchholz, K-attributed) earn-back work
isn't silently lost.

[hyperpolymath]

Reduced to proof-only; rest superseded

Triaged against current main: the F1 spike (8682447) and the F4/F2 earn-back (fb3742d → EchoPullbackUnivF4.agda, EchoStepNDModelF2.agda) are byte-identical to main — already landed via #54/#55/#56/#58/#60. The doc-reframe commits were superseded by main's own reframe; the add Nix flake commit was dropped (Guix-primary / no-Nix policy).

Sole content not already in main: ledger item B (0ca5a68) — new module proofs/agda/Ordinal/Buchholz/OrderExtendedDirect.agda (225 lines) + Smoke pins + All.agda registration. Branch rewritten to that single clean commit (+238/-0).

Local CI-parity verification (Agda 2.8.0, --ignore-interfaces): All.agda, Smoke.agda, characteristic/All.agda, examples/All.agda all green; new module is {-# OPTIONS --safe --without-K #-} with zero postulates / escape pragmas. Left for the repo's agda.yml to gate.

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 10 issues detected

Severity	Count
🔴 Critical	0
🟠 High	5
🟡 Medium	5

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 quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action actions/cache@v4 needs attention",
    "type": "unpinned_action",
    "file": "agda.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "No dependabot.yml or renovate.json found in echo-types",
    "type": "DependencyUpdate",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "high",
    "remediation": "Add .github/dependabot.yml or renovate.json configuration.",
    "scorecard_check": "Dependency-Update-Tool"
  },
  {
    "reason": "Nominal-only SAST in echo-types: codeql.yml language matrix contains no language present in the repo and lacks `actions`, so CodeQL records zero results on every commit. Remediation: set the CodeQL matrix to `language: actions`.",
    "type": "StaticAnalysis",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Add CodeQL or equivalent SAST workflow.",
    "scorecard_check": "SAST"
  },
  {
    "reason": "1 workflow(s) with tag-pinned (not SHA-pinned) actions in echo-types",
    "type": "DependencyPinning",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Pin GitHub Actions and Docker base images by SHA hash.",
    "scorecard_check": "Pinned-Dependencies"
  },
  {
    "reason": "Repository has 3 non-main remote branch(es). Policy: single main branch only.",
    "type": "GS007",
    "file": ".",
    "action": "delete_remote_branches",
    "rule_module": "git_state",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence