SMGaugeBosonType
plain-language theorem explainer
SMGaugeBosonType enumerates the five Standard Model gauge boson species via an inductive type whose constructors are gluon, W+, W-, Z, and photon. Recognition Science derivations of the SM gauge group would cite it when matching force-carrier species to configuration dimension. The declaration is a direct inductive enumeration that derives Fintype to enable immediate cardinality proofs.
Claim. The inductive type of Standard Model gauge bosons consists of the five constructors gluon, $W^+$, $W^-$, $Z$, and photon.
background
The module establishes that the SM gauge group SU(3)×SU(2)×U(1) arises from the rank decomposition (3,2,1) summing to six, matching spatial dimension D=3 for SU(3), D-1=2 for SU(2), and the scalar phase for U(1). Five gauge-boson types are identified with configuration dimension D=5, distinct from the twelve carriers obtained once multiplicities (eight gluons, three weak bosons, one photon) are counted. Upstream Z supplies the integer map from the anchor relation that assigns sector-dependent integers to rational charges for later mass formulas, though it is not invoked inside the boson-type definition itself.
proof idea
The declaration is an inductive definition that introduces five constructors and automatically derives the instances DecidableEq, Repr, BEq, and Fintype.
why it matters
It supplies the carrier-type enumeration required by the downstream theorems smGaugeBosonCount (Fintype.card = 5) and SMGroupCert (which packages the five-type count with the rank sum 3+2+1=6, gluon multiplicity 8, and total carriers 12). The definition fills the A1 SM Depth step by equating the five boson types with configuration dimension D=5, consistent with the framework landmarks of the (3,2,1) rank decomposition and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.