net_zero

formal source

 107def net (L : Ledger) : ℤ := L.total_debit + L.total_credit
 108
 109/-- Ledger net is always zero. -/
 110theorem net_zero (L : Ledger) : L.net = 0 := L.global_balance
 111
 112/-- Concatenate two ledgers. -/
 113def concat (L₁ L₂ : Ledger) : Ledger := {
 114  transactions := L₁.transactions ++ L₂.transactions,
 115  total_debit := L₁.total_debit + L₂.total_debit,
 116  total_credit := L₁.total_credit + L₂.total_credit,
 117  global_balance := by
 118    have h₁ := L₁.global_balance
 119    have h₂ := L₂.global_balance
 120    omega
 121}
 122
 123theorem concat_preserves_balance (L₁ L₂ : Ledger) :
 124    (concat L₁ L₂).net = 0 := (concat L₁ L₂).global_balance
 125
 126end Ledger
 127
 128/-! ## Conservation Laws as Ledger Instances -/
 129
 130/-- A conservation law: a named charge assignment with closure. -/
 131structure ConservationLaw (α : Type*) where
 132  /-- Name of the conserved quantity. -/
 133  name : String
 134  /-- Charge assignment to elements. -/
 135  charge : α → ℤ
 136  /-- Any interaction (list of elements) has net zero charge. -/
 137  closed : ∀ (interaction : List α), (interaction.map charge).sum = 0
 138
 139namespace ConservationLaw
 140