|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | + |
| 3 | +-- EchoFiberCount: honest finite-domain fiber counting. |
| 4 | +-- |
| 5 | +-- Companion to EchoDecidable. Where EchoDecidable answers |
| 6 | +-- "does an echo exist?" (axis-8 decidability), this module |
| 7 | +-- answers "how many?" — but only in the regime where the |
| 8 | +-- question has a constructive answer: a finite domain `Fin n` |
| 9 | +-- with decidable equality on the codomain. |
| 10 | +-- |
| 11 | +-- The headline value `FiberSize-fin f y _≟_` counts the |
| 12 | +-- preimages of `y : B` under `f : Fin n → B`, computed by |
| 13 | +-- enumerating `Fin n` and asking the decidable equality at |
| 14 | +-- each index. This replaces the earlier |
| 15 | +-- `EchoThermodynamics.FiberSize = 1` hardcode (which rendered |
| 16 | +-- every Landauer/Bennett claim vacuous): with an actual count |
| 17 | +-- in hand we can state honest finite-domain bounds. |
| 18 | +-- |
| 19 | +-- Headline lemmas (pinned in Smoke.agda): |
| 20 | +-- |
| 21 | +-- * FiberSize-fin-id-zero -- id : Fin (suc m) → Fin (suc m) has fiber 1 at zero |
| 22 | +-- * FiberSize-fin-const -- (λ _ → y₀) has fiber n at y₀ |
| 23 | +-- * FiberSize-fin≡0⇒no-echo -- count 0 ⇒ no echo witness |
| 24 | +-- * no-echo⇒FiberSize-fin≡0 -- no echo witness ⇒ count 0 |
| 25 | +-- |
| 26 | +-- The id-zero lemma is the single instance the |
| 27 | +-- `bennett-reversible` corollary in `EchoThermodynamics` |
| 28 | +-- runs on; the const lemma is the worst-case input for |
| 29 | +-- `landauer-collapse`; the bidirectional ≡0/¬Echo lemmas |
| 30 | +-- pin the count to the metatheoretic structure of `Echo`. |
| 31 | + |
| 32 | +module EchoFiberCount where |
| 33 | + |
| 34 | +open import Function.Base using (_∘_) |
| 35 | +open import Data.Empty using (⊥; ⊥-elim) |
| 36 | +import Data.Nat.Base as ℕ |
| 37 | +open ℕ using (ℕ) |
| 38 | +open import Data.Fin.Base using (Fin; zero; suc) |
| 39 | +open import Data.Product.Base using (Σ; _,_) |
| 40 | +open import Relation.Nullary using (¬_) |
| 41 | +open import Relation.Nullary.Decidable.Core using (Dec; yes; no) |
| 42 | +open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong) |
| 43 | + |
| 44 | +open import Echo using (Echo) |
| 45 | + |
| 46 | +---------------------------------------------------------------------- |
| 47 | +-- The fiber count |
| 48 | +---------------------------------------------------------------------- |
| 49 | + |
| 50 | +-- Counts the preimages of `y` under `f : Fin n → B` by enumerating |
| 51 | +-- the domain and asking the decidable equality at each index. Total |
| 52 | +-- and terminating: each recursion call shrinks the implicit `n`. |
| 53 | + |
| 54 | +FiberSize-fin : |
| 55 | + ∀ {b} {B : Set b} {n : ℕ} |
| 56 | + (f : Fin n → B) (y : B) → |
| 57 | + ((y₁ y₂ : B) → Dec (y₁ ≡ y₂)) → |
| 58 | + ℕ |
| 59 | +FiberSize-fin {n = ℕ.zero} f y _≟_ = ℕ.zero |
| 60 | +FiberSize-fin {n = ℕ.suc m} f y _≟_ with f zero ≟ y |
| 61 | +... | yes _ = ℕ.suc (FiberSize-fin (f ∘ suc) y _≟_) |
| 62 | +... | no _ = FiberSize-fin (f ∘ suc) y _≟_ |
| 63 | + |
| 64 | +---------------------------------------------------------------------- |
| 65 | +-- Auxiliary "all-hit" / "no-hit" lemmas |
| 66 | +---------------------------------------------------------------------- |
| 67 | + |
| 68 | +private |
| 69 | + suc≢0 : ∀ {k} → ℕ.suc k ≡ ℕ.zero → ⊥ |
| 70 | + suc≢0 () |
| 71 | + |
| 72 | + suc≢zero-Fin : ∀ {n} (i : Fin n) → ¬ (suc i ≡ zero) |
| 73 | + suc≢zero-Fin _ () |
| 74 | + |
| 75 | +---------------------------------------------------------------------- |
| 76 | +-- "no-hit" / "all-hit" lemmas (exposed for downstream use). |
| 77 | +-- |
| 78 | +-- These are the two extremal shapes of the count: the count is |
| 79 | +-- zero exactly when no index hits, and the count is `n` exactly |
| 80 | +-- when every index hits. Both proofs walk the FiberSize-fin |
| 81 | +-- recursion in lock-step with a hypothesis on f. |
| 82 | +---------------------------------------------------------------------- |
| 83 | + |
| 84 | +-- If f never hits y, the count is 0. |
| 85 | +FiberSize-fin-no-hit : |
| 86 | + ∀ {b} {B : Set b} {n : ℕ} |
| 87 | + (f : Fin n → B) (y : B) (_≟_ : (y₁ y₂ : B) → Dec (y₁ ≡ y₂)) → |
| 88 | + (∀ i → ¬ (f i ≡ y)) → |
| 89 | + FiberSize-fin f y _≟_ ≡ ℕ.zero |
| 90 | +FiberSize-fin-no-hit {n = ℕ.zero} f y _≟_ h = refl |
| 91 | +FiberSize-fin-no-hit {n = ℕ.suc m} f y _≟_ h with f zero ≟ y |
| 92 | +... | yes p = ⊥-elim (h zero p) |
| 93 | +... | no _ = FiberSize-fin-no-hit (f ∘ suc) y _≟_ (λ i → h (suc i)) |
| 94 | + |
| 95 | +-- If f hits y everywhere, the count is n. |
| 96 | +FiberSize-fin-all-hit : |
| 97 | + ∀ {b} {B : Set b} {n : ℕ} |
| 98 | + (f : Fin n → B) (y : B) (_≟_ : (y₁ y₂ : B) → Dec (y₁ ≡ y₂)) → |
| 99 | + (∀ i → f i ≡ y) → |
| 100 | + FiberSize-fin f y _≟_ ≡ n |
| 101 | +FiberSize-fin-all-hit {n = ℕ.zero} f y _≟_ h = refl |
| 102 | +FiberSize-fin-all-hit {n = ℕ.suc m} f y _≟_ h with f zero ≟ y |
| 103 | +... | yes _ = cong ℕ.suc (FiberSize-fin-all-hit (f ∘ suc) y _≟_ (λ i → h (suc i))) |
| 104 | +... | no ¬p = ⊥-elim (¬p (h zero)) |
| 105 | + |
| 106 | +---------------------------------------------------------------------- |
| 107 | +-- Headline 1 — FiberSize-fin-id-zero |
| 108 | +-- |
| 109 | +-- The identity `id : Fin (suc m) → Fin (suc m)` has fiber size 1 |
| 110 | +-- at the zero index. Specific instance of "any injection has |
| 111 | +-- singleton fibers everywhere"; the `bennett-reversible` corollary |
| 112 | +-- in `EchoThermodynamics` runs on this lemma plus `⌊log₂ 1 ⌋ ≡ 0`. |
| 113 | +---------------------------------------------------------------------- |
| 114 | + |
| 115 | +FiberSize-fin-id-zero : |
| 116 | + ∀ {m : ℕ} (_≟_ : (a b : Fin (ℕ.suc m)) → Dec (a ≡ b)) → |
| 117 | + FiberSize-fin {n = ℕ.suc m} (λ x → x) zero _≟_ ≡ ℕ.suc ℕ.zero |
| 118 | +FiberSize-fin-id-zero {m} _≟_ with (zero {m}) ≟ (zero {m}) |
| 119 | +... | yes refl = cong ℕ.suc (FiberSize-fin-no-hit (λ x → suc x) zero _≟_ suc≢zero-Fin) |
| 120 | +... | no ¬p = ⊥-elim (¬p refl) |
| 121 | + |
| 122 | +---------------------------------------------------------------------- |
| 123 | +-- Headline 2 — FiberSize-fin-const |
| 124 | +-- |
| 125 | +-- The constant function `(λ _ → y₀) : Fin n → B` has fiber size n |
| 126 | +-- at `y₀`: every domain index hits, so the count equals the domain |
| 127 | +-- size. This is the worst-case input for the Landauer bound — every |
| 128 | +-- Fin-index is collapsed onto a single output value. |
| 129 | +---------------------------------------------------------------------- |
| 130 | + |
| 131 | +FiberSize-fin-const : |
| 132 | + ∀ {b} {B : Set b} {n : ℕ} |
| 133 | + (y₀ : B) (_≟_ : (y₁ y₂ : B) → Dec (y₁ ≡ y₂)) → |
| 134 | + FiberSize-fin {n = n} (λ _ → y₀) y₀ _≟_ ≡ n |
| 135 | +FiberSize-fin-const y₀ _≟_ = FiberSize-fin-all-hit (λ _ → y₀) y₀ _≟_ (λ _ → refl) |
| 136 | + |
| 137 | +---------------------------------------------------------------------- |
| 138 | +-- Headline 3 — FiberSize-fin ≡ 0 ⟺ ¬ Echo (split into two halves). |
| 139 | +-- |
| 140 | +-- The constructive count zero is exactly the constructive absence |
| 141 | +-- of an echo. Pins `FiberSize-fin` to the metatheoretic structure |
| 142 | +-- of `Echo` from `Echo.agda`: count zero is the *only* numerical |
| 143 | +-- shape consistent with there being no witness. |
| 144 | +---------------------------------------------------------------------- |
| 145 | + |
| 146 | +FiberSize-fin≡0⇒no-echo : |
| 147 | + ∀ {b} {B : Set b} {n : ℕ} |
| 148 | + (f : Fin n → B) (y : B) (_≟_ : (y₁ y₂ : B) → Dec (y₁ ≡ y₂)) → |
| 149 | + FiberSize-fin f y _≟_ ≡ ℕ.zero → |
| 150 | + ¬ Echo f y |
| 151 | +FiberSize-fin≡0⇒no-echo {n = ℕ.zero} f y _≟_ p (() , _) |
| 152 | +FiberSize-fin≡0⇒no-echo {n = ℕ.suc m} f y _≟_ p (zero , q) with f zero ≟ y |
| 153 | +... | yes _ = ⊥-elim (suc≢0 p) |
| 154 | +... | no ¬q = ¬q q |
| 155 | +FiberSize-fin≡0⇒no-echo {n = ℕ.suc m} f y _≟_ p (suc i , q) with f zero ≟ y |
| 156 | +... | yes _ = ⊥-elim (suc≢0 p) |
| 157 | +... | no _ = FiberSize-fin≡0⇒no-echo (f ∘ suc) y _≟_ p (i , q) |
| 158 | + |
| 159 | +no-echo⇒FiberSize-fin≡0 : |
| 160 | + ∀ {b} {B : Set b} {n : ℕ} |
| 161 | + (f : Fin n → B) (y : B) (_≟_ : (y₁ y₂ : B) → Dec (y₁ ≡ y₂)) → |
| 162 | + ¬ Echo f y → |
| 163 | + FiberSize-fin f y _≟_ ≡ ℕ.zero |
| 164 | +no-echo⇒FiberSize-fin≡0 {n = ℕ.zero} f y _≟_ ¬e = refl |
| 165 | +no-echo⇒FiberSize-fin≡0 {n = ℕ.suc m} f y _≟_ ¬e with f zero ≟ y |
| 166 | +... | yes p = ⊥-elim (¬e (zero , p)) |
| 167 | +... | no _ = no-echo⇒FiberSize-fin≡0 (f ∘ suc) y _≟_ (λ { (i , q) → ¬e (suc i , q) }) |
| 168 | + |
| 169 | +---------------------------------------------------------------------- |
| 170 | +-- Companion remark. |
| 171 | +-- |
| 172 | +-- This module deliberately stays at the finite-domain `Fin n` level. |
| 173 | +-- The infinite-domain case (e.g. `ProgramState = ℕ → ℕ`) is *not* |
| 174 | +-- addressed: counting fibers of a function on an infinite type is |
| 175 | +-- not constructively meaningful in general. EchoThermodynamics's |
| 176 | +-- claims about CNOs over infinite state spaces are out of reach |
| 177 | +-- without a heavier semantic framework (capacity, measure, or |
| 178 | +-- equivalence-class quotients), and that limitation is now made |
| 179 | +-- explicit in `docs/ECHO-CNO-BRIDGE.adoc`. |
0 commit comments