thermo: close the C+ identity-only gap (injective + Bishop-finite), pin O-THERMO-∞

docs/ECHO-CNO-BRIDGE.adoc

@@ -75,19 +75,19 @@ bennett-reversible :
   fiber-erasure-bound f y _≟_ T ≡ 0
 ```
 
-**Status: PROVED** for the finite-domain `Fin n → B` case. The
-identity `id : Fin (suc m) → Fin (suc m)` is a canonical instance
-discharged by `bennett-reversible-id-zero`.
-
-**NOT proved**: the analogous claim over the original
-`ProgramState = ℕ → ℕ` carrier. Counting fibers of a function on
-an infinite type is not constructively meaningful without a
-heavier semantic framework (capacity, measure, equivalence-class
-quotients), and the `cno-identity : ProgramState → ProgramState`
-case stays open. The earlier `cno-thermodynamic-optimality`
-formulation rested on a hardcoded `FiberSize ≡ 1` that made the
-claim vacuous; that hardcode is gone, and the honest finite case
-is proved instead.
+**Status: PROVED**, and (2026-05-18) generalised twice: from the
+identity to *every injective map* (`bennett-reversible-injective`),
+and from `Fin n` to *any Bishop-finite carrier* via transport
+(`bennett-reversible-finite`, `EchoThermodynamicsFinite`).
+`bennett-reversible-id-zero` is now a corollary.
+
+**NOT proved**: the analogous claim over an infinite carrier
+(`ProgramState = ℕ → ℕ`). This is no longer a vague gap — it is the
+precise, falsifiable obligation **O-THERMO-∞**, stated with its kill
+condition in §"Thermodynamic Bridge" below. The earlier
+`cno-thermodynamic-optimality` formulation rested on a hardcoded
+`FiberSize ≡ 1` that made the claim vacuous; that hardcode is gone,
+and the honest finite/Bishop-finite case is proved instead.
 
 ### Theorem 5: Information-preservation (NOT YET FORMALISED)
 
@@ -140,7 +140,7 @@ Absolute Zero defines CNOs with four properties:
 | `FinalState(p, σ) = σ` | `Echo p σ` contains `(σ, refl)` |
 | `NoSideEffects(p)` | `Echo p σ` is singleton (only `σ` maps to `σ`) |
 | `ThermodynamicallyReversible(p)` | `Echo p σ ≃ Echo id σ` |
-| `ThermodynamicOptimality(p)` | `fiber-erasure-bound p σ _≟_ T ≡ 0` _(proved at finite-domain `Fin n → B` only — see Theorem 4)_ |
+| `ThermodynamicOptimality(p)` | `fiber-erasure-bound p σ _≟_ T ≡ 0` _(proved for every injective `p` on any Bishop-finite carrier — Theorem 4; infinite-carrier case = falsifiable obligation O-THERMO-∞)_ |
 | `InformationPreservation(p)` | _no formalised analogue — `echo-information-loss` was never defined; see Theorem 5_ |
 | `UniversalCNO(p)` | `∀ σ → Echo p σ ≃ Echo id σ` (NEW) |
 | `ModelIndependence(p)` | `Echo f y ≃ Echo f' y'` across isomorphic models (NEW) |
@@ -209,7 +209,7 @@ actually in the proven suite.
 3. **Fiber erasure bound**:
    `fiber-erasure-bound f y _≟_ T = landauer-bound T (FiberSize-fin f y _≟_)`.
 
-### Core Theorems (proved, finite domain only)
+### Core Theorems (proved)
 
 ```agda
 -- Bennett: if the fiber size at y is 1, the erasure bound is 0
