rankSU3
plain-language theorem explainer
rankSU3 defines the rank of the SU(3) factor in the Standard Model gauge group as the natural number 3. Physicists reconstructing the SM from Recognition Science forcing chains cite it when equating the SU(3) rank to spatial dimension D. The declaration is a direct constant assignment with no lemmas or computation required.
Claim. The rank of the Lie group $SU(3)$ is defined to be the natural number 3.
background
The module derives the Standard Model gauge group $SU(3)×SU(2)×U(1)$ via rank decomposition from the GaugeGroupCube construction. SU(3) rank is set equal to spatial dimension D, SU(2) rank to D-1, and U(1) rank to the scalar phase, with total rank 6. This matches the eight-tick octave and T8 step of the unified forcing chain that forces D=3.
proof idea
Direct definition that assigns the constant 3. No lemmas, tactics, or upstream results are applied; the value is supplied to match the spatial-dimension identification in the RS derivation.
why it matters
The definition supplies the SU(3) rank to gluonCount (yielding 8 gluons via $N^2-1$), totalRank (sum equals 6), and the SMGroupCert structure that certifies the full rank decomposition and carrier counts. It closes the T8 landmark by fixing D=3 as the SU(3) rank inside the SM group structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.