docs(proof-log): add 2026-04-28 — C1→A2→A1→B3 session log

Records the full session chain with decisions made and why:

* C1 — `FiberSize-fin` defined as pure recursive enumeration
  (no stdlib `count` shim); `bennett-reversible` parameterised
  by `FiberSize-fin ≡ 1` rather than a `Bijection f` typeclass
  input; infinite-domain `ProgramState = ℕ → ℕ` explicitly out
  of scope.
* A2 — `_⊑c_` defined as a one-way order on roles (Client →
  Server only) rather than an equivalence — keeps the join
  structure non-trivial.
* A1 — packaged via stdlib's `Function.Bundles._↔_` and
  `mk↔ₛ′`; per-fiber `(y : C) → ↔` rather than a global
  equivalence object.
* B3 — separate relation `_<ᵇ⁺_` rather than extending `_<ᵇ_`
  (preserves WF on the K-free core); explicit equality witness
  on shared-binder constructors (sidesteps K-restriction);
  four `extend-{lhs,rhs}` helpers for the mixed-shape trans
  cases.

Plus a "what I'd do differently" retrospective: try Route B
first for `_<ᵇ⁺_` WF (rank-embedding has a clearer failure
mode than Agda's structural-decrease checker); always force
clean Agda rebuild via `find -name '*.agdai' -delete` before
each task switch.

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

Author: hyperpolymath

docs/proof-log/2026-04-28.md

@@ -0,0 +1,205 @@
+# Proof-direction log — 2026-04-28
+
+## Session shape
+
+Recovery from 2026-04-28 morning XFS-induced crash, then a chain
+of four landed proof rungs:
+
+1. **C1** — redeem Landauer/Bennett bounds (PR #23, merged).
+2. **A2** — `EchoChoreo` per-decoration composition rung (PR #24, merged).
+3. **A1** — equivalence-record packaging for cancel-iso (PR #25, merged).
+4. **B3** — extended order `_<ᵇ⁺_` with shared-binder lex
+   constructors (this PR, in flight).
+
+Plus extensive cross-repo and cross-doc updates (CLAUDE.md, roadmap.md,
+overview.md, composition.md, taxonomy.md, ECHO-CNO-BRIDGE.adoc).
+
+The user requested all four in sequence ("do c1 then a2 then a1"
+followed by "yes" for B3) with the documentation pass at the end.
+
+## Decisions made and why
+
+### C1 — `FiberSize-fin` definition
+
+**Decision.** Pure recursive enumeration over `Fin n`, asking the
+decidable equality at each index. No `count` from stdlib (which
+isn't directly available at the right shape under the version we
+have).
+
+**Why.** Keeps the definition transparent, lets us prove the
+extremal lemmas (`-id-zero`, `-const`, `-no-hit`, `-all-hit`,
+`≡0⟺¬Echo`) by structural recursion on the same `Fin`-shape,
+no external dependencies.
+
+**Trade-off.** Quadratic-style proofs in some cases (e.g.
+`FiberSize-fin-id-zero` needs `fs-no-hit` for the `suc`-shifted
+tail). Acceptable at this scale.
+
+### C1 — `bennett-reversible` parameterised, not `Bijection`-typed
+
+**Decision.** `bennett-reversible` takes a `FiberSize-fin f y _≟_ ≡ 1`
+hypothesis directly, rather than a `Bijection f` typeclass-style
+input. The `bennett-reversible-id-zero` instance discharges the
+hypothesis for the canonical `id : Fin (suc m) → Fin (suc m)` at
+zero.
+
+**Why.** The user's spec mentioned "Bijection f" but the spec also
+explicitly noted "(a corollary of `FiberSize-fin id ≡ 1` and
+`⌊log₂ 1⌋ ≡ 0`)" — the corollary form IS the cleanest statement.
+Bringing in a real `Bijection` type would require either depending
+on stdlib's `Function.Bundles.Bijection` or rolling our own; both
+add ceremony for what's a one-line corollary.
+
+**Trade-off.** Callers wanting "if it's a bijection, the bound is
+zero" need to derive the FiberSize=1 fact themselves. Acceptable
+because the `id` instance is provided ready-made.
+
+### C1 — infinite-domain ProgramState explicitly out of scope
+
+**Decision.** Strip the `ProgramState = ℕ → ℕ` carrier and the
+trivial `cno-zero-energy-at-zero T=0` corollary from the new
+`EchoThermodynamics`. Document infinite-domain as out of reach
+in both the module preamble and `docs/ECHO-CNO-BRIDGE.adoc`.
+
+**Why.** Keeping the old infinite-domain machinery would invite
+future readers to mistake the trivial T=0 corollary for the full
+"CNOs dissipate zero energy" claim — exactly the original sin
+that made the deleted `ECHO-CNO-BRIDGE-SUMMARY.md` wrong.
+
+### A2 — `_⊑c_` as a one-way order, not an equivalence
+
+**Decision.** Restrict the choreographic-reachability order to
+`Client ⊑c Server` (one-way) plus reflexive self-loops. Three
+constructors (`c⊑c`, `c⊑s`, `s⊑s`).
+
+**Why.** The reverse `Server → Client` move via the same swap
+exists (swap is involutive), but including it would make `_⊑c_`
+an equivalence and collapse the join structure (every two roles
+would be mutually upper-bound). The whole point of the
+per-decoration composition rung is to test the recipe on a
+non-trivial order.
+
+**Trade-off.** Choreography in real life isn't directional this
+way. The order here is a pedagogical artefact, not a model of
+choreography. Documented as such in the module preamble.
+
+### A1 — packaging via `Function.Bundles._↔_` and `mk↔ₛ′`
+
+**Decision.** Use stdlib's `mk↔ₛ′` which takes `to`, `from`, and
+both `StrictlyInverse{ˡ,ʳ}` proofs. Both round-trips of the
+existing cancel-iso quartet feed in directly.
+
+**Why.** Keeps the package minimal — no need to define our own
+equivalence record. `mk↔ₛ′` builds the full `Inverse` (with
+`to-cong` / `from-cong` filled in via `≡.cong`). Downstream
+consumers can use any of the standard projections.
+
+**Trade-off.** Per-fiber `(y : C) → ↔` rather than a single global
+equivalence object. That's a consequence of the codomain `s y`
+varying with `y`; a global object would require a Σ-type or a
+reformulation. Per-fiber is the cleanest match for how
+`Echo (g ∘ f) y` is used downstream.
+
+### B3 — separate relation `_<ᵇ⁺_` rather than extending `_<ᵇ_`
+
+**Decision.** Define a new module `Ordinal.Buchholz.OrderExtended`
+with `_<ᵇ⁺_` (which lifts `_<ᵇ_` and adds `<ᵇ⁺-ψα`, `<ᵇ⁺-+2`),
+rather than adding the constructors directly to `_<ᵇ_`.
+
+**Why.** Adding the constructors to `_<ᵇ_` breaks the existing
+`wf-<ᵇ` proof's bundle structure. A single-mutual restructure
+that threads `Acc _<ᵇ_ α` and `Acc _<ᵇ_ β` through the bundle
+**and** uses `wf-<ᵇ` mutually was attempted twice today (once
+by this session, once by a parallel session) — both attempts
+produce code that scope-checks but fails Agda's termination
+checker on the `pred-bpsi-from → wf-<ᵇ → ...` cycle.
+
+**Trade-off.** Two relations now live side-by-side: the K-free
+core `_<ᵇ_` (with proven WF) and the extended `_<ᵇ⁺_` (with
+proven irrefl + trans, WF still open). Downstream consumers
+need to pick which one they need. Documented in
+`docs/echo-types/buchholz-extended-wf.md`; the next attempt
+should be Route B (rank-embedding into Brouwer).
+
+### B3 — explicit equality witness on `<ᵇ⁺-ψα` and `<ᵇ⁺-+2`
+
+**Decision.** Each constructor has the shape
+`∀ {ν₁ ν₂ α β} → ν₁ ≡ ν₂ → α <ᵇ β → bpsi ν₁ α <ᵇ⁺ bpsi ν₂ β`
+(equivalent for `+2`). The equality is an explicit argument, not
+an implicit binder identification.
+
+**Why.** The natural shape `bpsi ν α <ᵇ⁺ bpsi ν β` (sharing `ν`
+across both sides of `<ᵇ⁺`) triggers a reflexive `ν = ν` equation
+in irrefl's pattern unification, which `--without-K` rejects.
+Carrying the equality explicitly keeps all four constructor
+implicits as pattern variables, sidestepping the K-restriction.
+The equality is then NOT pattern-matched on `refl` in irrefl
+(matching `refl : x ≡ x` ALSO triggers K-restriction once the
+LHS/RHS of `<ᵇ⁺` have been unified to a common carrier); it is
+only matched in `<ᵇ⁺-trans` where the equality is on FRESH
+pattern variables, satisfying the Cockx–Sjöberg criterion.
+
+**Trade-off.** Callers must provide a `refl` argument explicitly
+(`<ᵇ⁺-ψα refl p`). Convenience wrappers `<ᵇ⁺-ψα-refl` and
+`<ᵇ⁺-+2-refl` paper over this for the common case.
+
+### B3 — four `extend-{lhs,rhs}` helpers in `<ᵇ⁺-trans`
+
+**Decision.** The mixed-shape transitivity cases
+(`base × shared-binder`) factor through four helper lemmas that
+walk the base witness's structure to swap the shared binder
+freely.
+
+**Why.** The base constructors that put `bpsi` (or `bplus`) on
+either side of `<ᵇ` (`<ᵇ-0-ψ`, `<ᵇ-Ωψ`, `<ᵇ-ψΩ`, `<ᵇ-+ψ`,
+`<ᵇ-ψ+`, etc.) do not constrain the relevant binder, so we can
+re-apply the constructor at a different binder value. The
+helpers make this explicit and bundle the case analysis once.
+
+**Trade-off.** Adds ~30 lines of explicit case work. Could be
+collapsed by using `cong` on a constructor parameter, but the
+explicit form is more readable.
+
+## Open at end of session
+
+* `_<ᵇ⁺_` well-foundedness — Route A failed twice, Route B is
+  the recommended next attempt. See
+  `docs/echo-types/buchholz-extended-wf.md`.
+* Brouwer Phase 1.3 limit case of `≤′-refl` — drafted by the
+  parallel session, reverted pending discharge.
+* Unbudgeted `_<ᵇʳᶠ_` global WF (pre-existing, not touched this
+  session).
+* C2 (Shannon-entropy formalisation), C3 (infinite-domain
+  Landauer), C4 (physical heat dissipation) — all noted in
+  roadmap.md as gated on prerequisites we don't have.
+
+## Files touched (this session, in order)
+
+* `proofs/agda/EchoFiberCount.agda` (new)
+* `proofs/agda/EchoThermodynamics.agda` (rewritten)
+* `proofs/agda/EchoStabilityTests.agda` (Section 2 rewritten)
+* `proofs/agda/All.agda` (wire EchoFiberCount + OrderExtended)
+* `proofs/agda/Smoke.agda` (pin all new headlines)
+* `proofs/agda/EchoChoreo.agda` (added _⊑c_ rung)
+* `proofs/agda/Echo.agda` (added Echo-comp-iso + cancel-iso packagers)
+* `proofs/agda/Ordinal/Buchholz/OrderExtended.agda` (new)
+* `docs/echo-types/composition.md` (rung sweep + cancel-iso closed)
+* `docs/echo-types/taxonomy.md` (§8 EchoFiberCount reference)
+* `docs/echo-types/roadmap.md` (rung-state refresh)
+* `docs/echo-types/overview.md` (Buchholz state refresh)
+* `docs/echo-types/buchholz-extended-wf.md` (new design note)
+* `docs/proof-log/2026-04-28.md` (this file)
+* `docs/ECHO-CNO-BRIDGE.adoc` (four overclaim sites swept)
+* `CLAUDE.md` (current rung state refresh)
+
+## What I'd do differently
+
+* **Try Route B first for `_<ᵇ⁺_` WF.** Two sessions burned on
+  Route A's termination problem; the rank-embedding route is
+  algebraic rather than proof-engineering and has a clearer
+  failure mode (a missing strict-monotonicity lemma is easier
+  to debug than Agda's structural-decrease checker).
+* **Verify build with `find -name '*.agdai' -delete` before each
+  task switch.** Cached `.agdai` files masked a broken
+  `WellFounded.agda` for several tool-invocations until I forced
+  a clean rebuild.