agda(B3): _<ᵇ⁺_ shared-binder lex constructors + WF design note + docs refresh (#26)

## Summary

- **Fixes broken main.** Commit \`e0f67cb\` added \`open import
Ordinal.Buchholz.OrderExtended\` to \`All.agda\` but did not commit the
file itself, leaving main with a dangling import (\`agda All.agda\`
exits 42). This PR ships the missing module.
- **B3 — shared-binder lex constructors.** New
\`Ordinal.Buchholz.OrderExtended.agda\` defining \`_<ᵇ⁺_\` with the two
K-restricted lex cases (\`<ᵇ⁺-ψα\`, \`<ᵇ⁺-+2\`); each constructor
carries an explicit equality witness so the K-free unifier never has to
eliminate a reflexive \`ν = ν\` (or \`x = x\`) equation. \`<ᵇ⁺-irrefl\`
and \`<ᵇ⁺-trans\` are proved (mixed cases via four private
\`extend-{lhs,rhs}\` helpers).
- **WF design note.** New \`docs/echo-types/buchholz-extended-wf.md\`
documents why \`wf-<ᵇ\` does not extend to \`_<ᵇ⁺_\` and the two design
routes (Route A: single-mutual restructure, attempted twice today and
blocked on Agda termination; Route B: rank-embedding into Brouwer
ordinals, recommended next attempt).
- **Doc refresh.** \`CLAUDE.md\` current rung state, \`composition.md\`
decoration sweep, \`roadmap.md\` status flags, \`overview.md\` Buchholz
paragraph, \`docs/proof-log/2026-04-28.md\` (NEW) full session log with
decisions made.

## Why

Two parallel sessions today both attempted to add \`<ᵇ-ψα\` and
\`<ᵇ-+2\` directly to \`_<ᵇ_\` and rebuild the WF proof as a single
mutual block. Both attempts produce code that scope-checks but fails
Agda's termination checker on the same cycle through \`wf-<ᵇ\`. The
pragmatic interim is to keep the K-free core \`_<ᵇ_\` (with proven
\`wf-<ᵇ\`) intact and define the lex extension in a sibling relation
\`_<ᵇ⁺_\` whose well-foundedness is documented as the next open step.

## What is NOT in this PR

- \`_<ᵇ⁺_\` well-foundedness — see \`buchholz-extended-wf.md\` for two
attempt routes.
- Brouwer Phase 1.3 limit case of \`≤′-refl\` — drafted by parallel
session in commit \`e0f67cb\`, deferred there.
- Reverting the broken \`OrderExtended\` import on main other than by
adding the file (alternative would be to remove the import; we ship the
file because its content is independently valuable).

## Compile-verification

\`\`\`
agda -i proofs/agda proofs/agda/All.agda
agda -i proofs/agda proofs/agda/Smoke.agda
\`\`\`

Both exit 0 under \`--safe --without-K\`. No postulates introduced.

## Test plan

- [ ] \`agda -i proofs/agda proofs/agda/All.agda\` exits 0
- [ ] \`agda -i proofs/agda proofs/agda/Smoke.agda\` exits 0
- [ ] \`grep -n postulate
proofs/agda/Ordinal/Buchholz/OrderExtended.agda\` returns nothing
- [ ] \`<ᵇ⁺-base\`, \`<ᵇ⁺-ψα\`, \`<ᵇ⁺-+2\`, \`<ᵇ⁺-irrefl\`,
\`<ᵇ⁺-trans\`, plus convenience wrappers all pinned in \`Smoke.agda\`

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Author: hyperpolymath

CLAUDE.md

@@ -138,9 +138,106 @@ work to `main` and refresh all documentation:
    name, the commits folded in, the remaining open pieces of the
    milestone, and the proposed smallest useful next advance.
 
-## Current rung state (2026-04-27)
+## Current rung state (2026-04-28)
+
+Just landed: **Honest-thermo rung + 5-decoration sweep close +
+cancel-iso packaging + extended-order lex constructors.** Five
+PRs merged to `main` in one chain (#23, #24, #25, plus B3 in this
+commit, plus the doc + 6a2 sweep). Headlines:
+
+### C1 — `EchoFiberCount` + redeemed `EchoThermodynamics` (PR #23)
+
+* `EchoFiberCount.FiberSize-fin : (Fin n → B) → B → DecEq → ℕ` —
+  honest preimage count by enumeration.
+* Headlines: `FiberSize-fin-id-zero` (id has fiber 1),
+  `FiberSize-fin-const` (constant collapse: fiber n),
+  `FiberSize-fin-{no,all}-hit`,
+  `FiberSize-fin≡0⇒no-echo`, `no-echo⇒FiberSize-fin≡0`.
+* `EchoThermodynamics` rewritten against `Data.Nat.Logarithm.⌊log₂_⌋`:
+  `landauer-bound T n = k * T * ⌊log₂ n ⌋`,
+  `bennett-reversible : FiberSize-fin ≡ 1 ⇒ erasure-bound ≡ 0`,
+  `bennett-reversible-id-zero` (concrete instance),
+  `landauer-collapse : (∀ x → f x ≡ y) ⇒ bound ≡ k·T·⌊log₂ n⌋`.
+* `docs/ECHO-CNO-BRIDGE.adoc` swept: four overclaim sites at
+  lines 71/80/122/174 replaced with honest "proved at finite
+  domain only" or explicit "NOT proved" notes.
+* `docs/echo-types/taxonomy.md` §8 references EchoFiberCount as
+  the quantitative companion to EchoDecidable.
+
+### A2 — `EchoChoreo` per-decoration composition rung (PR #24)
+
+* `_⊑c_` (3 constructors) — choreographic-reachability order on
+  roles (Client one-way to Server via the canonical `client-to-server`
+  swap-square).
+* `⊑c-trans`, `⊑c-prop` — transitive + propositional.
+* `applyChoreo`, `applyChoreo-comp` — transport + decomposition.
+* `_⊔c_` with `⊑c-⊔c-{left, right, univ}` — join (Server top).
+* `applyChoreo-compose`, `applyChoreo-via-join` — factoring-free
+  composition + join restatement.
+* Closes the **five-decoration sweep** at the per-decoration
+  composition rung (grade, linear, indexed, modal, role).
+* `docs/echo-types/composition.md` §6 marked sweep closed.
+
+### A1 — Equivalence-record packaging for cancel-iso (PR #25)
+
+* `Echo.Echo-comp-iso : (f : A → B) (g : B → C) (y : C) →
+  Echo (g ∘ f) y ↔ Σ B (λ b → Echo f b × g b ≡ y)` —
+  unconditional accumulation iso, packaged via stdlib's
+  `Function.Bundles._↔_` and `mk↔ₛ′`.
+* `Echo.cancel-iso : ... → Echo (g ∘ f) y ↔ Echo f (s y)` —
+  per-fiber cancellation equivalence, parameterised by `s-left`,
+  `s-right`, and both triangle identities.
+* Closes `composition.md` §4 ("Full cancel-iso with round-trips").
+
+### B3 — Extended order `_<ᵇ⁺_` with shared-binder lex constructors
+
+* New module `Ordinal.Buchholz.OrderExtended.agda`. Adds two
+  lex constructors that the K-restriction kept out of the core
+  `_<ᵇ_`:
+  * `<ᵇ⁺-ψα : ∀ {ν₁ ν₂ α β} → ν₁ ≡ ν₂ → α <ᵇ β → bpsi ν₁ α <ᵇ⁺ bpsi ν₂ β`
+  * `<ᵇ⁺-+2 : ∀ {x₁ x₂ y₁ y₂} → x₁ ≡ y₁ → x₂ <ᵇ y₂ → bplus x₁ x₂ <ᵇ⁺ bplus y₁ y₂`
+* Each constructor carries an explicit equality witness so the
+  implicits are pairwise distinct — the K-free unifier never
+  has to eliminate a reflexive `ν = ν` (or `x = x`) equation.
+* `<ᵇ⁺-irrefl`, `<ᵇ⁺-trans` proved (the `_<ᵇ⁺_` × `_<ᵇ_` mixed
+  cases route through four extension helpers
+  `bpsi-extend-{lhs,rhs}`, `bplus-extend-{lhs,rhs}`).
+* **Well-foundedness for `_<ᵇ⁺_` is OPEN.** Two design routes
+  documented in `docs/echo-types/buchholz-extended-wf.md`:
+  Route A (single-mutual block with widened bundle, attempted
+  but blocked on Agda's termination checker) and Route B
+  (rank-embedding into Brouwer ordinals, recommended
+  next-attempt). The K-free core `_<ᵇ_` and its `wf-<ᵇ` proof
+  remain intact.
+* New convenience wrappers `<ᵇ⁺-ψα-refl`, `<ᵇ⁺-+2-refl` for
+  callers with concrete same-binder cases.
+
+All headlines pinned in `Smoke.agda`. `agda proofs/agda/All.agda`
+and `agda proofs/agda/Smoke.agda` both exit 0 under
+`--safe --without-K`. No postulates introduced.
+
+### Open at this rung
+
+* `_<ᵇ⁺_` well-foundedness (see `buchholz-extended-wf.md`).
+  Two routes documented; the single-mutual restructure (Route A)
+  was attempted twice in 2026-04-28 sessions and both attempts
+  failed Agda's termination checker for the same cycle through
+  `wf-<ᵇ`. Rank-embedding (Route B) into Brouwer ordinals is the
+  recommended next attempt — needs a `rank : BT → Ord` function
+  plus the strict-monotonicity lemmas listed in the design note.
+* Brouwer Phase 1.3 (recursive `_≤′_` and `_<′_`) — drafted by
+  the parallel session with `osuc-mono-≤′ p = p` and the limit
+  case of `≤′-refl` deferred; module reverted pending the
+  limit-case discharge.
+* Unbudgeted `_<ᵇʳᶠ_` global WF (see Previous rung state).
+* Push the surface-route WF back into `Order.agda`'s main
+  `_<ᵇ_` package once `_<ᵇ⁺_` WF lands.
 
-Just landed: **Per-decoration composition rung** across
+---
+
+## Previous rung state (2026-04-27)
+
+Landed: **Per-decoration composition rung** across
 `EchoGraded.agda` and `EchoLinear.agda`. Both decorations commute
 with composition under the same recipe (decoration order →
 propositionality → join → factoring-free compose → via-join

docs/echo-types/buchholz-extended-wf.md

@@ -0,0 +1,139 @@
+# Buchholz `_<ᵇ⁺_`: well-foundedness gap
+
+`Ordinal.Buchholz.OrderExtended._<ᵇ⁺_` adds two shared-binder lex
+constructors on top of `Ordinal.Buchholz.Order._<ᵇ_`:
+
+* **`<ᵇ⁺-ψα`** — `bpsi ν α <ᵇ⁺ bpsi ν β` whenever `α <ᵇ β`
+  (lex on the ψ-argument at a fixed Ω-index).
+* **`<ᵇ⁺-+2`** — `bplus x y₁ <ᵇ⁺ bplus x y₂` whenever `y₁ <ᵇ y₂`
+  (lex on the right summand at a fixed left summand).
+
+`<ᵇ⁺-irrefl` and `<ᵇ⁺-trans` are proved. **Well-foundedness for
+`_<ᵇ⁺_` is open.** This note records why and sketches the two
+viable design routes.
+
+## Why `wf-<ᵇ` does not extend directly
+
+`Ordinal.Buchholz.WellFounded.wf-<ᵇ` is built from a per-Ω-index
+bundle:
+
+```agda
+ΩBundle μ = Acc _<ᵇ_ (bOmega μ) × ((α : BT) → Acc _<ᵇ_ (bpsi μ α))
+
+<ᵇ-bundle-fromΩ : ∀ {μ} → Acc _<Ω_ μ → ΩBundle μ
+```
+
+The bundle's `psiAcc α` returns `Acc _<ᵇ_ (bpsi μ α)` for any `α`,
+discharging predecessors via case analysis on `_<ᵇ_`'s
+constructors. The new `<ᵇ⁺-ψα` constructor introduces predecessors
+shaped `bpsi μ β` for arbitrary `β <ᵇ α`. Discharging those needs
+recursion on `Acc _<ᵇ_ α` — but `psiAcc` does not carry an `Acc α`
+argument, so the natural attempt
+
+```agda
+predPsi α (<ᵇ-ψα {α = β} refl _) = psiAcc β
+```
+
+calls `psiAcc β` with `β` strictly smaller than `α` only via
+`<ᵇ`, not structurally. Agda's termination checker rejects the
+mutual cycle `predPsi → psiAcc → predPsi` because the first
+argument does not decrease.
+
+Symmetrically, `<ᵇ⁺-+2` introduces predecessors `bplus α y₁` for
+arbitrary `y₁ <ᵇ y₂`, and the existing `<ᵇ-acc-bplus-from` only
+threads `Acc _<ᵇ_ α` (the left summand), so the right-summand lex
+case has no decreasing measure either.
+
+## Two design routes
+
+### Route A — single-mutual block with widened bundle
+
+Replace the per-Ω-index bundle with a single mutual block in
+which:
+
+```agda
+ΩBundle μ = Acc _<ᵇ_ (bOmega μ)
+          × ((α : BT) → Acc _<ᵇ_ α → Acc _<ᵇ_ (bpsi μ α))
+
+<ᵇ-acc-bplus-from-both :
+  ∀ {α β} → Acc _<ᵇ_ α → Acc _<ᵇ_ β → Acc _<ᵇ_ (bplus α β)
+```
+
+i.e. the ψ-side of the bundle takes `Acc _<ᵇ_ α` as a parameter,
+and `bplus`-acc takes `Acc _<ᵇ_` for **both** summands. `wf-<ᵇ`
+becomes mutual with the bundle and supplies the extra `Acc` args
+via BT structural recursion (`wf-<ᵇ α` for the smaller subterm).
+
+**Status of attempt.** Drafted twice (in this PR and again by a
+parallel session on 2026-04-28); both attempts are
+constructionally identical and both are rejected by Agda's
+termination checker. The reported cycle is
+`pred-bpsi-from → wf-<ᵇ → <ᵇ-acc-bpsi → <ᵇ-acc-bpsi-from`. The
+cycle is well-founded in lex order on
+`(BT-structure of carrier, witness)`, but Agda does not see the
+witness as decreasing the BT carrier without an explicit
+size-measure annotation. A sized-types or explicit measure
+encoding (e.g. via `Induction.WellFounded.<-rec` with a measure
+into ℕ × ℕ) is the next thing to try; failing that, fall back
+to Route B.
+
+### Route B — rank-embedding into Brouwer ordinals
+
+Define `rank : BT → Ord` (Brouwer, already present in
+`Ordinal.Brouwer`) such that `x <ᵇ⁺ y → rank x < rank y`. Then
+WF for `_<ᵇ⁺_` follows from `Ordinal.Brouwer.wf-<` by
+transport along `rank`.
+
+Sketch of `rank`:
+
+```agda
+rank bzero        = oz
+rank (bOmega μ)   = ω-rank μ
+rank (bplus α β)  = rank α ⊕ rank β
+rank (bpsi μ α)   = psi-rank μ ⊕ rank α   -- conjectural form
+```
+
+The arithmetic infrastructure (`_⊕_`, `nat-to-ord`, `ω-rank`,
+`psi-rank`) is in `Ordinal.Brouwer.Arithmetic`. The strict
+decrease must hold on every `<ᵇ⁺` constructor:
+
+* `<ᵇ-ψΩ μ<ν` — Ω-index decrease must dominate the ψ-arg
+  comparison; needs `psi-rank` to be strictly monotone in μ at a
+  rate that swamps `_⊕_`-additions of the ψ-arg.
+* `<ᵇ⁺-ψα` — ψ-arg strict decrease at fixed μ; needs
+  `psi-rank μ ⊕ ·` to preserve `<` on the right.
+* `<ᵇ⁺-+2` — right-summand strict decrease at fixed left;
+  needs `· ⊕ rank α` to be `<`-monotone on the left.
+
+**Status.** Not attempted yet. The constructive Brouwer-ordinal
+arithmetic in this repo is light (Phase 1.1/1.2); some of the
+strict-monotonicity lemmas the `rank` proof would need are not
+yet present.
+
+## Pragmatic interim — leave `_<ᵇ_` and `_<ᵇ⁺_` separate
+
+Today's commit ships the constructors in `_<ᵇ⁺_` only, leaving
+`Ordinal.Buchholz.Order._<ᵇ_` (and its `wf-<ᵇ`) intact. Downstream
+consumers that need only the K-free core (e.g. the
+`VeblenComparisonModel` chain) keep their existing WF guarantee.
+Consumers that need the lex cases use `_<ᵇ⁺_` and accept that
+WF is not yet established for it.
+
+## Recommended next attempt
+
+Route B (rank-embedding) is lower-risk: the arithmetic lemmas
+needed are bounded and discoverable, and `Ordinal.Brouwer.wf-<`
+is already proved. Route A's failure mode is Agda's termination
+checker, which is harder to debug than provable mathematics.
+
+## See also
+
+* `proofs/agda/Ordinal/Buchholz/Order.agda` — the K-free core.
+* `proofs/agda/Ordinal/Buchholz/OrderExtended.agda` — the
+  extended relation defined in this PR.
+* `proofs/agda/Ordinal/Buchholz/WellFounded.agda` — the bundle
+  proof for `_<ᵇ_`.
+* `proofs/agda/Ordinal/Brouwer.agda`,
+  `proofs/agda/Ordinal/Brouwer/Arithmetic.agda` — the rank
+  target if Route B is taken.
+* `docs/buchholz-plan.adoc` — the broader Buchholz workstream.

docs/echo-types/overview.md

@@ -96,10 +96,14 @@ maps can admit different echo types.
   Buchholz workstream in this repo (`docs/buchholz-plan.adoc`) is a
   parallel, syntactic development; its relationship to Echo Types
   via `EchoOrdinal.agda` is a bridge, not a reduction. At present,
-  the current admitted Buchholz core has a closed well-foundedness
-  route, and finite same-binder depth is now handled by iterated
-  mediated wrappers, while the full intended order remains open at
-  the shared-binder internalization step.
+  the current K-free Buchholz core (`Ordinal.Buchholz.Order._<ᵇ_`)
+  has a closed well-foundedness route, finite same-binder depth is
+  handled by iterated mediated wrappers, and the shared-binder lex
+  cases (`<ᵇ⁺-ψα`, `<ᵇ⁺-+2`) are now internalised in the extended
+  relation `Ordinal.Buchholz.OrderExtended._<ᵇ⁺_` with proven
+  irrefl + trans; well-foundedness for `_<ᵇ⁺_` is the next open
+  step, with two design routes documented in
+  `docs/echo-types/buchholz-extended-wf.md`.
 - **Not a completed categorical semantics.** See
   `docs/assessment.adoc` for the current M5 verdict.
 

docs/echo-types/roadmap.md

@@ -53,11 +53,15 @@ Paths marked **[unblocked]** can proceed today. Paths marked
   isomorphism `Echo(g ∘ f) y ≃ Σ B (λ b → Echo(f) b × (g b ≡ y))`.
   Shipped as `Echo-comp-iso-{to, from, from-to, to-from}`; both
   round-trips are definitional. See `composition.md` §1.
-- **[partial]** `cancel-iso-to` / `cancel-iso-from` in `Echo.agda`:
-  forward and backward maps for the cancellation corollary, each
-  needing only the relevant half of g's iso structure. Round-trips
-  are **deferred** pending a triangle-identity coherence or a stdlib
-  `Function.Bundles.Inverse` shim. See `composition.md` §3.
+- **[landed]** `cancel-iso-to` / `cancel-iso-from` /
+  `cancel-iso-from-to` / `cancel-iso-to-from` in `Echo.agda`,
+  packaged as `Echo.cancel-iso : ... → Echo (g ∘ f) y ↔ Echo f (s y)`
+  via stdlib's `Function.Bundles._↔_` and `mk↔ₛ′`. Both round-trips
+  parameterised by their respective triangle identities (one
+  triangle implies the other in HoTT but the adjustment is
+  non-trivial path algebra, so both stay explicit). Companion
+  `Echo.Echo-comp-iso` packages the unconditional accumulation iso
+  the same way. See `composition.md` §3 + §4.
 - **[landed]** Pentagon coherence for three-fold composition.
   Projection lemmas `Echo-comp-iso-pent-B` and `Echo-comp-iso-pent-echo`
   both `refl` in `Echo.agda`. The full Σ-associativity iso between the
@@ -88,23 +92,37 @@ Paths marked **[unblocked]** can proceed today. Paths marked
   (monotone in ε), and `echo-approx-compose` (additive composition
   under a non-expansive outer leg, realising the taxonomy §2
   conjecture). Wired into `All.agda` and `Smoke.agda`.
-- **[partial]** Per-decoration composition lemmas in `EchoGraded`,
-  `EchoLinear`, `EchoIndexed`, `EchoChoreo`, `EchoEpistemic`: check
-  each commutes with basic composition. Grade case **landed** in
-  `EchoGraded.agda` as `degrade-compose` (any factoring of a
-  `g1 ≤g g3` transition through an intermediate `g2` collapses to
-  the same degraded echo) plus `degrade-via-join` (same statement
-  through the join `_⊔g_`), proved from `≤g-prop` (the order is
-  propositional) and `degrade-comp`. Supporting lemmas
-  `≤g-⊔g-left`, `≤g-⊔g-right`, `≤g-⊔g-univ` exhibit `_⊔g_` as the
-  categorical join. Linear case **landed** in `EchoLinear.agda` as
-  `_≤m_`, `≤m-trans`, `degradeMode`, and `degradeMode-comp`
-  (`linear ⊑ linear ⊑ affine ⊑ affine`; `degradeMode-comp` is the
-  per-decoration composition lemma; auxiliary corollaries
-  `degradeMode-id-linear`, `degradeMode-id-affine`,
-  `degradeMode-strict-is-weaken` make the relationship to the
-  existing `weaken` definitional). Indexed / role / modal cases
-  remain unblocked.
+- **[landed]** Per-decoration composition lemmas across the
+  five-decoration family — **sweep complete** (2026-04-28):
+  `EchoGraded.degrade-compose`, `EchoLinear.degradeMode-compose`,
+  `EchoIndexed.map-role-indexed-comp`,
+  `EchoChoreo.applyChoreo-{comp, compose, via-join}` along the
+  choreographic-reachability order `_⊑c_`, and
+  `EchoEpistemic.knowledge-monotone-{comp, id}`. Each follows the
+  same recipe (decoration order → propositionality → join →
+  factoring-free compose → via-join restatement). All headlines
+  pinned in `Smoke.agda`.
+- **[landed]** Honest finite-domain Landauer/Bennett bounds
+  (2026-04-28). `EchoFiberCount.agda` provides the actual fiber
+  count `FiberSize-fin : (Fin n → B) → B → DecEq → ℕ` plus four
+  headline lemmas (`FiberSize-fin-id-zero`, `FiberSize-fin-const`,
+  bidirectional `FiberSize-fin ≡ 0 ⟺ ¬ Echo`).
+  `EchoThermodynamics.agda` rewritten against
+  `Data.Nat.Logarithm.⌊log₂_⌋`: `bennett-reversible`,
+  `bennett-reversible-id-zero`, `landauer-collapse`. Replaces the
+  earlier `FiberSize = 1` hardcode that rendered the prior
+  CNO-zero-energy claims vacuous. Infinite-domain
+  (`ProgramState = ℕ → ℕ`) case explicitly out of scope.
+  `docs/ECHO-CNO-BRIDGE.adoc` swept to remove four overclaim sites.
+- **[partial]** Buchholz extended order `_<ᵇ⁺_` (2026-04-28).
+  `Ordinal.Buchholz.OrderExtended.agda` adds the two K-restricted
+  shared-binder lex constructors (`<ᵇ⁺-ψα`, `<ᵇ⁺-+2`) on top of
+  the K-free core `_<ᵇ_`, with explicit equality witnesses to
+  keep implicits pairwise distinct. `<ᵇ⁺-irrefl` and `<ᵇ⁺-trans`
+  proved (mixed cases via four `extend-{lhs, rhs}` helpers).
+  Well-foundedness for `_<ᵇ⁺_` is **OPEN** — see
+  `docs/echo-types/buchholz-extended-wf.md` for the two design
+  routes (single-mutual or rank-embedding via Brouwer).
 - **[unblocked]** Add example-library Agda files matching
   `examples.md`: start with examples 1–4 already in-suite, then
   example 7 (ordinal collapse is in `EchoOrdinal`); examples 5, 6,
@@ -153,22 +171,30 @@ Paths marked **[unblocked]** can proceed today. Paths marked
 
 ## Proof-assistant-dependent work — gated
 
-- **[gated on B1]** Internalize the missing shared-binder shapes as
-  actual constructors/comparison principles of the real Buchholz
-  order. The current route closes well-foundedness for the admitted
-  core and handles arbitrary finite same-binder depth via iterated
-  wrappers, but not yet for the full intended constructor package.
-- **[gated on B1]** Re-close totality/inversion/transitivity and
-  well-foundedness for the enlarged order after that internalization,
-  including shared-binder cases such as `<ᵇ-ψα` and `<ᵇ-+2`.
+- **[partial]** Internalize the missing shared-binder shapes as
+  actual constructors of the Buchholz order. **Done** for the
+  irrefl + trans layer in `Ordinal.Buchholz.OrderExtended._<ᵇ⁺_`
+  with `<ᵇ⁺-ψα` and `<ᵇ⁺-+2` (2026-04-28). Well-foundedness for
+  the enlarged order is open — see the gated entry below.
+- **[gated on `_<ᵇ⁺_` WF]** Re-close well-foundedness for the
+  enlarged order. Two design routes documented in
+  `docs/echo-types/buchholz-extended-wf.md`: single-mutual block
+  with widened bundle (Route A — attempted, blocked on Agda
+  termination) or rank-embedding into Brouwer ordinals (Route B
+  — recommended next-attempt; scaffolded by
+  `Ordinal.Buchholz.RankBrouwer.agda` from the parallel session).
 - **[gated on B1]** Ordinal semantics of BT terms: denotation
   `BT → Ordinal` preserving order. Requires a formal `Ordinal` type
   as a prerequisite, which is itself downstream of WF.
-- **[gated on B1]** Landauer / Shannon rigorous bridge (separate
-  handoff pack in `docs/echo-types/roadmap.md` would cross-reference
-  this). The current `EchoThermodynamics.agda` is a stub; genuine
-  content requires a preimage-count that itself needs ordinal / finite
-  type infrastructure.
+- **[partial]** Landauer / Shannon rigorous bridge. **Done** for
+  the finite-domain Landauer/Bennett shape in
+  `EchoThermodynamics.agda` (rewritten 2026-04-28 against
+  `EchoFiberCount.FiberSize-fin` and `Data.Nat.Logarithm.⌊log₂_⌋`).
+  Open: infinite-domain `ProgramState = ℕ → ℕ` extension (needs a
+  capacity / measure / equivalence-class-quotient framework);
+  Shannon-entropy formalisation (no probability-monad in stdlib v2
+  at the level needed); physical heat-dissipation realisation
+  (the bound is information-theoretic, not a physical claim).
 - **[gated on B2]** CNO-equivalence verification across echo-types
   and `absolute-zero`. Needs cross-repo access.
   Bridge slot now exists on the adjacent side at