rankDecomposition
plain-language theorem explainer
The theorem establishes the gauge rank decomposition as 3 for SU(3), 2 for SU(2), and 1 for U(1). Gauge theorists deriving the Standard Model group from cubic symmetries cite this result. The proof is a direct term that applies reflexivity to the three constant definitions.
Claim. The gauge ranks satisfy $rank(SU(3)) = 3$, $rank(SU(2)) = 2$, and $rank(U(1)) = 1$.
background
The Gauge Group from 3-Cube module derives the (3,2,1) partition from the automorphism group of the 3-cube Q3. gaugeRankSU3 is defined as 3 from the three face-pair directions, gaugeRankSU2 as 2 from the principal sub-cube orientations, and gaugeRankU1 as 1 from the overall phase. The module states that this yields the total rank 6 matching the SM gauge group and extends GaugeFromCube.lean with the Wolfenstein A prediction.
proof idea
The term proof is a one-line wrapper that applies reflexivity to each component of the conjunction, confirming equality to the hardcoded values 3, 2, and 1.
why it matters
This supplies the decomp field in gaugeCubeCert, which certifies the full gauge structure from the cube. It is referenced by CubicSymmetryCert and the rank_sum and rank_length theorems in CubicSymmetryGroupFromRS. The result realizes the rank decomposition step consistent with D=3 spatial dimensions in the forcing chain and the unique decreasing partition of 6 into three parts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.