SMCharge
plain-language theorem explainer
SMCharge enumerates the three conserved charges of the Standard Model as electric, baryon, and lepton. Researchers deriving conservation from topological linking in D=3 cite this enumeration when showing that exactly three independent charges exist only in that dimension. The declaration is a finite inductive type that derives decidable equality and finiteness with no additional lemmas.
Claim. The set of Standard Model charges is the inductive type whose constructors are electric charge, baryon number, and lepton number.
background
TopologicalConservation formalizes the claim that conservation laws arise from topology (linking in D=3) rather than from continuous symmetries. Charge is treated as a linking number, hence integer-valued and invariant under continuous deformation of trajectories in the ledger. The module imports DimensionForcing to establish that only D=3 permits non-trivial linking and ParticleGenerations to relate charges to face pairs.
proof idea
This is an inductive definition with three constructors (electric, baryon, lepton) that automatically derives DecidableEq and Fintype.
why it matters
The definition supplies the concrete charges for the F-012 certificate on topological conservation. It is referenced by topological_conservation_certificate to equate the card of the type with independent_charge_count 3 and by all_threes_unified to identify the same 3 across charges, face pairs, and winding numbers. This step completes the passage from dimension forcing to quantized, topologically protected conservation laws.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.