conj_involution

formal source

  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]
  99
 100/-- **PROVED: Adding a paired event preserves balance.** -/
 101theorem paired_preserves_balance (page : LedgerPage)
 102    (h : IsBalanced page) (e : LedgerEvent) :
 103    IsBalanced ⟨page.events ++ [e, e.conj], 0⟩ := by
 104  rcases page with ⟨events, bal⟩
 105  simp [IsBalanced, computeBalance, List.foldl_append, LedgerEvent.conj] at h ⊢