applyUpdate

formal source

 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]
 140  ring
 141
 142/-! ## Quantum Superposition -/
 143
 144/-- A quantum state is a superposition over ledger configurations. -/
 145structure QuantumState (n : ℕ) where
 146  /-- The possible ledger configurations -/
 147  configurations : Fin n → Ledger
 148  /-- Complex amplitudes -/
 149  amplitudes : Fin n → ℂ
 150  /-- Normalization: |ψ|² = 1 -/