def definition def or abbrev

`emptyLedger`

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

formal statement (Lean)

  95def emptyLedger : Ledger := {

Definition body.

  96  entries := []
  97  balance := 0
  98  balance_eq := by simp
  99}
 100

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

empty_ledger_balance in IndisputableMonolith.Foundation.QuantumLedger decl_use
empty_ledger_cost in IndisputableMonolith.Foundation.QuantumLedger decl_use
empty_ledger_phase in IndisputableMonolith.Foundation.QuantumLedger decl_use
quantum_ledger_fundamentals in IndisputableMonolith.Foundation.QuantumLedger decl_use