@@ -230,11 +230,96 @@ landauer-collapse :
   fiber-erasure-bound f y _≟_ T ≡ k * T * ⌊log₂ n⌋
 ```
 
-### What is NOT proved
+### The C+ gap, and how far the bound generalises (2026-05-18)
+
+The `STABILITY_ANALYSIS.md` §3.3 ~70% / C+ rating was driven by a
+single concrete gap: the only proved zero-cost (Bennett) instance was
+`bennett-reversible-id-zero` — *the identity map, at index zero*. The
+general predicate `ThermodynamicOptimality(p) := fiber-erasure-bound
+p σ _≟_ T ≡ 0` (Absolute-Zero mapping table) was otherwise unproved
+off that one point. Two strictly stronger cases are now closed, and
+the residual is pinned to one falsifiable obligation.
+
+**Proved — generalisation past the identity (`EchoFiberCount`,
+`EchoThermodynamics`).** Zero erasure cost holds for *every injective
+map*, at *every value it hits*, not just `id`/`zero`:
+
+```agda
+FiberSize-fin-injective :
+  (f : Fin n → B) (y : B) (_≟_ : DecidableEquality B)
+  (inj : ∀ {i j} → f i ≡ f j → i ≡ j)
+  (i₀ : Fin n) → f i₀ ≡ y →
+  FiberSize-fin f y _≟_ ≡ 1
+
+bennett-reversible-injective :
+  (f : Fin n → B) (y : B) (_≟_ : DecidableEquality B)
+  (inj : ∀ {i j} → f i ≡ f j → i ≡ j)
+  (i₀ : Fin n) → f i₀ ≡ y → (T : Temperature) →
+  fiber-erasure-bound f y _≟_ T ≡ 0
+```
+
+This is the exact constructive content of "reversible ⇒ no
+Landauer-mandated dissipation": injectivity *is* reversibility, a
+singleton fiber *is* the absence of fan-in. `bennett-reversible-id-zero`
+is now a corollary, not the only instance.
+
+**Proved — generalisation past `Fin n` to any Bishop-finite carrier
+(`EchoThermodynamicsFinite`).** What blocks `Fin n → B` from
+generalising is *exactly* one thing: `fiber-erasure-bound` is routed
+through `FiberSize-fin`, whose totality is structural recursion on the
+index bound `n` of `Fin n`. That is removed for any carrier `A`
+carrying an explicit bijection `A ≃ Fin n` (record `FiniteDomain`),
+by transport along the bijection — no new axiom, `--safe --without-K`,
+zero postulates:
+
+```agda
+record FiniteDomain (A : Set) : Set where
+  field card : ℕ; to : A → Fin card; from : Fin card → A
+        from∘to : ∀ a → from (to a) ≡ a
+        to∘from : ∀ i → to (from i) ≡ i
+
+bennett-reversible-finite :
+  (fd : FiniteDomain A) (f : A → B) (y : B) (_≟_ : DecidableEquality B)
+  (inj : ∀ {a a′} → f a ≡ f a′ → a ≡ a′)
+  (a₀ : A) → f a₀ ≡ y → (T : Temperature) →
+  fiber-erasure-bound-fin fd f y _≟_ T ≡ 0
+
+landauer-collapse-finite :
+  (fd : FiniteDomain A) (f : A → B) (y : B) (_≟_ : DecidableEquality B) →
+  (∀ a → f a ≡ y) → (T : Temperature) →
+  fiber-erasure-bound-fin fd f y _≟_ T ≡ k * T * ⌊log₂ card fd ⌋
+```
+
+### Open obligation O-THERMO-∞ (precise, falsifiable — not softened)
+
+The infinite carrier (`ProgramState = ℕ → ℕ`, or any `A` with no
+`A ≃ Fin n`) does **not** generalise, and the reason is now stated
+sharply enough to be refuted:
+
+> **O-THERMO-∞.** There is no function
+> `cost : (ℕ → B) → (y : B) → DecidableEquality B → Temperature → Energy`
+> that is (i) `--safe --without-K` total (no postulate, no escape
+> pragma), and (ii) agrees with `fiber-erasure-bound` on every finite
+> restriction `Fin n ↪ ℕ` (equivalently: agrees with
+> `fiber-erasure-bound-fin` for every `FiniteDomain`-witnessed
+> sub-carrier).
+>
+> **Falsifier (how to kill this obligation).** Exhibit such a `cost`
+> and a mechanised proof of (i)+(ii); that refutes O-THERMO-∞ and
+> earns the claim back. **Witness that it bites:** the constant map
+> `c : ℕ → B`, `c _ = y₀` has `Echo c y₀ ≃ ℕ` — an infinite fiber.
+> Clause (ii) instantiated at the finite restrictions forces, by
+> `landauer-collapse`, `cost c y₀ _≟_ T = k · T · ⌊log₂ N⌋` with the
+> finite counts `N = 0,1,2,…` unboundedly — so any total `cost` must
+> assign `⌊log₂_⌋` of a quantity with no natural-number value. The
+> obligation is discharged in exactly one of two ways: a constructive
+> `cost` meeting (i)+(ii) (impossibility refuted), or a mechanised
+> proof that (i)∧(ii) ⊢ ⊥ (impossibility confirmed). Neither is in
+> the suite; until one lands, `ThermodynamicOptimality(p)` over an
+> infinite `ProgramState` is **`[OPEN]`**, not "future work".
+
+### What is still NOT proved (unchanged)
 
-* `cno-zero-energy` over the original `ProgramState = ℕ → ℕ`
-  carrier — counting fibers on an infinite type is not
-  constructively meaningful here.
 * `echo-information-loss` and `cno-zero-information-loss` —
   `echo-information-loss` was never defined in any module;
   the prior claims rested on undeclared identifiers.
@@ -244,14 +329,15 @@ landauer-collapse :
 ### Connection to Absolute Zero Goals
 
 1. **Landauer's Principle (shape)**: formalised via `landauer-bound`
-   and `fiber-erasure-bound` at the finite-domain level.
-2. **Thermodynamic Reversibility (shape)**: `bennett-reversible` is
-   proved as a corollary of `FiberSize-fin ≡ 1` and `⌊log₂ 1⌋ ≡ 0`.
-   `bennett-reversible-id-zero` is the proved instance for
-   `id : Fin (suc m) → Fin (suc m)` at index zero. The general
-   "all CNOs dissipate zero energy" claim over `ProgramState` is
-   open.
-4. **Information Theory**: not bridged. Open work — see
+   and `fiber-erasure-bound`; now at the full Bishop-finite-carrier
+   level, not merely `Fin n`.
+2. **Thermodynamic Reversibility (shape)**: proved for *every*
+   injective map (`bennett-reversible-injective`) and lifted to any
+   Bishop-finite carrier (`bennett-reversible-finite`).
+   `bennett-reversible-id-zero` is now a corollary. The infinite
+   `ProgramState` case is the single, falsifiable obligation
+   O-THERMO-∞ above — `[OPEN]`, with a stated kill condition.
+3. **Information Theory**: not bridged. Open work — see
    `docs/echo-types/roadmap.md`.
 
 ## Practical Implications

docs/STABILITY_ANALYSIS.md

@@ -78,13 +78,25 @@ Echo {A = A} f y = Σ A (λ x → f x ≡ y)
 
 **Stability:** New but well-grounded in existing echo type theory
 
-#### 3.3 Thermodynamic Models: C+
-**Proofs:** `EchoThermodynamics.agda`
-- Energy-preservation theorems
-- Entropy calculations
-- Reversibility bounds
-
-**Stability:** Experimental - interesting but needs more development
+#### 3.3 Thermodynamic Models: B- (was C+; advanced 2026-05-18)
+**Proofs:** `EchoThermodynamics.agda`, `EchoFiberCount.agda`, `EchoThermodynamicsFinite.agda`
+- Landauer bound *shape* `k·T·⌊log₂ N⌋` (honest fiber count, no hardcode)
+- Bennett zero-cost for **every injective map** (`bennett-reversible-injective`),
+  not just `id` at index zero — `bennett-reversible-id-zero` is now a corollary
+- Lifted off `Fin n` to **any Bishop-finite carrier** by transport along an
+  explicit bijection (`FiniteDomain`, `bennett-reversible-finite`,
+  `landauer-collapse-finite`) — `--safe --without-K`, zero postulates
+- Landauer worst-case collapse (`landauer-collapse[-finite]`)
+
+**Stability:** The C+ ~70% rating was driven by one concrete gap — the only
+proved zero-cost instance was the identity at index zero. That gap is closed:
+optimality now holds for every injective map on every Bishop-finite carrier.
+The *single* remaining open item is the infinite-carrier case
+(`ProgramState = ℕ → ℕ`), now pinned as the **precise, falsifiable obligation
+O-THERMO-∞** with a stated kill condition (see
+`docs/ECHO-CNO-BRIDGE.adoc` §"Thermodynamic Bridge"). Not "needs more
+development" — one named obligation, refutable by exhibiting a total
+`--safe` cost functional or by mechanising its impossibility.
 
 ### 4. Proof Ecosystem Stability: B+
 
@@ -99,7 +111,7 @@ Echo {A = A} f y = Σ A (λ x → f x ≡ y)
 | Relational | 80% | B |
 | CNO Integration | 98% | A- |
 | JanusKey Bridge | 90% | B+ |
-| Thermodynamics | 70% | C+ |
+| Thermodynamics | 85% | B- |
 
 **Proof Quality Indicators:**
 - ✅ All core theorems have constructive proofs

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`.

