hyperpolymath
diff --git a/‎docs/ECHO-CNO-BRIDGE.adoc‎
Lines changed: 93 additions & 37 deletions b/‎docs/ECHO-CNO-BRIDGE.adoc‎
Lines changed: 93 additions & 37 deletions
diff --git a/‎docs/echo-types/taxonomy.md‎
Lines changed: 23 additions & 9 deletions b/‎docs/echo-types/taxonomy.md‎
Lines changed: 23 additions & 9 deletions
diff --git a/‎proofs/agda/All.agda‎
Lines changed: 1 addition & 0 deletions b/‎proofs/agda/All.agda‎
Lines changed: 1 addition & 0 deletions
diff --git a/‎proofs/agda/EchoFiberCount.agda‎
Lines changed: 179 additions & 0 deletions b/‎proofs/agda/EchoFiberCount.agda‎
Lines changed: 179 additions & 0 deletions
@@ -65,23 +65,45 @@ cno-composition-echo : ∀ (s : ProgramState) (e : Echo cno-identity s) →
 
 **Proof**: Composing identity functions preserves echo structure.
 
-### Theorem 4: CNO Thermodynamic Optimality (NEW)
+### Theorem 4: Bennett-reversible erasure cost (FINITE DOMAIN ONLY)
 
 ```agda
-cno-thermodynamic-optimality : ∀ (s : ProgramState) (T : Temperature) → 
-                               fiber-energy cno-identity s T ≡ zero
+-- in EchoThermodynamics
+bennett-reversible :
+  (f : Fin n → B) (y : B) (_≟_ : DecidableEquality B) (T : Temperature) →
+  FiberSize-fin f y _≟_ ≡ 1 →
+  fiber-erasure-bound f y _≟_ T ≡ 0
 ```
 
-**Proof**: CNOs dissipate zero energy according to Landauer's principle.
-
-### Theorem 5: CNO Information Preservation
-
-```agda
-cno-information-preservation : ∀ (s : ProgramState) → 
-                               echo-information-loss cno-identity s ≡ zero
-```
-
-**Proof**: CNOs preserve all information (zero information loss).
+**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.
+
+### Theorem 5: Information-preservation (NOT YET FORMALISED)
+
+The earlier `cno-information-preservation` headline referenced a
+function `echo-information-loss` that was never defined and a
+notion of CNO-information that has no formal analogue in the
+current Agda corpus. **No theorem of this form exists in the
+proven suite.** The closest formalised statement is the qualitative
+`FiberSize-fin ≡ 0 ⟺ ¬ Echo` bidirectional in `EchoFiberCount` —
+the count is zero exactly when no metatheoretic witness exists —
+but that is a witness-presence statement, not an
+information-preservation statement.
+
+A real Shannon-entropy / mutual-information formalisation is open
+work; see `docs/echo-types/roadmap.md` under the thermodynamic
+items.
 
 ### Theorem 6: Universal CNO Definition (NEW)
 
@@ -118,8 +140,8 @@ 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-energy p σ T ≡ zero` |
-| `InformationPreservation(p)` | `echo-information-loss p σ ≡ zero` |
+| `ThermodynamicOptimality(p)` | `fiber-erasure-bound p σ _≟_ T ≡ 0` _(proved at finite-domain `Fin n → B` only — see Theorem 4)_ |
+| `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) |
 
