cubeFacePairs_eq_3
plain-language theorem explainer
The equality fixes the cube face-pair count at three to match the three spatial dimensions that generate the SU(3) factor in the standard-model gauge group. Researchers tracing the (3,2,1) rank decomposition from the 3-cube automorphism group B₃ cite this step when assembling the total gauge rank of six. The proof is a direct reflexivity reduction on the explicit definition of cubeFacePairs.
Claim. The number of face-pair directions on the three-cube equals three: $N = 3$, where $N$ denotes the cube face-pair count fixed by $D=3$.
background
The module derives the gauge group SU(3)×SU(2)×U(1) from the 3-cube Q₃ = {0,1}³ and its automorphism group B₃ = (ℤ/2)³ ⋊ S₃. Three face-pair directions supply the SU(3) rank, two principal sub-cube orientations supply the SU(2) rank, and one overall phase supplies the U(1) rank, yielding the unique decreasing partition (3,2,1) of total rank 6. The upstream definition cubeFacePairs : ℕ := 3 records the face-pair count for D=3. The rank definitions from PreTemporalForcingOrder and OrderPreservation supply numerical ordering on forcing stages and on states ordered by J-cost, respectively.
proof idea
The proof is a one-line term-mode wrapper that applies reflexivity directly to the definition cubeFacePairs := 3.
why it matters
The equality anchors the SU(3) rank inside the cube-face construction and thereby supports the full (3,2,1) decomposition of the standard-model gauge group. It realizes the T8 landmark that forces D=3 spatial dimensions from the eight-tick octave and the self-similar fixed point phi. No downstream theorems are recorded yet; the step closes the geometric origin of the gauge ranks without introducing new open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.