SMGaugeAlgebraCert
plain-language theorem explainer
The SM gauge algebra certificate packages the generator counts 8 for the strong factor, 3 for the weak factor, and 1 for hypercharge, together with their sum of 12 and the fact that exactly three factors exist. A physicist deriving gauge groups from cube automorphisms would cite this record to verify that the Lie-algebra dimensions match the observed Standard Model. The declaration is a plain structure definition that assembles the five assertions directly from the factor-count functions.
Claim. A certificate asserting that the strong gauge factor has $8$ generators, the weak gauge factor has $3$ generators, the hypercharge factor has $1$ generator, the total number of gauge generators is $12$, and the set of gauge factors has cardinality $3$.
background
The module establishes the Lie-algebra structure of the Standard Model gauge group by recording the canonical generator counts $(8,3,1)$ for $(su(3),su(2),u(1))$. SMGaugeFactor is the inductive type whose three constructors label the strong, weak, and hypercharge sectors. factorGenCount maps each constructor to the appropriate count via suGenCount for the non-abelian factors and uGenCount for the abelian one. smTotalGenCount is defined as the sum of these three values. The upstream factor_count theorem states that the cardinality of SMGaugeFactor is exactly $3$, matching the three-layer decomposition of the cube automorphism group.
proof idea
The declaration is a structure definition with no proof obligations. It simply records the five equalities that constitute the certificate, each of which is supplied by the sibling definitions factorGenCount, smTotalGenCount, and the theorem factor_count.
why it matters
This certificate is instantiated by the downstream definition smGaugeAlgebraCert, which supplies the concrete numerical values. The module doc states that any RS-derived gauge group sharing the cube-automorphism rank decomposition must have exactly twelve generators; the certificate makes that numerical claim explicit and falsifiable. It therefore closes the Lie-algebra-level part of the gauge-from-cube identification begun in GaugeFromCube and GaugeGroupStructure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.