factor_count
plain-language theorem explainer
The theorem asserts that the standard model gauge algebra decomposes into precisely three factors. Researchers deriving gauge groups from cube automorphisms would cite this count to confirm the three-layer rank structure. The proof is a direct decision computation on the finite type with three enumerated constructors.
Claim. The set of standard model gauge factors has cardinality three.
background
The module records the Lie-algebra structure of SU(3) × SU(2) × U(1) by enumerating its irreducible factors. SMGaugeFactor is the inductive type whose three constructors label the strong sector (eight generators), weak sector (three generators), and hypercharge sector (one generator); the type carries decidable equality and a Fintype instance. This sits inside the gauge algebra certificate that records the empirical generator counts 8 + 3 + 1 = 12.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype.card expression on the three-element finite type.
why it matters
The result populates the factor_count field of the SMGaugeAlgebraCert structure, which certifies the full set of generator counts. It directly implements the three-layer decomposition stated in the module documentation for the cube-automorphism rank structure, thereby supporting the Recognition Science claim that any gauge group with the same rank decomposition must possess exactly twelve generators.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.