color_from_axis_permutations
plain-language theorem explainer
The result equates the number of axis permutations on the three-dimensional cube to the factorial of the color count, confirming that the S₃ factor in the cube automorphism group supplies the Weyl group order for the SU(3) color symmetry. Gauge theorists reconstructing the Standard Model from geometric symmetries of Q₃ would cite this identification. The proof is a one-line simplification that unfolds the definitions of axis permutation count as D! and color count from face-pair data.
Claim. The number of permutations of the three coordinate axes equals the factorial of the number of colors: $3! = (N_c(3))!$.
background
The GaugeFromCube module starts from the 3-cube Q₃ whose automorphism group is the hyperoctahedral group B₃ = (ℤ/2ℤ)³ ⋊ S₃ of order 48. Axis permutations constitute the S₃ factor of order 6; these act on the three face-pairs of the cube. The sibling definition axis_perm_count D := Nat.factorial D therefore returns 6 when D = 3. N_colors is obtained from the face_pairs construction in ParticleGenerations, which assigns three colors to the three face-pairs when D = 3. The local setting is the first layer of the gauge-group derivation: S₃ supplies the color structure of SU(3).
proof idea
The proof is a one-line simp tactic that applies the definitions of axis_perm_count, N_colors, and face_pairs, reducing both sides of the equality to the numeral 6.
why it matters
The theorem supplies the explicit order match between axis permutations and color multiplicity, completing the S₃ → SU(3) step in the module's derivation of SU(3) × SU(2) × U(1) from B₃. It anchors the D = 3 spatial dimensions (T8) to the color degree of freedom via face-pair counting. No open scaffolding remains on this equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.