deterministic_has_zero_entropy

formal source

 155
 156/-- **THEOREM IC-001.11**: The deterministic distribution (one outcome certain) has zero entropy.
 157    Perfect knowledge = zero information cost = balanced ledger. -/
 158theorem deterministic_has_zero_entropy {n : ℕ} (d : ShannonEntropy.ProbDist n) (i : Fin n)
 159    (hdet : d.probs i = 1) (hother : ∀ j ≠ i, d.probs j = 0) :
 160    ShannonEntropy.shannonEntropy d = 0 :=
 161  ShannonEntropy.zero_entropy_deterministic d i hdet hother
 162
 163/-- **THEOREM IC-001.12**: Maximum entropy occurs for the uniform distribution.
 164    Uniform = maximum uncertainty = maximum information cost. -/
 165theorem uniform_has_max_entropy (n : ℕ) (hn : n > 0) :
 166    ShannonEntropy.shannonEntropy (ShannonEntropy.uniform n hn) = Real.log n :=
 167  ShannonEntropy.max_entropy_uniform n hn
 168
 169/-! ## §V. Information Cost Over Ledger States -/
 170
 171/-- A ledger state: a finite collection of recognition events. -/
 172structure LedgerState where
 173  /-- The recognition events in this state. -/
 174  events : List RecognitionEvent
 175
 176/-- Total information cost of a ledger state. -/
 177noncomputable def totalInfoCost (s : LedgerState) : ℝ :=
 178  s.events.foldl (fun acc e => acc + infoCost e) 0
 179
 180/-- Helper: foldl of nonneg additions starting from 0 is nonneg. -/
 181private lemma foldl_add_nonneg (es : List RecognitionEvent) (acc : ℝ) (hacc : acc ≥ 0) :
 182    es.foldl (fun a e => a + infoCost e) acc ≥ 0 := by
 183  induction es generalizing acc with
 184  | nil => simpa
 185  | cons e es ih =>
 186    simp only [List.foldl_cons]
 187    apply ih
 188    linarith [info_cost_nonneg e]