echo-types: earn back ledger item B (Buchholz) — K-attributed part

The two same-binder Buchholz-order sub-cases (bpsi ν α <ᵇ bpsi ν β
with α <ᵇ β; bplus x y₂ <ᵇ bplus x z₂ with y₂ <ᵇ z₂) were ledgered
as "not constructible pending a K-free reformulation". Reconfirmed
the obstruction on Agda 2.8 (Order.agda cited 2.6.3): the *naive*
<ᵇ-irrefl matches x <ᵇ x, forcing the shared-binder deletion
ν =?= ν, which --without-K rejects.

New module Ordinal.Buchholz.OrderExtendedDirect defines the
extended direct relation _<ᵇᵈ_ carrying *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 deletion is never
                invoked;
  * <ᵇ-trans   full extended transitivity;
  * embed      conservativity: core Order._<ᵇ_ ↪ _<ᵇᵈ_ (faithful
                strict extension, not a redefinition).

Wired into All.agda, pinned in Smoke.agda; full + smoke build green.

Strictly scoped: WF of the direct relation remains a
termination-checker matter (not K) delivered via the
ExtendedOrder._<ᵇ⁺_ measure, which stays load-bearing; trichotomy
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 / order / Status updated. MAP.adoc
status line deferred (tracked, exact patch recorded) to PR #54
which introduces MAP.adoc.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

docs/echo-types/earn-back-plan.adoc

@@ -210,15 +210,30 @@ single index; it moves no claim.
   wired into `All`/`Smoke`. Retraction follow-up F-2026-05-18a.
 
 | B
-| Buchholz order: `Ordinal/Buchholz/Order.agda` `_<ᵇ_` compares ψ by
-  Ω-index only and asserts `<ᵇ-ψΩ≤` as a constructor; same-binder
-  sub-cases (`bpsi ν α <ᵇ bpsi ν β` with `α <ᵇ β`;
-  `bplus x y₂ <ᵇ bplus x z₂` with `y₂ <ᵇ z₂`) are not constructible
-  pending a K-free reformulation. Direct-constructor totality / WF do
-  not land; `ExtendedOrder.agda` is the honest closed wrapper (WF via
-  the comparison *measure* `_<ᵇ⁺_`).
-| Disclosed structural-fidelity gap. *Off the echo-types paper
-  critical path.* Long-tail workstream.
+| Buchholz order — K-attributed part *earned back* (F-2026-05-18b;
+  `proofs/agda/Ordinal/Buchholz/OrderExtendedDirect.agda`). The two
+  same-binder sub-cases (`bpsi ν α <ᵇ bpsi ν β` with `α <ᵇ β`;
+  `bplus x y₂ <ᵇ bplus x z₂` with `y₂ <ᵇ z₂`) *are* directly
+  constructible: `_<ᵇᵈ_` carries both as constructors and proves
+  irreflexivity and transitivity `--safe --without-K`, *zero
+  postulates and zero escape pragmas*. The earlier "not constructible
+  pending a K-free reformulation" was specific to the *naive*
+  `<ᵇ-irrefl` matching `x <ᵇ x` (shared-binder deletion `ν =?= ν`,
+  reconfirmed on Agda 2.8 — not a 2.6.3 artefact); the reformulation
+  `<ᵇ⇒≢ ∘ refl` discharged by `cong`-projection injectivity + the
+  K-free *conflict* rule (no `refl` ever matched) sidesteps it
+  without K. The K-free core `Order._<ᵇ_` embeds faithfully (`embed`;
+  conservativity — strict extension, not a redefinition).
+  *Residual, not K and not earned here:* well-foundedness of the
+  direct relation remains the termination-checker problem of
+  `docs/echo-types/buchholz-extended-wf.md` (Routes A/B), orthogonal
+  to K; WF stays delivered via the comparison *measure*
+  `ExtendedOrder._<ᵇ⁺_`, which remains load-bearing. Trichotomy /
+  totality out of scope. *Moves no paper claim* (item B is off the
+  paper critical path).
+| K-attributed sub-claim *earned back* (F-2026-05-18b). Residual
+  WF-via-measure is a disclosed termination-checker gap, *off the
+  echo-types paper critical path*, long-tail.
 
 | C
 | `characteristic/` open obligations: general recipe-non-triviality
