s3_is_weyl_of_su3
plain-language theorem explainer
The identification shows that the number of axis permutations on the 3-cube equals 3! and evaluates to 6, confirming S₃ as the Weyl group of SU(3) color. Researchers deriving gauge groups from polyhedral symmetries cite this step in the cube-to-SU(3) mapping. The proof is a direct term-mode verification that applies reflexivity to the definition and norm_num to the factorial value.
Claim. The number of permutations of the three coordinate axes equals $3!$ and $3! = 6$.
background
The module derives the Standard Model gauge group from the automorphism group of the 3-cube Q₃. Its vertices are {0,1}³ and the full automorphism group is the hyperoctahedral group B₃ of order 48, decomposed as (ℤ/2ℤ)³ ⋊ S₃. The S₃ factor permutes the three axes and therefore the three face-pairs, each tied to one color charge (red, green, blue) via the QuarkColors construction. The definition axis_perm_count D returns the factorial of D, so the case D = 3 yields the order of S₃. This rests on the prior derivations of three generations and three colors from the same face-pairs.
proof idea
The proof is a term-mode pair ⟨rfl, by norm_num⟩. Reflexivity equates axis_perm_count 3 to the definition Nat.factorial 3. Norm_num then evaluates the concrete equality 3! = 6.
why it matters
This supplies the order of the S₃ Weyl group inside the three-layer decomposition of B₃ that produces SU(3) × SU(2) × U(1) from cube symmetry. It completes the first layer, where axis permutations account for the rank-2 structure of SU(3) color. The result sits at the D = 3 step of the forcing chain and links the Recognition Composition Law to the emergence of color charges from face-pairs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.