SMGaugeFactor
plain-language theorem explainer
SMGaugeFactor enumerates the three gauge factors of the Standard Model as an inductive type with constructors for the strong, weak, and hypercharge sectors. A physicist deriving gauge symmetries from discrete structures would cite this to anchor the generator counts 8, 3, and 1. The definition proceeds by direct inductive enumeration that automatically derives decidable equality and finite cardinality.
Claim. The inductive type of Standard Model gauge factors consists of three constructors: one for the strong interaction corresponding to the Lie algebra of SU(3), one for the weak interaction corresponding to the Lie algebra of SU(2), and one for the hypercharge interaction corresponding to the Lie algebra of U(1).
background
This declaration sits in the SM Gauge Algebra module, which supplies the Lie-algebra-level structure for SU(3) × SU(2) × U(1) after the cube-automorphism certificate has matched the rank decomposition B₃ = (ℤ/2)³ ⋊ S₃ to the gauge ranks (3, 2, 1). The module records the canonical generator counts (8, 3, 1) that match the dimensions N²-1 for N = 3, 2, 1, with the total of 12 generators aligning with the empirical Standard Model count. Upstream dependencies supply RS-native units (with c = 1) and the Generator structure guaranteeing non-trivial generators via the Law of Logic.
proof idea
The declaration is an inductive definition with three explicit constructors and automatic derivation of DecidableEq, Repr, BEq, and Fintype. No separate proof body or tactic steps are required.
why it matters
The type anchors the downstream theorems factor_count (exactly three factors), factorGenCount (mapping to 8, 3, 1), and the certificate SMGaugeAlgebraCert (total of 12 generators). It realizes the Recognition Science structural prediction that any gauge group sharing the cube-automorphism rank decomposition must possess precisely 12 generators; deviation would falsify the gauge-group-from-cube identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.