@@ -164,39 +186,73 @@ ModelIndependence : ∀ {A B A' B' : Ob} (f : A → B) (f' : A' → B')
 3. **Category Theory Module**: Formalizes echo types as fibrations
 4. **Functorial Properties**: Proves echo maps preserve categorical structure
 
-## Thermodynamic Bridge
+## Thermodynamic Bridge — finite-domain Landauer/Bennett bounds
 
-The `EchoThermodynamics.agda` module establishes a critical connection between echo types and Landauer's principle, directly supporting Absolute Zero's thermodynamic formalization goals.
+The `EchoFiberCount.agda` + `EchoThermodynamics.agda` pair
+formalises the *shape* of Landauer's bound at the finite-domain
+`Fin n → B` level. The earlier draft of this section claimed
+significantly more than was proved (a `FiberSize ≡ 1` hardcode
+made `cno-zero-energy` and `cno-zero-information-loss` vacuous);
+those claims have been retracted and replaced with what is
+actually in the proven suite.
 
 ### Key Concepts
 
-1. **Fiber Energy**: `fiber-energy f y T = landauer-energy T * fiber-size f y`
-2. **Information Loss**: `echo-information-loss f x = fiber-size f (f x) - 1`
-3. **CNO Optimality**: CNOs minimize energy dissipation
+1. **Honest fiber count**:
+   `FiberSize-fin f y _≟_` enumerates `Fin n` and asks the
+   decidable equality at each index — actual preimage count, not
+   a hardcoded constant.
+2. **Landauer bound shape**:
+   `landauer-bound T n = k * T * ⌊log₂ n⌋`. Linear in T,
+   logarithmic in the alternatives count. `⌊log₂ 0⌋ = ⌊log₂ 1⌋ = 0`
+   discharges the trivial corners.
+3. **Fiber erasure bound**:
+   `fiber-erasure-bound f y _≟_ T = landauer-bound T (FiberSize-fin f y _≟_)`.
 
-### Core Theorems
+### Core Theorems (proved, finite domain only)
 
 ```agda
--- CNOs dissipate zero energy
-cno-zero-energy : ∀ (s : ProgramState) (T : Temperature) → 
-                  fiber-energy cno-identity s T ≡ zero
-
--- CNOs preserve all information
-cno-zero-information-loss : ∀ (s : ProgramState) → 
-                           echo-information-loss cno-identity s ≡ zero
-
--- Thermodynamic verification
-thermodynamic-cno-verification : ∀ (p : ProgramState → ProgramState) → 
-                                 (∀ σ → fiber-energy p σ T ≡ zero) → 
-                                 (∀ σ → cno-zero-energy σ T)
+-- Bennett: if the fiber size at y is 1, the erasure bound is 0
+bennett-reversible :
+  (f : Fin n → B) (y : B) (_≟_ : DecidableEquality B) (T : Temperature) →
+  FiberSize-fin f y _≟_ ≡ 1 →
+  fiber-erasure-bound f y _≟_ T ≡ 0
+
+-- Identity at index zero — canonical instance
+bennett-reversible-id-zero :
+  (_≟_ : DecidableEquality (Fin (suc m))) (T : Temperature) →
+  fiber-erasure-bound (λ x → x) zero _≟_ T ≡ 0
+
+-- Landauer worst case: every input maps to the same y
+landauer-collapse :
+  (f : Fin n → B) (y : B) (_≟_ : DecidableEquality B) (T : Temperature) →
+  (∀ x → f x ≡ y) →
+  fiber-erasure-bound f y _≟_ T ≡ k * T * ⌊log₂ n⌋
 ```
 
+### What is NOT proved
+
+* `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.
+* `cno-energy-hierarchy`, `thermodynamic-cno-verification` —
+  no proven analogue exists.
+
 ### Connection to Absolute Zero Goals
 
-1. **Landauer's Principle**: Formalized via `fiber-energy` and `landauer-energy`
-2. **Thermodynamic Reversibility**: Proven via `cno-zero-energy`
-3. **Energy Hierarchy**: Established via `cno-energy-hierarchy`
-4. **Information Theory**: Bridged via `echo-information-loss`
+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
+   `docs/echo-types/roadmap.md`.
 
 ## Practical Implications
 
 
@@ -210,15 +210,29 @@ intensional core, same proof relevance, etc.) and differ only in
 whether a witness is reachable by a feasible algorithm. The security
 of every modern cryptosystem depends on this axis being real.
 
-*Agda anchor.* `EchoDecidable.agda` formalises refinement 3 below
-(decidability-respecting echo) as the first axis-8 artifact under
-`--safe --without-K`. Full cost-tracking refinements (1, 2, 4) are
-not yet formalised — Agda's type system does not express complexity
-bounds, so asymptotic computational access cannot be named at the
-type level without further machinery. Adjacent stdlib pieces:
-- `Data.Nat.Logarithm.⌊log₂⌋` and arithmetic complexity conventions
-  admit informal-level statements like "this function runs in `O(n
-  log n)`", but without a cost monad.
+*Agda anchor.* Two artifacts now live at this axis:
+- `EchoDecidable.agda` formalises refinement 3 below
+  (decidability-respecting echo) as the first axis-8 artifact under
+  `--safe --without-K` — the *qualitative* "yes / no" layer.
+- `EchoFiberCount.agda` (companion) provides the *quantitative*
+  layer for the finite-domain regime: `FiberSize-fin f y _≟_ : ℕ`
+  enumerates `Fin n` and asks the decidable equality at each
+  index, returning the actual preimage count. Headlines:
+  `FiberSize-fin-id-zero` (id has fiber 1), `FiberSize-fin-const`
+  (constant collapse: fiber n), and the bidirectional
+  `FiberSize-fin ≡ 0 ⟺ ¬ Echo`. This is the count
+  `EchoThermodynamics.fiber-erasure-bound` runs on, replacing the
+  earlier `FiberSize ≡ 1` hardcode that rendered all
+  Landauer/Bennett claims vacuous.
+
+Full cost-tracking refinements (1, 2, 4) remain unformalised —
+Agda's type system does not express complexity bounds, so
+asymptotic computational access cannot be named at the type level
+without further machinery. Adjacent stdlib pieces:
+- `Data.Nat.Logarithm.⌊log₂⌋` (now imported by
+  `EchoThermodynamics`) and arithmetic complexity conventions admit
+  informal-level statements like "this function runs in `O(n log n)`",
+  but without a cost monad.
 - `EchoLinear.agda` and `EchoGraded.agda` restrict what one can *do*
   with witnesses via usage modes and grades. These are proxies for
   resource control, not full computational-access tracking.
 
@@ -18,6 +18,7 @@ open import EchoCNOBridge
 open import EchoApprox
 open import EchoIndexed
 open import EchoDecidable
+open import EchoFiberCount
 open import EchoEpistemicResidue
 open import EchoRelational
 open import EchoCategorical
 
@@ -0,0 +1,179 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- EchoFiberCount: honest finite-domain fiber counting.
+--
+-- Companion to EchoDecidable. Where EchoDecidable answers
+-- "does an echo exist?" (axis-8 decidability), this module
+-- answers "how many?" — but only in the regime where the
+-- question has a constructive answer: a finite domain `Fin n`
+-- with decidable equality on the codomain.
+--
+-- The headline value `FiberSize-fin f y _≟_` counts the
+-- preimages of `y : B` under `f : Fin n → B`, computed by
+-- enumerating `Fin n` and asking the decidable equality at
+-- each index. This replaces the earlier
+-- `EchoThermodynamics.FiberSize = 1` hardcode (which rendered
+-- every Landauer/Bennett claim vacuous): with an actual count
+-- in hand we can state honest finite-domain bounds.
+--
+-- Headline lemmas (pinned in Smoke.agda):
+--
+--   * FiberSize-fin-id-zero       -- id : Fin (suc m) → Fin (suc m) has fiber 1 at zero
+--   * FiberSize-fin-const         -- (λ _ → y₀) has fiber n at y₀
+--   * FiberSize-fin≡0⇒no-echo     -- count 0 ⇒ no echo witness
+--   * no-echo⇒FiberSize-fin≡0     -- no echo witness ⇒ count 0
+--
+-- The id-zero lemma is the single instance the
+-- `bennett-reversible` corollary in `EchoThermodynamics`
+-- runs on; the const lemma is the worst-case input for
+-- `landauer-collapse`; the bidirectional ≡0/¬Echo lemmas
+-- pin the count to the metatheoretic structure of `Echo`.
+
+module EchoFiberCount where
+
+open import Function.Base                         using (_∘_)
+open import Data.Empty                            using (⊥; ⊥-elim)
+import      Data.Nat.Base                         as ℕ
+open        ℕ                                     using (ℕ)
+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 Echo                                  using (Echo)
+
+----------------------------------------------------------------------
+-- The fiber count
+----------------------------------------------------------------------
+
+-- Counts the preimages of `y` under `f : Fin n → B` by enumerating
+-- the domain and asking the decidable equality at each index. Total
+-- and terminating: each recursion call shrinks the implicit `n`.
+
+FiberSize-fin :
+  ∀ {b} {B : Set b} {n : ℕ}
+  (f : Fin n → B) (y : B) →
+  ((y₁ y₂ : B) → Dec (y₁ ≡ y₂)) →
+  ℕ
+FiberSize-fin {n = ℕ.zero}  f y _≟_ = ℕ.zero
+FiberSize-fin {n = ℕ.suc m} f y _≟_ with f zero ≟ y
+... | yes _ = ℕ.suc (FiberSize-fin (f ∘ suc) y _≟_)
+... | no  _ = FiberSize-fin (f ∘ suc) y _≟_
+
+----------------------------------------------------------------------
+-- Auxiliary "all-hit" / "no-hit" lemmas
+----------------------------------------------------------------------
+
+private
+  suc≢0 : ∀ {k} → ℕ.suc k ≡ ℕ.zero → ⊥
+  suc≢0 ()
+
+  suc≢zero-Fin : ∀ {n} (i : Fin n) → ¬ (suc i ≡ zero)
+  suc≢zero-Fin _ ()
+
+----------------------------------------------------------------------
+-- "no-hit" / "all-hit" lemmas (exposed for downstream use).
+--
+-- These are the two extremal shapes of the count: the count is
+-- zero exactly when no index hits, and the count is `n` exactly
+-- when every index hits. Both proofs walk the FiberSize-fin
+-- recursion in lock-step with a hypothesis on f.
+----------------------------------------------------------------------
+
+-- If f never hits y, the count is 0.
+FiberSize-fin-no-hit :
+  ∀ {b} {B : Set b} {n : ℕ}
+  (f : Fin n → B) (y : B) (_≟_ : (y₁ y₂ : B) → Dec (y₁ ≡ y₂)) →
+  (∀ i → ¬ (f i ≡ y)) →
+  FiberSize-fin f y _≟_ ≡ ℕ.zero
+FiberSize-fin-no-hit {n = ℕ.zero}  f y _≟_ h = refl
+FiberSize-fin-no-hit {n = ℕ.suc m} f y _≟_ h with f zero ≟ y
+... | yes p = ⊥-elim (h zero p)
+... | no  _ = FiberSize-fin-no-hit (f ∘ suc) y _≟_ (λ i → h (suc i))
+
+-- If f hits y everywhere, the count is n.
+FiberSize-fin-all-hit :
+  ∀ {b} {B : Set b} {n : ℕ}
+  (f : Fin n → B) (y : B) (_≟_ : (y₁ y₂ : B) → Dec (y₁ ≡ y₂)) →
+  (∀ i → f i ≡ y) →
+  FiberSize-fin f y _≟_ ≡ n
+FiberSize-fin-all-hit {n = ℕ.zero}  f y _≟_ h = refl
+FiberSize-fin-all-hit {n = ℕ.suc m} f y _≟_ h with f zero ≟ y
+... | yes _ = cong ℕ.suc (FiberSize-fin-all-hit (f ∘ suc) y _≟_ (λ i → h (suc i)))
+... | no ¬p = ⊥-elim (¬p (h zero))
+
+----------------------------------------------------------------------
+-- Headline 1 — FiberSize-fin-id-zero
+--
+-- The identity `id : Fin (suc m) → Fin (suc m)` has fiber size 1
+-- at the zero index. Specific instance of "any injection has
+-- singleton fibers everywhere"; the `bennett-reversible` corollary
+-- in `EchoThermodynamics` runs on this lemma plus `⌊log₂ 1 ⌋ ≡ 0`.
+----------------------------------------------------------------------
+
+FiberSize-fin-id-zero :
+  ∀ {m : ℕ} (_≟_ : (a b : Fin (ℕ.suc m)) → Dec (a ≡ b)) →
+  FiberSize-fin {n = ℕ.suc m} (λ x → x) zero _≟_ ≡ ℕ.suc ℕ.zero
+FiberSize-fin-id-zero {m} _≟_ with (zero {m}) ≟ (zero {m})
+... | yes refl = cong ℕ.suc (FiberSize-fin-no-hit (λ x → suc x) zero _≟_ suc≢zero-Fin)
+... | no  ¬p   = ⊥-elim (¬p refl)
+
+----------------------------------------------------------------------
+-- Headline 2 — FiberSize-fin-const
+--
+-- The constant function `(λ _ → y₀) : Fin n → B` has fiber size n
+-- at `y₀`: every domain index hits, so the count equals the domain
+-- size. This is the worst-case input for the Landauer bound — every
+-- Fin-index is collapsed onto a single output value.
+----------------------------------------------------------------------
+
+FiberSize-fin-const :
+  ∀ {b} {B : Set b} {n : ℕ}
+  (y₀ : B) (_≟_ : (y₁ y₂ : B) → Dec (y₁ ≡ y₂)) →
+  FiberSize-fin {n = n} (λ _ → y₀) y₀ _≟_ ≡ n
+FiberSize-fin-const y₀ _≟_ = FiberSize-fin-all-hit (λ _ → y₀) y₀ _≟_ (λ _ → refl)
+
+----------------------------------------------------------------------
+-- Headline 3 — FiberSize-fin ≡ 0 ⟺ ¬ Echo (split into two halves).
+--
+-- The constructive count zero is exactly the constructive absence
+-- of an echo. Pins `FiberSize-fin` to the metatheoretic structure
+-- of `Echo` from `Echo.agda`: count zero is the *only* numerical
+-- shape consistent with there being no witness.
+----------------------------------------------------------------------
+
+FiberSize-fin≡0⇒no-echo :
+  ∀ {b} {B : Set b} {n : ℕ}
+  (f : Fin n → B) (y : B) (_≟_ : (y₁ y₂ : B) → Dec (y₁ ≡ y₂)) →
+  FiberSize-fin f y _≟_ ≡ ℕ.zero →
+  ¬ Echo f y
+FiberSize-fin≡0⇒no-echo {n = ℕ.zero}  f y _≟_ p (() , _)
+FiberSize-fin≡0⇒no-echo {n = ℕ.suc m} f y _≟_ p (zero  , q) with f zero ≟ y
+... | yes _  = ⊥-elim (suc≢0 p)
+... | no  ¬q = ¬q q
+FiberSize-fin≡0⇒no-echo {n = ℕ.suc m} f y _≟_ p (suc i , q) with f zero ≟ y
+... | yes _ = ⊥-elim (suc≢0 p)
+... | no  _ = FiberSize-fin≡0⇒no-echo (f ∘ suc) y _≟_ p (i , q)
+
+no-echo⇒FiberSize-fin≡0 :
+  ∀ {b} {B : Set b} {n : ℕ}
+  (f : Fin n → B) (y : B) (_≟_ : (y₁ y₂ : B) → Dec (y₁ ≡ y₂)) →
+  ¬ Echo f y →
+  FiberSize-fin f y _≟_ ≡ ℕ.zero
+no-echo⇒FiberSize-fin≡0 {n = ℕ.zero}  f y _≟_ ¬e = refl
+no-echo⇒FiberSize-fin≡0 {n = ℕ.suc m} f y _≟_ ¬e with f zero ≟ y
+... | yes p = ⊥-elim (¬e (zero , p))
+... | no  _ = no-echo⇒FiberSize-fin≡0 (f ∘ suc) y _≟_ (λ { (i , q) → ¬e (suc i , q) })
+
+----------------------------------------------------------------------
+-- Companion remark.
+--
+-- This module deliberately stays at the finite-domain `Fin n` level.
+-- The infinite-domain case (e.g. `ProgramState = ℕ → ℕ`) is *not*
+-- addressed: counting fibers of a function on an infinite type is
+-- not constructively meaningful in general. EchoThermodynamics's
+-- claims about CNOs over infinite state spaces are out of reach
+-- without a heavier semantic framework (capacity, measure, or
+-- equivalence-class quotients), and that limitation is now made
+-- explicit in `docs/ECHO-CNO-BRIDGE.adoc`.