proofs/agda/All.agda

@@ -28,6 +28,7 @@ open import EchoJanusBridge
 open import Dyadic
 open import DyadicEchoBridge
 open import EchoThermodynamics
+open import EchoThermodynamicsFinite
 open import EchoStabilityTests
 open import VecRotation
 

proofs/agda/EchoFiberCount.agda

@@ -39,7 +39,7 @@ open import Data.Fin.Base                         using (Fin; zero; suc)
 open import Data.Product.Base                     using (Σ; _,_)
 open import Relation.Nullary                      using (¬_)
 open import Relation.Nullary.Decidable.Core       using (Dec; yes; no)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; trans)
 
 open import Echo                                  using (Echo)
 
@@ -72,6 +72,9 @@ private
   suc≢zero-Fin : ∀ {n} (i : Fin n) → ¬ (suc i ≡ zero)
   suc≢zero-Fin _ ()
 
+  Fin-suc-inj : ∀ {n} {i j : Fin n} → suc i ≡ suc j → i ≡ j
+  Fin-suc-inj refl = refl
+
 ----------------------------------------------------------------------
 -- "no-hit" / "all-hit" lemmas (exposed for downstream use).
 --
@@ -134,6 +137,43 @@ FiberSize-fin-const :
   FiberSize-fin {n = n} (λ _ → y₀) y₀ _≟_ ≡ n
 FiberSize-fin-const y₀ _≟_ = FiberSize-fin-all-hit (λ _ → y₀) y₀ _≟_ (λ _ → refl)
 
