echo-types: Bennett zero-cost on an arbitrary carrier (past Bishop-finite)

Steps 1-3 of the thermodynamic-bridge continuation, stacked on PR #58.

1. EchoThermodynamicsArbitrary: FiberSubsingleton (K-free, --without-K
   safe surrogate for fibre isProp) + injective⇒fiber-subsingleton for
   an arbitrary carrier A : Set a (no Fin, no FiniteDomain).
2. reversible-erasure-cost (occupancy-keyed) + bennett-reversible-
   arbitrary: Bennett zero-cost for every injective map on any carrier,
   no finiteness. Anti-vacuity: occupancy≡FiberSize-fin and
   bennett-arbitrary-refines-finite certify the structural cost
   coincides with PR #58's established count and strictly subsumes it.
3. cno-identity over the genuine infinite absolute-zero Program carrier;
   bennett-reversible-cno-identity makes 'a CNO dissipates zero Landauer
   energy' a real theorem, not the historically vacuous claim.

EchoFiberCount: added FiberSize-fin-subsingleton (Headline 2c), the
finite-domain anti-vacuity hook (FiberSize-fin-injective is its
corollary; kept as-is upstream for pin stability).

O-THERMO-∞ unchanged and NOT discharged: re-narrowed in docs to be
specifically the quantitative-collapse functional on an infinite
carrier (orthogonal to the now-closed Bennett zero direction).

All --safe --without-K, zero postulates, zero escape pragmas.
Smoke.agda + All.agda exit 0. Docs (ECHO-CNO-BRIDGE §Thermodynamic
Bridge, STABILITY_ANALYSIS §3.3 ~90%/B-, MAP.adoc status tag) updated
in the same PR per the MAP governance rule.

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

Author: hyperpolymath

docs/ECHO-CNO-BRIDGE.adoc

@@ -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 for every injective `p` on any Bishop-finite carrier — Theorem 4; infinite-carrier case = falsifiable obligation O-THERMO-∞)_ |
+| `ThermodynamicOptimality(p)` | `reversible-erasure-cost p σ d T ≡ 0` _(proved for every injective `p` on **any** carrier — Bishop-finite via `fiber-erasure-bound`, arbitrary/infinite incl. the `Program` CNO via `reversible-erasure-cost` — Theorem 4; the quantitative-collapse functional on an infinite carrier is the 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) |
@@ -290,11 +290,64 @@ landauer-collapse-finite :
   fiber-erasure-bound-fin fd f y _≟_ T ≡ k * T * ⌊log₂ card fd ⌋
 ```
 
+**Proved — Bennett zero-cost on an _arbitrary_ carrier, past
+Bishop-finite (`EchoThermodynamicsArbitrary`).** The finiteness in the
+two results above is an artefact of routing cost through
+`FiberSize-fin` (an enumeration); the *physical content* of Bennett —
+a reversible map has no fan-in — needs no finiteness at all. An
+injective `f : A → B` has a subsingleton fiber for *any* `A : Set a`.
+Keying the Bennett cost on a decidable-inhabitation occupancy instead
+of an enumeration discharges this with no finiteness hypothesis,
+`--safe --without-K`, zero postulates:
+
+```agda
+FiberSubsingleton f y = (p q : Echo f y) → proj₁ p ≡ proj₁ q  -- K-free
+
+injective⇒fiber-subsingleton :                                -- any A
+  (inj : ∀ {x x′} → f x ≡ f x′ → x ≡ x′) → FiberSubsingleton f y
+
+bennett-reversible-arbitrary :        -- A : Set a arbitrary; no Fin, no ≃
+  (inj : ∀ {x x′ : A} → f x ≡ f x′ → x ≡ x′)
+  (d : Dec (Echo f y)) (T : Temperature) →
+  reversible-erasure-cost f y d T ≡ 0
+```
+
+This is **not** a vacuous re-definition: `occupancy≡FiberSize-fin`
+proves the occupancy *coincides with* the established honest count
+`FiberSize-fin` on every finite restriction under the subsingleton
+hypothesis, and `bennett-arbitrary-refines-finite` shows it strictly
+subsumes the `Fin n` result of PR #58. The `--without-K` reason
+for the first-projection form (not full fiber `isProp`) is recorded in
+the module header: full `isProp` needs `B` an h-set / UIP, unavailable
+under `--without-K`; the projection form is K-free provable from
+injectivity and is exactly what the count needs.
+
+**The real CNO theorem, on the infinite carrier.** `cno-identity :
+Program → Program` (the absolute-zero `Program = List Instruction`
+carrier — *infinite*, the very `ProgramState`-flavoured type the
+original companion remarks disclaimed) is injective, so
+`bennett-reversible-cno-identity` gives erasure cost `≡ 0` at every
+fiber and temperature. "A CNO dissipates zero Landauer energy" is now
+a *real* theorem for the identity/injective CNO over the genuine
+infinite carrier — no longer the vacuous claim the deleted
+`ECHO-CNO-BRIDGE-SUMMARY.md` made.
+
 ### Open obligation O-THERMO-∞ (precise, falsifiable — not softened)
 
+NOTE: O-THERMO-∞ is **unchanged and not discharged** by the
+arbitrary-carrier result above. The Bennett *zero-cost* direction no
+longer needs finiteness; O-THERMO-∞ is now sharpened to be
+specifically about the *quantitative* `fiber-erasure-bound` /
+`landauer-collapse` functional — the **count/collapse** direction —
+on an infinite carrier. That is a strictly different functional from
+the occupancy-keyed Bennett cost (occupancy is capped at 1; the
+collapse cost grows as `⌊log₂ N⌋` with the fiber count). Nothing below
+is softened to "future work".
+
 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:
+`A ≃ Fin n`), for the **quantitative collapse functional**, 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`
@@ -332,11 +385,16 @@ sharply enough to be refuted:
    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.
