smGaugeAlgebraCert
plain-language theorem explainer
The definition assembles the Standard Model gauge algebra certificate by populating its fields with the certified generator counts for the strong, weak, and hypercharge sectors. A physicist tracing gauge groups back to cube automorphisms cites it to record the exact 8 + 3 + 1 = 12 match. The construction is a direct structure instantiation that simply names the already-decided count theorems for each field.
Claim. The SM gauge algebra certificate is the structure satisfying strong generators = 8, weak generators = 3, hypercharge generators = 1, total generators = 12, and number of gauge factors = 3.
background
The module records the Lie-algebra-level generator counts that accompany the cube-automorphism rank decomposition B₃ = (ℤ/2)³ ⋊ S₃ already established for the SM gauge group ranks (3, 2, 1). The structure SMGaugeAlgebraCert packages five facts: the strong factor contributes 8 generators, the weak factor contributes 3, the hypercharge factor contributes 1, the sum is exactly 12, and exactly three distinct factors appear. Upstream theorems establish each count separately by direct computation on the finite type of SMGaugeFactor.
proof idea
The definition is a direct structure constructor. It assigns the result of the strong_gen_count theorem to the strong field, the weak_gen_count theorem to the weak field, the hyper_gen_count theorem to the hyperY field, the sm_total_gen_count theorem to the total field, and the factor_count theorem to the factor_count field.
why it matters
This definition supplies the concrete numerical certificate that any RS-derived gauge group with the same cube-automorphism decomposition must possess exactly twelve generators. It closes the generator-count layer of the SM gauge algebra module and thereby supports the structural prediction that deviations from twelve generators would falsify the cube-to-gauge identification. No downstream theorems yet consume the certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.