@@ -263,8 +278,10 @@ single index; it moves no claim.
   make-or-break and unlocks *F3* (A3). Now the next action.
 . *Doc-integrity* (D) — reconcile alongside step 1; removes a drift
   vector at near-zero cost.
-. *Buchholz* (B) — separate long-tail; keep the `ExtendedOrder`
-  wrapper load-bearing. Not paper-blocking.
+. *Buchholz* (B) — K-attributed part *earned back* 2026-05-18
+  (F-2026-05-18b). `ExtendedOrder` wrapper stays load-bearing for the
+  residual WF-via-measure (a termination-checker, not-K, matter). Not
+  paper-blocking; moved no paper claim.
 . *`characteristic/`* (C) — lowest priority; EI-2 already terminated.
 
 == Status
@@ -287,3 +304,19 @@ single index; it moves no claim.
   *Strictly scoped:* F2 is the Echo functor only — the graded-comonad,
   model-independence, and conservativity claims remain retracted; F1
   (coassoc) and F3 remain open.
+* *2026-05-18 — ledger item B (Buchholz), K-attributed part EARNED
+  BACK.* `proofs/agda/Ordinal/Buchholz/OrderExtendedDirect.agda`: the
+  two same-binder constructors `<ᵇ-ψα` / `<ᵇ-+2` are directly
+  constructible; irreflexivity + transitivity proved
+  `--safe --without-K`, zero postulates / zero escape pragmas, via
+  the `<ᵇ⇒≢ ∘ refl` + `cong`-projection / conflict-rule no-confusion
+  reformulation (the naive shared-binder deletion was first
+  reconfirmed to still fail on Agda 2.8). Core `Order._<ᵇ_` embeds
+  faithfully (`embed`). Wired into `All.agda`, pinned in `Smoke.agda`;
+  full + smoke build green. Logged as retraction follow-up
+  F-2026-05-18b. *Strictly scoped:* this is item B's *K-attributed*
+  sub-claim only. WF of the direct relation remains a
+  termination-checker matter (not K) delivered via the
+  `ExtendedOrder._<ᵇ⁺_` measure, which stays load-bearing; trichotomy
+  out of scope. *No paper claim moved* — item B is off the paper
+  critical path.

docs/retractions.adoc

@@ -192,6 +192,78 @@ note), `docs/echo-types/conservativity.adoc` (scope), and
 to the *conditional/scoped* earned claim, never beyond it;
 `docs/echo-types/earn-back-plan.adoc` ledger rows A2/A4 and Status.
 