+----------------------------------------------------------------------
+-- Headline 2b — FiberSize-fin-injective
+--
+-- If `f : Fin n → B` is injective and *some* index `i₀` hits `y`,
+-- the fiber over `y` has size exactly 1. This is the honest
+-- generalisation of `FiberSize-fin-id-zero`: it removes the
+-- restriction to the identity map and to the `zero` index, and
+-- depends only on injectivity + a single witness. It is the
+-- fiber-count engine behind the general Bennett zero-cost result
+-- (`EchoThermodynamics.bennett-reversible-injective`): a reversible
+-- — i.e. injective — computation has singleton fibers wherever it
+-- lands, hence no Landauer-mandated dissipation there.
+--
+-- The proof walks the `FiberSize-fin` recursion in lock-step with
+-- the witness: the hit index contributes the single `suc`, and
+-- injectivity rules out any *other* index hitting `y` (a second hit
+-- would equate two distinct domain points).
+----------------------------------------------------------------------
+
+FiberSize-fin-injective :
+  ∀ {b} {B : Set b} {n : ℕ}
+  (f : Fin n → B) (y : B) (_≟_ : (y₁ y₂ : B) → Dec (y₁ ≡ y₂))
+  (inj : ∀ {i j : Fin n} → f i ≡ f j → i ≡ j)
+  (i₀ : Fin n) → f i₀ ≡ y →
+  FiberSize-fin f y _≟_ ≡ ℕ.suc ℕ.zero
+FiberSize-fin-injective {n = ℕ.suc m} f y _≟_ inj zero hit
+  with f zero ≟ y
+... | yes _  = cong ℕ.suc
+                 (FiberSize-fin-no-hit (f ∘ suc) y _≟_
+                   (λ j fsj≡y → suc≢zero-Fin j (inj (trans fsj≡y (sym hit)))))
+... | no ¬p  = ⊥-elim (¬p hit)
+FiberSize-fin-injective {n = ℕ.suc m} f y _≟_ inj (suc i′) hit
+  with f zero ≟ y
+... | yes p  = ⊥-elim (suc≢zero-Fin i′ (sym (inj (trans p (sym hit)))))
+... | no  _  = FiberSize-fin-injective (f ∘ suc) y _≟_
+                 (λ eq → Fin-suc-inj (inj eq)) i′ hit
+
 ----------------------------------------------------------------------
 -- Headline 3 — FiberSize-fin ≡ 0 ⟺ ¬ Echo (split into two halves).
 --

