LedgerUpdate

formal source

 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) :
 134    (applyUpdate L u).balance = L.balance := rfl
 135
 136/-- **COST ADDITIVITY**: The cost of an updated ledger is the sum of costs. -/
 137theorem ledger_cost_additive (L : Ledger) (u : LedgerUpdate) :
 138    totalCost (applyUpdate L u) = u.entry1.cost + u.entry2.cost + totalCost L := by
 139  simp only [totalCost, applyUpdate, List.map_cons, List.sum_cons]