totalInfoCost

formal source

 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]
 189
 190/-- **THEOREM IC-001.13**: Total information cost is non-negative. -/
 191theorem total_info_cost_nonneg (s : LedgerState) : totalInfoCost s ≥ 0 := by
 192  unfold totalInfoCost
 193  exact foldl_add_nonneg s.events 0 (le_refl 0)
 194
 195/-- **THEOREM IC-001.14**: The empty ledger state has zero information cost.
 196    Consistent with: no recognition events = no information. -/
 197theorem empty_state_zero_cost : totalInfoCost ⟨[]⟩ = 0 := by
 198  unfold totalInfoCost
 199  simp
 200
 201/-- The "it from bit" principle formalized:
 202    Two ledger states are physically identical iff they have the same events. -/
 203theorem ledger_identity (s₁ s₂ : LedgerState) :
 204    s₁.events = s₂.events ↔ s₁ = s₂ := by
 205  constructor
 206  · intro h; cases s₁; cases s₂; simp_all
 207  · intro h; rw [h]