theorem
proved
empty_ledger_cost
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.QuantumLedger on GitHub at line 103.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
reciprocal -
of -
totalCost -
of -
A -
empty_ledger_cost -
reciprocal -
is -
of -
totalCost -
emptyLedger -
totalCost -
is -
of -
is -
of -
A -
is -
A -
that
used by
formal source
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
126 rw [u.reciprocal, Real.log_inv]
127 ring
128 rw [L.balance_eq]
129 linarith [h_cancel]
130}
131
132/-- **CONSERVATION THEOREM**: Applying an update preserves balance. -/
133theorem ledger_balance_conserved (L : Ledger) (u : LedgerUpdate) :