+   injective map (`bennett-reversible-injective`), lifted to any
+   Bishop-finite carrier (`bennett-reversible-finite`), and now to an
+   *arbitrary* carrier with no finiteness at all
+   (`bennett-reversible-arbitrary`), including the genuine infinite
+   `Program` CNO (`bennett-reversible-cno-identity`).
+   `bennett-reversible-id-zero` is a corollary. The remaining
+   falsifiable obligation O-THERMO-∞ above is now specifically the
+   *quantitative collapse* functional on an infinite carrier —
+   `[OPEN]`, with a stated kill condition; the Bennett zero direction
+   is closed for all carriers.
 3. **Information Theory**: not bridged. Open work — see
    `docs/echo-types/roadmap.md`.
 

docs/STABILITY_ANALYSIS.md

@@ -79,24 +79,35 @@ Echo {A = A} f y = Σ A (λ x → f x ≡ y)
 **Stability:** New but well-grounded in existing echo type theory
 
 #### 3.3 Thermodynamic Models: B- (was C+; advanced 2026-05-18)
-**Proofs:** `EchoThermodynamics.agda`, `EchoFiberCount.agda`, `EchoThermodynamicsFinite.agda`
+**Proofs:** `EchoThermodynamics.agda`, `EchoFiberCount.agda`, `EchoThermodynamicsFinite.agda`, `EchoThermodynamicsArbitrary.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
+- Bennett zero-cost lifted further to an **arbitrary carrier — no finiteness
+  at all** (`bennett-reversible-arbitrary`, occupancy-keyed; K-free
+  subsingleton route), certified faithful vs. the established count
+  (`occupancy≡FiberSize-fin`, `bennett-arbitrary-refines-finite`), and
+  instantiated on the genuine **infinite** absolute-zero `Program` CNO
+  (`bennett-reversible-cno-identity`) — the historically vacuous
+  "CNO dissipates zero energy" is now a real theorem
 - 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.
+proved zero-cost instance was the identity at index zero. That gap is fully
+closed: the Bennett zero-cost direction now holds for every injective map on
+**every carrier** — Bishop-finite *and* arbitrary/infinite, including the
+genuine infinite `Program` CNO. The *single* remaining open item is narrower
+than before: it is now specifically the **quantitative collapse functional**
+(`fiber-erasure-bound` / `landauer-collapse`) on an infinite carrier — 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. Grade
+held at **B-** per the standing rule (no re-rate above B- until O-THERMO-∞ is
+discharged or refuted), though scope of the residual has materially shrunk.
 
 ### 4. Proof Ecosystem Stability: B+
 
@@ -111,7 +122,7 @@ development" — one named obligation, refutable by exhibiting a total
 | Relational | 80% | B |
 | CNO Integration | 98% | A- |
 | JanusKey Bridge | 90% | B+ |
-| Thermodynamics | 85% | B- |
+| Thermodynamics | 90% | B- |
 
 **Proof Quality Indicators:**
 - ✅ All core theorems have constructive proofs

docs/echo-types/MAP.adoc

@@ -55,16 +55,23 @@ remainder of information-losing computation: for `f : A → B`,
 === Thermodynamic — Landauer/Bennett energy bounds `[REAL*]`
 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.
+injective map* on *any Bishop-finite carrier*, and now lifted to an
+*arbitrary carrier with no finiteness at all* (K-free subsingleton /
+occupancy route), certified faithful against the established count and
+instantiated on the genuine *infinite* absolute-zero `Program` CNO —
+so "a CNO dissipates zero Landauer energy" is now a real theorem, not
+the historically vacuous claim. The residual is narrower: only the
+*quantitative collapse* functional on an infinite carrier, pinned as
+the falsifiable obligation **O-THERMO-∞** (kill condition stated,
+unchanged, *not* discharged by the arbitrary-carrier Bennett result).
+Re-rated B- / ~90% in STABILITY_ANALYSIS §3.3 (was C+ / ~70%,
+2026-05-18). Stays `[REAL*]` — real, still partial — grade held at B-
+per the standing rule until O-THERMO-∞ is discharged or refuted.
 
 * Proofs: `proofs/agda/EchoThermodynamics.agda`,
   `proofs/agda/EchoFiberCount.agda`,
-  `proofs/agda/EchoThermodynamicsFinite.agda`.
+  `proofs/agda/EchoThermodynamicsFinite.agda`,
+  `proofs/agda/EchoThermodynamicsArbitrary.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

