gaugeRankSU2
plain-language theorem explainer
gaugeRankSU2 sets the SU(2) gauge rank to 2 from the two principal sub-cube orientations in the 3-cube model. Researchers deriving the Standard Model gauge structure from cube symmetries cite this constant to fill the middle slot of the (3,2,1) partition. The declaration is a direct constant assignment with no computation.
Claim. The rank of the SU(2) gauge group factor is defined as $2$.
background
The GaugeGroupCube module derives the Standard Model gauge ranks from the automorphism group of the 3-cube Q₃. Face-pair directions give rank 3 for SU(3), two principal sub-cube orientations give rank 2 for SU(2), and one overall phase gives rank 1 for U(1), for a total rank of 6. This matches the rank of SU(3)×SU(2)×U(1) and is the unique decreasing partition of 6 into three parts with the leading term equal to spatial dimension D=3.
proof idea
The declaration is a direct definition that assigns the natural number 2.
why it matters
gaugeRankSU2 supplies the middle value required by GaugeCubeCert to certify the full (3,2,1) decomposition and total rank 6. It is used by rankDecomposition and totalGaugeRank to assert the equality gaugeRankSU3 = 3 ∧ gaugeRankSU2 = 2 ∧ gaugeRankU1 = 1. The assignment aligns with the Recognition Science forcing chain where D=3 emerges from the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.