theorem proved term proof

`empty_ledger_net_flow`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 120theorem empty_ledger_net_flow (agent : ℕ) : net_flow empty_ledger agent = 0 := by

Term-mode proof.

 121  simp [net_flow, empty_ledger]
 122
 123/-! ## Conservation from Symmetry -/
 124
 125/-- Log reciprocal cancellation: log(r) + log(1/r) = 0. -/

Lean names referenced from this declaration's body.