@@ -29,6 +29,7 @@ open import Dyadic
 open import DyadicEchoBridge
 open import EchoThermodynamics
 open import EchoThermodynamicsFinite
+open import EchoThermodynamicsArbitrary
 open import EchoStabilityTests
 open import VecRotation
 

proofs/agda/EchoFiberCount.agda

@@ -174,6 +174,42 @@ FiberSize-fin-injective {n = ℕ.suc m} f y _≟_ inj (suc i′) hit
 ... | no  _  = FiberSize-fin-injective (f ∘ suc) y _≟_
                  (λ eq → Fin-suc-inj (inj eq)) i′ hit
 
+----------------------------------------------------------------------
+-- Headline 2c — FiberSize-fin-subsingleton
+--
+-- The fiber-local hypothesis behind the arbitrary-carrier Bennett
+-- result. If the fiber over `y` is a *subsingleton* — any two hitting
+-- indices coincide — and *some* index `i₀` hits, then the count is
+-- exactly 1. This is strictly weaker as a hypothesis than global
+-- injectivity: it only constrains the indices over `y`. Indeed
+-- `FiberSize-fin-injective` is the corollary obtained by feeding
+-- `ss i j fi fj = inj (trans fi (sym fj))` (kept as-is upstream for
+-- pin stability; this lemma is the honest generalisation).
+--
+-- The proof walks the `FiberSize-fin` recursion in lock-step with the
+-- witness exactly as the injective version does, but discharges the
+-- "no other hit" obligation from subsingleton-ness rather than from
+-- injectivity.
+----------------------------------------------------------------------
+
+FiberSize-fin-subsingleton :
+  ∀ {b} {B : Set b} {n : ℕ}
+  (f : Fin n → B) (y : B) (_≟_ : (y₁ y₂ : B) → Dec (y₁ ≡ y₂))
+  (ss : (i j : Fin n) → f i ≡ y → f j ≡ y → i ≡ j)
+  (i₀ : Fin n) → f i₀ ≡ y →
+  FiberSize-fin f y _≟_ ≡ ℕ.suc ℕ.zero
+FiberSize-fin-subsingleton {n = ℕ.suc m} f y _≟_ ss zero hit
+  with f zero ≟ y
+... | yes _  = cong ℕ.suc
+                 (FiberSize-fin-no-hit (f ∘ suc) y _≟_
+                   (λ j fsj≡y → suc≢zero-Fin j (ss (suc j) zero fsj≡y hit)))
+... | no ¬p  = ⊥-elim (¬p hit)
+FiberSize-fin-subsingleton {n = ℕ.suc m} f y _≟_ ss (suc i′) hit
+  with f zero ≟ y
+... | yes p  = ⊥-elim (suc≢zero-Fin i′ (sym (ss zero (suc i′) p hit)))
+... | no  _  = FiberSize-fin-subsingleton (f ∘ suc) y _≟_
+                 (λ i j fi fj → Fin-suc-inj (ss (suc i) (suc j) fi fj)) i′ hit
+
 ----------------------------------------------------------------------
 -- Headline 3 — FiberSize-fin ≡ 0 ⟺ ¬ Echo (split into two halves).
 --