sm_charge_count
plain-language theorem explainer
The theorem establishes that the Standard Model possesses exactly three conserved charges by computing the cardinality of the inductive type SMCharge. Researchers tracing topological origins of conservation in D = 3 would cite this to confirm the charge count matches the three independent axes forced by dimension. The proof is a direct decision procedure that enumerates the three constructors of the finite type.
Claim. The set of Standard Model charges has cardinality three: $ |SMCharge| = 3 $.
background
SMCharge is the inductive type whose constructors are electric, baryon, and lepton, representing the three conserved charges of the Standard Model. The module formalizes conservation as arising from topological linking numbers in D = 3 rather than continuous symmetries, with the key distinction that topological charges are integer-valued and invariant under continuous deformation. This result rests on the SMCharge definition and feeds the claim that exactly three independent charges exist only in three dimensions.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the finite inductive type SMCharge, whose three constructors are enumerated by the Fintype instance.
why it matters
This supplies the explicit count of three that is required by sm_charges_match_D3 and the topological_conservation_certificate (F-012), which asserts that conservation laws are topological, integer-valued, and possible only in D = 3. It unifies with all_threes_unified in WindingCharges and closes the loop between the charge definition and the dimension-forcing chain (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.