theorem proved term proof

`empty_ledger_cost`

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

formal statement (Lean)

 117theorem empty_ledger_cost : ledger_cost empty_ledger = 0 := by simp [ledger_cost, empty_ledger]

Term-mode proof.

 118
 119/-- The empty ledger has zero net flow. -/

From the project-wide theorem graph. These declarations reference this one in their body.

ledger_forcing_principle in IndisputableMonolith.Foundation.LedgerForcing decl_use
empty_ledger_cost in IndisputableMonolith.Foundation.QuantumLedger decl_use
finiteEulerLedger_cost_formula in IndisputableMonolith.NumberTheory.ConcreteEulerLedger decl_use

Lean names referenced from this declaration's body.