def
definition
concat
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RRF.Foundation.Ledger on GitHub at line 113.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
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
141/-- Electric charge conservation (trivial example). -/
142def trivial : ConservationLaw Unit := {
143 name := "trivial",