pith. machine review for the scientific record. sign in
theorem proved tactic proof

cpt_preserves_balance

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 124theorem cpt_preserves_balance (L : Ledger) :
 125    ((L.entries.map applyCPT).map LedgerEntry.charge).sum = 0 := by

proof body

Tactic-mode proof.

 126  -- C negates charges: sum of negated charges = -(sum of charges) = -0 = 0
 127  have hsum : (L.entries.map LedgerEntry.charge).sum = 0 := L.balanced
 128  -- The transformed charge is -e.charge for each entry
 129  have h_map : (L.entries.map applyCPT).map LedgerEntry.charge =
 130      L.entries.map (fun e => -e.charge) := by
 131    rw [List.map_map]
 132    congr 1
 133  rw [h_map]
 134  -- Sum of negations = -(sum)
 135  rw [show (L.entries.map (fun e => -e.charge)).sum =
 136      -(L.entries.map LedgerEntry.charge).sum by
 137    induction L.entries with
 138    | nil => simp
 139    | cons h t ih => simp only [List.map_cons, List.sum_cons, ih]; ring]
 140  rw [hsum, neg_zero]
 141
 142/-- Helper: reverseTick is an involution. -/

depends on (18)

Lean names referenced from this declaration's body.