diff --git a/docs/ECHO-CNO-BRIDGE.adoc b/docs/ECHO-CNO-BRIDGE.adoc index f1f8bc3..c6b316a 100644 --- a/docs/ECHO-CNO-BRIDGE.adoc +++ b/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 diff --git a/docs/STABILITY_ANALYSIS.md b/docs/STABILITY_ANALYSIS.md index c885546..8fc51f2 100644 --- a/docs/STABILITY_ANALYSIS.md +++ b/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 diff --git a/docs/echo-types/MAP.adoc b/docs/echo-types/MAP.adoc index 5ec0e84..3f06461 100644 --- a/docs/echo-types/MAP.adoc +++ b/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`. diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index 5774dad..970b99b 100644 --- a/proofs/agda/All.agda +++ b/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 diff --git a/proofs/agda/EchoFiberCount.agda b/proofs/agda/EchoFiberCount.agda index 54f323e..6138df1 100644 --- a/proofs/agda/EchoFiberCount.agda +++ b/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). -- diff --git a/proofs/agda/EchoThermodynamics.agda b/proofs/agda/EchoThermodynamics.agda index d7c22f9..c454d11 100644 --- a/proofs/agda/EchoThermodynamics.agda +++ b/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 -- diff --git a/proofs/agda/EchoThermodynamicsFinite.agda b/proofs/agda/EchoThermodynamicsFinite.agda new file mode 100644 index 0000000..d2ae21d --- /dev/null +++ b/proofs/agda/EchoThermodynamicsFinite.agda @@ -0,0 +1,148 @@ +{-# OPTIONS --safe --without-K #-} + +-- EchoThermodynamicsFinite: the Landauer/Bennett bounds, lifted +-- off `Fin n` to *any Bishop-finite carrier*. +-- +-- Motivation. +-- +-- `EchoThermodynamics` proves the bound *shape* only for +-- `f : Fin n → B`, because the cost functional is routed through +-- `EchoFiberCount.FiberSize-fin`, whose totality is structural +-- recursion on the index bound `n` of `Fin n`. The honest question +-- the C+ rating poses is: *how far past `Fin n → B` does this go?* +-- +-- Answer, made precise here: +-- +-- * It generalises, with no new axioms, to **every Bishop-finite +-- carrier** `A` — i.e. any `A` equipped with a bijection +-- `A ≃ Fin n`. The bridge is pure transport: precompose with +-- the bijection's `from : Fin n → A`, and the finite-domain +-- results apply verbatim. This module discharges that case. +-- +-- * It does **not** generalise to an arbitrary infinite carrier +-- (e.g. `ProgramState = ℕ → ℕ`). That residue is a *stated, +-- falsifiable* obligation — O-THERMO-∞ in +-- `docs/ECHO-CNO-BRIDGE.adoc` §"Thermodynamic Bridge" — not a +-- softened "future work" line. It is recorded there, not +-- postulated here: this module introduces zero postulates and +-- no escape pragmas, exactly like the rest of the suite. +-- +-- Headlines (pinned in Smoke.agda): +-- +-- * FiniteDomain -- Bishop-finite carrier record +-- * fiber-erasure-bound-fin -- cost for a finite carrier +-- * bennett-reversible-finite -- injective f on finite A, a hit ⇒ 0 +-- * landauer-collapse-finite -- f collapses onto y ⇒ k·T·⌊log₂ n⌋ + +module EchoThermodynamicsFinite where + +open import Function.Base using (_∘_) +import Data.Nat.Base as ℕ +open ℕ using (ℕ; _*_) +open import Data.Fin.Base using (Fin) +open import Data.Nat.Logarithm using (⌊log₂_⌋) +open import Relation.Nullary.Decidable.Core using (Dec) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; trans) + +open import EchoThermodynamics using + ( Temperature + ; Energy + ; k + ; landauer-bound + ; fiber-erasure-bound + ; bennett-reversible-injective + ; landauer-collapse + ) + +---------------------------------------------------------------------- +-- Bishop-finite carrier +-- +-- `A` is Bishop-finite when it is in explicit bijection with some +-- `Fin n`. We carry both round-trips: `from∘to` transports a +-- domain witness onto `Fin n`, and `to∘from` gives injectivity of +-- `from`. No `--without-K`-unsafe content: these are bare +-- propositional equalities. +---------------------------------------------------------------------- + +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 + +open FiniteDomain public + +---------------------------------------------------------------------- +-- Cost functional for a finite carrier. +-- +-- Defined by precomposition with the bijection's `from`, so it is +-- *definitionally* the `Fin card` cost of `f ∘ from`. That +-- definitional identity is what lets the finite-domain proofs apply +-- verbatim, with no transport lemma on the bound itself. +---------------------------------------------------------------------- + +fiber-erasure-bound-fin : + ∀ {b} {A : Set} {B : Set b} + (fd : FiniteDomain A) (f : A → B) (y : B) → + ((y₁ y₂ : B) → Dec (y₁ ≡ y₂)) → + Temperature → Energy +fiber-erasure-bound-fin fd f y _≟_ T = + fiber-erasure-bound (f ∘ from fd) y _≟_ T + +---------------------------------------------------------------------- +-- bennett-reversible-finite +-- +-- Bennett, off `Fin n`: an injective `f : A → B` on a Bishop-finite +-- carrier `A` that hits `y` at some `a₀` has erasure bound zero at +-- `y`. The two obligations of `bennett-reversible-injective` for +-- `f ∘ from` are discharged by the bijection laws: +-- +-- * injectivity of `f ∘ from` = injectivity of `f` ∘ injectivity +-- of `from`, and `from` is injective because `to ∘ from ≡ id`; +-- * the witness index is `to a₀`, with `from∘to` carrying the +-- hit `f a₀ ≡ y` back along the round-trip. +---------------------------------------------------------------------- + +bennett-reversible-finite : + ∀ {b} {A : Set} {B : Set b} + (fd : FiniteDomain A) (f : A → B) (y : B) + (_≟_ : (y₁ y₂ : B) → Dec (y₁ ≡ y₂)) + (inj : ∀ {a a′ : A} → f a ≡ f a′ → a ≡ a′) + (a₀ : A) → f a₀ ≡ y → + (T : Temperature) → + fiber-erasure-bound-fin fd f y _≟_ T ≡ 0 +bennett-reversible-finite fd f y _≟_ inj a₀ hit T = + bennett-reversible-injective (f ∘ from fd) y _≟_ g-inj (to fd a₀) g-hit T + where + -- `from` is injective: it has a left inverse `to`. + from-inj : ∀ {i j} → from fd i ≡ from fd j → i ≡ j + from-inj {i} {j} e = + trans (sym (to∘from fd i)) (trans (cong (to fd) e) (to∘from fd j)) + + g-inj : ∀ {i j} → (f ∘ from fd) i ≡ (f ∘ from fd) j → i ≡ j + g-inj e = from-inj (inj e) + + g-hit : (f ∘ from fd) (to fd a₀) ≡ y + g-hit = trans (cong f (from∘to fd a₀)) hit + +---------------------------------------------------------------------- +-- landauer-collapse-finite +-- +-- Worst case off `Fin n`: if `f` collapses the whole Bishop-finite +-- carrier onto `y`, the erasure bound is the full Landauer cost +-- `k · T · ⌊log₂ card⌋`. (`card` is the carrier's bijective size; +-- the bijection makes "how many alternatives were erased" a sharp +-- finite number.) +---------------------------------------------------------------------- + +landauer-collapse-finite : + ∀ {b} {A : Set} {B : Set b} + (fd : FiniteDomain A) (f : A → B) (y : B) + (_≟_ : (y₁ y₂ : B) → Dec (y₁ ≡ y₂)) → + (∀ a → f a ≡ y) → + (T : Temperature) → + fiber-erasure-bound-fin fd f y _≟_ T ≡ k * T * ⌊log₂ card fd ⌋ +landauer-collapse-finite fd f y _≟_ h T = + landauer-collapse (f ∘ from fd) y _≟_ T (λ i → h (from fd i)) diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index cc4de29..5aac346 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -73,6 +73,7 @@ open import EchoFiberCount using ; FiberSize-fin-no-hit ; FiberSize-fin-all-hit ; FiberSize-fin-id-zero + ; FiberSize-fin-injective ; FiberSize-fin-const ; FiberSize-fin≡0⇒no-echo ; no-echo⇒FiberSize-fin≡0 @@ -84,9 +85,17 @@ open import EchoThermodynamics using ; ⌊log₂1⌋≡0 ; bennett-reversible ; bennett-reversible-id-zero + ; bennett-reversible-injective ; landauer-collapse ) +open import EchoThermodynamicsFinite using + ( FiniteDomain + ; fiber-erasure-bound-fin + ; bennett-reversible-finite + ; landauer-collapse-finite + ) + open import EchoChoreo using ( Role ; Global