su3_rank_eq_face_pairs
plain-language theorem explainer
The declaration equates the SU(3) gauge rank to the number of face-pair directions on the 3-cube. Researchers deriving Standard Model gauge structure from cube symmetries would cite this step. The proof is a direct reflexivity reduction because both quantities are defined as the constant 3.
Claim. The rank of SU(3) equals the number of face-pair directions of the three-dimensional cube: $3=3$.
background
The module derives the (3,2,1) rank decomposition of the Standard Model gauge group from the automorphism group of the 3-cube. cubeFacePairs counts the three face-pair directions that arise from D=3 spatial dimensions. gaugeRankSU3 is defined as the integer 3 to capture the SU(3) contribution to the total rank of 6.
proof idea
One-line reflexivity proof. Both sides are definitionally equal to the constant 3, so the equality holds immediately by rfl.
why it matters
The equality is invoked inside gaugeCubeCert to certify the full (3,2,1) decomposition. It supplies the SU(3) component of the rank partition that the module obtains from the 3-cube automorphism group B3, consistent with the Recognition Science derivation of D=3 and the total gauge rank 6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.