particleCharge
plain-language theorem explainer
particleCharge supplies the integer charge map for ParticlePair in the RRF ledger. Researchers building conservation laws for charge or baryon number would reference it when instantiating the ConservationLaw structure. The definition is a direct case split on the two constructors of ParticlePair.
Claim. The function assigning charges to particle pairs satisfies $q(particle) = 1$ and $q(antiparticle) = -1$.
background
The module establishes the Ledger as a list of transactions with global balance enforced by total debit plus total credit equaling zero. ConservationLaw packages a name, a charge map from type α to ℤ, and the requirement that every list of elements has net charge sum zero. ParticlePair is the inductive type with constructors particle and antiparticle, used to model pairs in conservation statements. Upstream, this draws on the general ConservationLaw inductive from Physics.ConservationLawsFromRS and the Mass abbrev from RSNativeUnits.
proof idea
The definition is implemented by pattern matching directly on the ParticlePair inductive type.
why it matters
It completes the charge component inside the ConservationLaw structure for the ledger, enabling instances that enforce zero net charge for interactions. This supports the double-entry bookkeeping principle in RRF, which aligns with the Recognition Science forcing chain through conservation closure. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.