smGaugeBosonCount
plain-language theorem explainer
The theorem states that the finite set of Standard Model gauge boson types has exactly five elements. Recognition Science researchers cite it to confirm that the force-carrier classification matches the configuration dimension derived from the spatial dimension. The proof is a one-line decision procedure that exhaustively counts the constructors of the enumerated inductive type.
Claim. The set of Standard Model gauge boson types has cardinality five, where the types are the gluon, $W^+$, $W^-$, $Z$, and the photon: $|5| = 5$.
background
The module certifies the Standard Model gauge group SU(3)×SU(2)×U(1) through its rank decomposition, with SU(3) of rank 3 tied to spatial dimension, SU(2) of rank 2, and U(1) of rank 1, for a total rank of six. SMGaugeBosonType is the inductive type whose constructors are gluon, Wplus, Wminus, Z, and photon; each constructor derives DecidableEq, Repr, BEq, and Fintype so that cardinality is computable. The framework distinguishes this count of five types from the total of twelve carriers once gluon multiplicity is restored, and equates the type count to configuration dimension five.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality Fintype.card of the finite type equals five. The tactic succeeds by exhaustive enumeration over the five constructors supplied by the inductive definition.
why it matters
This supplies the five_types field inside the smGroupCert definition that certifies the overall group structure. It completes the gauge-boson classification step in the RS derivation via GaugeGroupCube.lean and aligns with the forcing-chain assignment of configuration dimension five, consistent with the spatial dimension three that fixes the SU(3) rank.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.