factor_count
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not compute the generator count inside each factor.
- Does not prove the Lie-algebra isomorphism to the standard model.
- Does not address possible extensions or additional gauge factors.
formal statement (Lean)
57theorem factor_count : Fintype.card SMGaugeFactor = 3 := by decide
proof body
58