LedgerEvent

formal source

  52/-- A **ledger event** is a signed integer flow on an edge.
  53    Positive = debit, negative = credit.
  54    The group structure is (ℤ, +, 0). -/
  55structure LedgerEvent where
  56  /-- The flow value (positive = debit, negative = credit) -/
  57  flow : ℤ
  58deriving DecidableEq, Repr
  59
  60instance : Add LedgerEvent := ⟨fun e₁ e₂ => ⟨e₁.flow + e₂.flow⟩⟩
  61instance : Neg LedgerEvent := ⟨fun e => ⟨-e.flow⟩⟩
  62instance : Zero LedgerEvent := ⟨⟨0⟩⟩
  63
  64/-- The conjugate (paired) event: ē = −e. -/
  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 -/