gaugeRankSU3
plain-language theorem explainer
gaugeRankSU3 defines the SU(3) gauge rank as the integer 3, matching the three face-pair directions of the 3-cube. Researchers reconstructing the Standard Model gauge group from cube automorphisms cite this when assembling the (3,2,1) decomposition. The declaration is a direct constant definition with no lemmas or computation.
Claim. The rank of the SU(3) gauge group is defined as the natural number 3.
background
The Gauge Group from 3-Cube module derives the Standard Model gauge ranks from the 3-cube Q₃ and its automorphism group B₃ = (ℤ/2)³ ⋊ S₃. Three face-pair directions in the cube fix the SU(3) rank component, while two sub-cube orientations and one phase fix the remaining ranks. This definition supplies the value 3 for the first component, consistent with D = 3 spatial dimensions from the forcing chain T8.
proof idea
The declaration is a direct definition that assigns the constant 3. No lemmas are applied and no tactics are used.
why it matters
This definition anchors the SU(3) rank in the cube-derived gauge structure and feeds directly into GaugeCubeCert, rankDecomposition, totalGaugeRank, and su3_rank_eq_face_pairs. It realizes the (3,2,1) partition of total rank 6 as the unique decreasing partition with first part equal to D = 3. Downstream theorems confirm the match to the Standard Model gauge group.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.