`balanced`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.LedgerForcing
domain: Foundation
line: 93 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.LedgerForcing on GitHub at line 93.

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

  90  L.events.foldl (fun acc e => acc + event_cost e) 0
  91
  92/-- A ledger is balanced if its event list is balanced. -/
  93def balanced (L : Ledger) : Prop := balanced_list L.events
  94
  95/-- Every Ledger is balanced by construction. -/
  96theorem ledger_balanced (L : Ledger) : balanced L := L.double_entry
  97
  98/-- The net flow at an agent. -/
  99noncomputable def net_flow (L : Ledger) (agent : ℕ) : ℝ :=
 100  L.events.foldl (fun acc e =>
 101    if e.source = agent then acc + Real.log e.ratio
 102    else if e.target = agent then acc + Real.log e.ratio
 103    else acc) 0
 104
 105/-! ## The Empty Ledger -/
 106
 107/-- The empty ledger: no events. -/
 108def empty_ledger : Ledger := {
 109  events := []
 110  double_entry := fun _ => by simp [List.count_nil]
 111}
 112
 113/-- The empty ledger is balanced. -/
 114theorem empty_ledger_balanced : balanced empty_ledger := empty_ledger.double_entry
 115
 116/-- The empty ledger has zero cost. -/
 117theorem empty_ledger_cost : ledger_cost empty_ledger = 0 := by simp [ledger_cost, empty_ledger]
 118
 119/-- The empty ledger has zero net flow. -/
 120theorem empty_ledger_net_flow (agent : ℕ) : net_flow empty_ledger agent = 0 := by
 121  simp [net_flow, empty_ledger]
 122
 123/-! ## Conservation from Symmetry -/

papers checked against this theorem

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