ConservationLaw
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.