ConservationLaw
ConservationLaw encodes a named integer charge on any type α such that the net charge over every finite list of elements is zero. Ledger-based derivations of conservation in Recognition Science cite this structure when instantiating specific laws for energy, momentum or charge. The declaration is a plain structure with three fields and carries no proof obligations.
claimA conservation law on a type $α$ is a triple consisting of a name $N$, a charge function $q:α→ℤ$, and a closure condition asserting that for every list $l$ of elements of $α$ the sum of $q$ applied to the elements of $l$ equals zero.
background
The RRF.Foundation.Ledger module presents ledger algebra as the accounting structure that enforces conservation via double-entry bookkeeping: every transaction satisfies debit plus credit equals zero. Conservation laws appear as concrete instances of this ledger closure. Upstream results supply the J-cost calibration from PhiForcingDerived and the gauge content from SpectralEmergence that later motivate the specific conserved quantities appearing in the Physics layer.
proof idea
The declaration is a structure definition that introduces three fields directly: a String name, an integer-valued charge map, and a universal quantification over lists that enforces zero net charge. No lemmas or tactics are invoked; the definition stands alone as a type with no computational content.
why it matters in Recognition Science
This structure supplies the common interface used by ConservationCert to assert that exactly five conservation laws exist, three of which arise from spacetime symmetries corresponding to D = 3. It is instantiated locally for the trivial charge and for particle-antiparticle pairs, and feeds the inductive enumeration of energy, momentum, angular momentum, electric charge and baryon number in ConservationLawsFromRS.
scope and limits
- Does not enumerate which physical quantities receive conservation laws.
- Does not derive the laws from the Recognition forcing chain T0-T8.
- Does not distinguish continuous versus discrete charge assignments.
- Does not supply a mechanism for generating additional laws.
formal statement (Lean)
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). -/