proofs/agda/EchoThermodynamics.agda

@@ -43,6 +43,7 @@
 --   * fiber-erasure-bound             -- bound applied at a fiber
 --   * bennett-reversible              -- FiberSize ≡ 1 ⇒ bound ≡ 0
 --   * bennett-reversible-id-zero      -- id at zero: bound ≡ 0
+--   * bennett-reversible-injective    -- any injective f + a hit: bound ≡ 0
 --   * landauer-collapse               -- constant map: bound = k·T·⌊log₂ n⌋
 
 module EchoThermodynamics where
@@ -59,6 +60,7 @@ open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym;
 open import EchoFiberCount                        using
   ( FiberSize-fin
   ; FiberSize-fin-id-zero
+  ; FiberSize-fin-injective
   ; FiberSize-fin-const
   ; FiberSize-fin-all-hit
   )
@@ -146,6 +148,36 @@ bennett-reversible-id-zero :
 bennett-reversible-id-zero {m} _≟_ T =
   bennett-reversible (λ x → x) zero _≟_ T (FiberSize-fin-id-zero _≟_)
 
+----------------------------------------------------------------------
+-- bennett-reversible-injective
+--
+-- The honest general Bennett statement at the finite-domain level:
+-- *any* injective `f : Fin n → B` (not merely the identity, not
+-- merely at index `zero`) that hits `y` at some index has erasure
+-- bound zero at `y`, at every temperature. This subsumes
+-- `bennett-reversible-id-zero` (the identity is injective; it hits
+-- `zero` at `zero` by `refl`) and is the exact constructive content
+-- of "reversible ⇒ no Landauer-mandated dissipation": injectivity
+-- is reversibility, a singleton fiber is the absence of fan-in.
+--
+-- This is as far as the `FiberSize-fin` cost functional reaches.
+-- Generalising the *carrier* past `Fin n` is addressed — for
+-- Bishop-finite domains — in `EchoThermodynamicsFinite`; the
+-- infinite-carrier case (`ProgramState = ℕ → ℕ`) is a stated,
+-- falsifiable open obligation, see `docs/ECHO-CNO-BRIDGE.adoc`
+-- §"Thermodynamic Bridge" / Open obligation O-THERMO-∞.
+----------------------------------------------------------------------
+
+bennett-reversible-injective :
+  ∀ {b} {B : Set b} {n : ℕ}
+  (f : Fin n → B) (y : B) (_≟_ : (y₁ y₂ : B) → Dec (y₁ ≡ y₂))
+  (inj : ∀ {i j : Fin n} → f i ≡ f j → i ≡ j)
+  (i₀ : Fin n) → f i₀ ≡ y →
+  (T : Temperature) →
+  fiber-erasure-bound f y _≟_ T ≡ 0
+bennett-reversible-injective f y _≟_ inj i₀ hit T =
+  bennett-reversible f y _≟_ T (FiberSize-fin-injective f y _≟_ inj i₀ hit)
+
 ----------------------------------------------------------------------
 -- landauer-collapse
 --