cubeFacePairs
plain-language theorem explainer
The definition assigns the natural number 3 to the count of face-pair directions on the 3-cube. Gauge theorists reconstructing Standard Model ranks from cube symmetries cite this constant to fix the SU(3) component. The assignment is a direct geometric count drawn from the three spatial directions of Q3.
Claim. The number of face-pair directions on the three-dimensional cube $Q_3 = {0,1}^3$ is 3.
background
The module derives the (3,2,1) rank decomposition of SU(3)×SU(2)×U(1) from the automorphism group B3 of the 3-cube Q3. The cube possesses three face-pair directions, two principal sub-cube orientations, and one overall phase, yielding total rank 6. This matches the Standard Model gauge group rank and is the unique decreasing partition of 6 into three parts consistent with D=3.
proof idea
The definition is a direct assignment of the constant 3, encoding the geometric count of face pairs in three dimensions.
why it matters
This supplies the base value for su3_rank_eq_face_pairs and GaugeCubeCert, which certify gaugeRankSU3 = 3 and the full (3,2,1) decomposition. It implements the T8 step of the forcing chain, where D=3 spatial dimensions are forced, grounding the gauge group ranks in Recognition Science geometry. The parent theorems are the equality and certification statements that close the cube-to-gauge link.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.