def
definition
def or abbrev
applyUpdate
show as:
view Lean formalization →
formal statement (Lean)
120noncomputable def applyUpdate (L : Ledger) (u : LedgerUpdate) : Ledger := {
proof body
Definition body.
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. -/