totalGaugeRank
plain-language theorem explainer
The theorem establishes that the ranks assigned to SU(3), SU(2), and U(1) sum to 6. Model builders deriving the Standard Model gauge structure from the 3-cube automorphism group would cite this when confirming the total rank matches the expected value. The proof is a one-line decision procedure that evaluates the three constant definitions directly.
Claim. $3 + 2 + 1 = 6$, where the summands are the ranks of SU(3), SU(2), and U(1) respectively.
background
The Gauge Group from 3-Cube module derives the (3,2,1) rank decomposition of SU(3)×SU(2)×U(1) from the cube automorphism group B₃ = (ℤ/2)³ ⋊ S₃. The 3-cube Q₃ supplies three face-pair directions (SU(3) rank 3), two principal sub-cube orientations (SU(2) rank 2), and one overall phase (U(1) rank 1). Upstream definitions fix gaugeRankSU3 := 3, gaugeRankSU2 := 2, and gaugeRankU1 := 1, while the phase function from EightTick supplies the 8-tick periodicity kπ/4.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the arithmetic sum of the three gauge rank constants.
why it matters
This supplies the total_rank field inside the GaugeCubeCert certificate, confirming that the rank decomposition sums to 6 and matches the dimension of the Standard Model gauge algebra. It closes the rank accounting step in the derivation of the gauge group from the 3-cube, consistent with D=3 spatial dimensions. The parent structure gaugeCubeCert packages this with the decomposition and face-pair equalities for downstream use in the Wolfenstein A prediction extension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.