+==== Follow-up F-2026-05-18b (2026-05-18) — ledger item B (Buchholz), K-attributed part earned back
+
+Scope note. This follow-up resolves *proof-debt ledger item B*
+(`docs/echo-types/earn-back-plan.adoc`), **not** an R-2026-05-18
+retracted claim. Item B was a disclosed structural-fidelity gap,
+explicitly *off the echo-types paper critical path*; this entry is
+logged here only because the earn-back plan designates
+`docs/retractions.adoc` as the single locus for outcomes. *No paper,
+conservativity, or abstract claim moves as a result of this
+follow-up*, and no R-2026-05-18 retraction is reopened or earned back.
+
+==== Finding
+
+Item B held that the two same-binder Buchholz-order sub-cases
+(`bpsi ν α <ᵇ bpsi ν β` with `α <ᵇ β`; `bplus x y₂ <ᵇ bplus x z₂`
+with `y₂ <ᵇ z₂`) were "not constructible pending a K-free
+reformulation". The obstruction was first *reconfirmed* on Agda 2.8
+(the `Order.agda` comment cited 2.6.3): the *naive* `<ᵇ-irrefl`
+matches `x <ᵇ x`, and the shared binder forces the unifier through
+the reflexive equation `ν =?= ν`, whose elimination is the
+K-restricted *deletion* rule — rejected under `--without-K`. The
+constructors themselves were never the problem; the naive eliminator
+was.
+
+==== Action taken
+
+`proofs/agda/Ordinal/Buchholz/OrderExtendedDirect.agda` defines the
+extended direct relation `_<ᵇᵈ_` carrying *both* same-binder
+constructors and proves, `--safe --without-K`, **zero postulates /
+zero escape pragmas**:
+
+* `<ᵇ-irrefl` — via the generalised `<ᵇ⇒≢ : x <ᵇᵈ y → x ≡ y → ⊥`
+  (indices kept distinct, so no shared-binder unification arises),
+  the supplied equation discharged by `cong` of total projections
+  plus the K-free *conflict* rule. `refl` is never matched, so the
+  K-restricted deletion rule is never invoked;
+* `<ᵇ-trans` — full extended transitivity (the new constructors only
+  add ordinary constructor-pair clauses);
+* `embed : Order._<ᵇ_ ⇒ _<ᵇᵈ_` — conservativity: the K-free core
+  embeds faithfully; this is a strict extension, not a redefinition.
+
+Wired into `proofs/agda/All.agda`, pinned in `proofs/agda/Smoke.agda`;
+the full suite and smoke build green with it included.
+
+==== What is NOT earned back by this follow-up
+
+Well-foundedness of the *direct* relation. That is a
+termination-checker matter (Routes A/B of
+`docs/echo-types/buchholz-extended-wf.md`), orthogonal to K, and is
+**not** addressed here. WF stays delivered via the comparison
+*measure* `Ordinal.Buchholz.ExtendedOrder._<ᵇ⁺_`, which remains
+load-bearing exactly as before. Trichotomy/totality are out of scope.
+
+==== Artefacts edited 2026-05-18 pursuant to this follow-up
+
+`docs/echo-types/earn-back-plan.adoc` (ledger row B, recommended-order
+item 4, Status). No `paper.adoc` / `conservativity.adoc` /
+`types-abstract.adoc` edit — item B carries no claim in those.
+
+*Deferred doc-integrity follow-up (tracked, not duplicated).*
+`docs/echo-types/MAP.adoc` does not yet exist on `main` (it lands with
+the open Master-Map PR #54). To avoid an add/add duplication, its
+item-B status line is *not* copied here; the exact one-line
+replacement to apply *in or after #54* is: replace the bullet
+"`Known structural-fidelity gap on direct-constructor _<ᵇ_ (Buchholz
+item B in the earn-back ledger) — off the paper critical path.`" with
+"`Direct-constructor same-binder sub-cases (Buchholz item B) earned
+back K-free in Ordinal/Buchholz/OrderExtendedDirect.agda
+(F-2026-05-18b: irreflexivity + transitivity, zero postulates);
+residual WF stays via the ExtendedOrder._<ᵇ⁺_ measure. Off the paper
+critical path.`" The `[REAL]` section tag is unchanged.
+
 == Revision policy
 
 Append-only. New retractions get the next `R-YYYY-MM-DD` id. An entry

proofs/agda/All.agda

@@ -69,6 +69,7 @@ open import Ordinal.Buchholz.VeblenProjectionMeasure
 open import Ordinal.Buchholz.VeblenComparisonTarget
 open import Ordinal.Buchholz.VeblenComparisonModel
 open import Ordinal.Buchholz.ExtendedOrder
+open import Ordinal.Buchholz.OrderExtendedDirect
 open import Ordinal.Buchholz.LiftedExtendedOrder
 open import Ordinal.Buchholz.IteratedExtendedOrder
 open import Ordinal.Buchholz.RankBrouwer