paired_event_sum_zero

formal source

  65def LedgerEvent.conj (e : LedgerEvent) : LedgerEvent := ⟨-e.flow⟩
  66
  67/-- **PROVED: Paired events sum to zero (double-entry).** -/
  68theorem paired_event_sum_zero (e : LedgerEvent) : e + e.conj = 0 := by
  69  cases e with
  70  | mk flow =>
  71      change ({ flow := flow + (-flow) } : LedgerEvent) = { flow := 0 }
  72      simp
  73
  74/-- **PROVED: Conjugation is an involution.** -/
  75theorem conj_involution (e : LedgerEvent) : e.conj.conj = e := by
  76  cases e
  77  simp [LedgerEvent.conj]
  78
  79/-! ## §2. The Ledger as a Multiset of Paired Events -/
  80
  81/-- A **ledger page** is a finite list of events with a balance constraint. -/
  82structure LedgerPage where
  83  /-- The events on this page -/
  84  events : List LedgerEvent
  85  /-- The balance: sum of all flows -/
  86  balance : ℤ := events.foldl (fun acc e => acc + e.flow) 0
  87
  88/-- Compute the balance of a list of events. -/
  89def computeBalance (events : List LedgerEvent) : ℤ :=
  90  events.foldl (fun acc e => acc + e.flow) 0
  91
  92/-- A **balanced ledger page** has σ = 0. -/
  93def IsBalanced (page : LedgerPage) : Prop :=
  94  computeBalance page.events = 0
  95
  96/-- The empty page is balanced. -/
  97theorem empty_balanced : IsBalanced ⟨[], 0⟩ := by
  98  simp [IsBalanced, computeBalance]