structure
definition
ConservationLaw
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.RRF.Foundation.Ledger on GitHub at line 131.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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",
144 charge := fun _ => 0,
145 closed := fun l => by
146 have h : l.map (fun _ => (0 : ℤ)) = List.replicate l.length 0 := by
147 induction l with
148 | nil => rfl
149 | cons _ _ ih => simp [ih, List.replicate_succ]
150 rw [h]
151 clear h
152 induction l.length with
153 | zero => rfl
154 | succ n ih => simp [List.replicate_succ, ih]
155}
156
157/-- Conservation law from particle-antiparticle pairs. -/
158inductive ParticlePair | particle | antiparticle
159
160def particleCharge : ParticlePair → ℤ
161 | .particle => 1