echo-types: MAP.adoc — Thermodynamic Directions status tag (governance)

Per MAP.adoc governance rule "update the relevant Directions entry
*and* its status tag in the same PR". Thermodynamic entry stays
[REAL*] (real, still partial) but the description now records: Bennett
zero-cost generalised to every injective map on any Bishop-finite
carrier; identity-at-zero is a corollary; sole residual = falsifiable
obligation O-THERMO-∞; re-rated B-/~85% (was C+/~70%).

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

Author: hyperpolymath

docs/echo-types/MAP.adoc

@@ -53,11 +53,18 @@ remainder of information-losing computation: for `f : A → B`,
 == Directions
 
 === Thermodynamic — Landauer/Bennett energy bounds `[REAL*]`
-Finite-domain Landauer/Bennett bounds; `ThermodynamicallyReversible(p)
-≙ Echo p σ ≃ Echo id σ`. Rated ~70% / C+ in STABILITY_ANALYSIS.
+Landauer/Bennett bound *shape*; `ThermodynamicallyReversible(p)
+≙ Echo p σ ≃ Echo id σ`. Zero-cost (Bennett) proved for *every
+injective map* on *any Bishop-finite carrier* (transport along an
+explicit bijection); the identity-at-zero instance is now a corollary.
+Sole residual is the infinite-carrier case, pinned as the falsifiable
+obligation **O-THERMO-∞** (kill condition stated). Re-rated B- / ~85%
+in STABILITY_ANALYSIS §3.3 (was C+ / ~70%, 2026-05-18). Stays `[REAL*]`
+— real, still partial — until O-THERMO-∞ is discharged or refuted.
 
 * Proofs: `proofs/agda/EchoThermodynamics.agda`,
-  `proofs/agda/EchoFiberCount.agda`.
+  `proofs/agda/EchoFiberCount.agda`,
+  `proofs/agda/EchoThermodynamicsFinite.agda`.
 * Docs: `docs/ECHO-CNO-BRIDGE.adoc` §"Thermodynamic Bridge",
   `docs/STABILITY_ANALYSIS.md` §3.3, `docs/WORK_PLAN.md` §5,
   `docs/adjacency/hott-fibers.adoc`.