`LedgerState`

definition

show as: view math explainer →

module: IndisputableMonolith.Information.InformationIsLedger
domain: Information
line: 172 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Information.InformationIsLedger on GitHub at line 172.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 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]
 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. -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.