Ledger

formal source

  79/-! ## Ledger Structure with Conservation -/
  80
  81/-- A ledger is a collection of entries with conservation constraint. -/
  82structure Ledger where
  83  /-- The entries in the ledger -/
  84  entries : List LedgerEntry
  85  /-- Total balance (sum of log-ratios) -/
  86  balance : ℝ
  87  /-- Balance equals sum of log-ratios -/
  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) -/