ParticlePair
plain-language theorem explainer
ParticlePair is the inductive type distinguishing particles from antiparticles to support charge conservation within the RRF ledger. Researchers modeling conservation laws in Recognition Science cite it when defining signed quantities for transactions. The definition is a direct two-constructor inductive type with no proof obligations or additional structure.
Claim. The type of particle pairs is the inductive type generated by the two constructors particle and antiparticle.
background
The RRF ledger algebra treats conservation as double-entry bookkeeping: every transaction requires debit plus credit to equal zero. Each conservation law (energy, charge, momentum) appears as an instance of ledger closure. The ParticlePair type supplies the binary distinction required to assign opposite signs to particles and antiparticles, thereby enforcing net-zero charge on balanced entries.
proof idea
The declaration is the inductive definition of the particle-pair type with exactly two constructors.
why it matters
This definition is the immediate prerequisite for the particleCharge map that returns +1 for particle and -1 for antiparticle, thereby realizing charge conservation inside the ledger. It supplies the concrete distinction needed for the module's treatment of conservation laws as ledger closure and feeds directly into downstream charge-assignment functions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.