def
definition
emptyLedger
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.QuantumLedger on GitHub at line 95.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
92 (L.entries.map (·.cost)).sum
93
94/-- Empty ledger has zero balance. -/
95def emptyLedger : Ledger := {
96 entries := []
97 balance := 0
98 balance_eq := by simp
99}
100
101theorem empty_ledger_balance : emptyLedger.balance = 0 := rfl
102
103theorem empty_ledger_cost : totalCost emptyLedger = 0 := by
104 simp [totalCost, emptyLedger]
105
106/-! ## Ledger Updates -/
107
108/-- A ledger update is a pair of entries that cancel (reciprocal ratios). -/
109structure LedgerUpdate where
110 /-- First entry -/
111 entry1 : LedgerEntry
112 /-- Second entry (reciprocal) -/
113 entry2 : LedgerEntry
114 /-- The ratios are reciprocals -/
115 reciprocal : entry2.ratio = entry1.ratio⁻¹
116 /-- Different IDs -/
117 distinct : entry1.id ≠ entry2.id
118
119/-- Apply an update to a ledger. -/
120noncomputable def applyUpdate (L : Ledger) (u : LedgerUpdate) : Ledger := {
121 entries := u.entry1 :: u.entry2 :: L.entries
122 balance := L.balance -- Preserved because log(r) + log(1/r) = 0
123 balance_eq := by
124 simp only [List.map_cons, List.sum_cons]
125 have h_cancel : Real.log u.entry1.ratio + Real.log u.entry2.ratio = 0 := by