trivial
plain-language theorem explainer
This definition supplies the trivial conservation law on the unit type by assigning zero charge to every element and verifying that the sum over any interaction list vanishes. Ledger-based models of electric charge conservation cite it as the base case before introducing particle distinctions. The verification proceeds via two inductions on list length to establish the zero-sum property.
Claim. Let $C$ be the conservation law on the unit type with charge function identically zero. Then for any finite list of elements the sum of their charges equals zero.
background
The RRF ledger algebra encodes conservation through double-entry bookkeeping: every transaction balances debit and credit, and each conservation law is an instance of ledger closure. A conservation law is a named quantity equipped with a charge map from elements to integers such that the total charge summed over any interaction list is zero. The module sets this structure as the core accounting device for quantities including energy, momentum, and electric charge.
proof idea
The definition builds the structure by providing the name string, the constant-zero charge function, and a closure proof. The proof first applies induction on list length to show that the constant-zero map produces a list of zeros, then applies a second induction on length to conclude that the sum of any number of zeros is zero.
why it matters
This definition instantiates the conservation-law structure at its simplest level, anchoring the ledger framework before particle-antiparticle or multi-element cases appear. It directly supports the general ConservationLaw type used in physics derivations from the RS-native units and forcing chain. No downstream results depend on it yet, leaving it as an illustrative base case within the RRF foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.