ledger_balanced

formal source

  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 -/
 124
 125/-- Log reciprocal cancellation: log(r) + log(1/r) = 0. -/
 126theorem log_reciprocal_cancel {r : ℝ} (_hr : r > 0) : Real.log r + Real.log (r⁻¹) = 0 := by