def
definition
totalCost
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 91.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
88 balance_eq : balance = (entries.map (fun e => Real.log e.ratio)).sum
89
90/-- The total J-cost of a ledger. -/
91noncomputable def totalCost (L : Ledger) : ℝ :=
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