axis_perm_count
plain-language theorem explainer
Axis permutations in D dimensions are counted by D factorial. Gauge group derivations from the 3-cube cite this when isolating the S3 factor that supplies the color structure of SU(3). The declaration is a direct abbreviation to the standard factorial on natural numbers.
Claim. The number of permutations of the $D$ coordinate axes is $D!$.
background
The GaugeFromCube module derives the Standard Model gauge group from the automorphism group B3 of the 3-cube Q3. Axis permutations form Layer 1 of the decomposition B3 = (Z/2Z)^D ⋊ S_D: the symmetric group S_D obtained by permuting the D coordinate axes. For D=3 this yields S3 of order 6, which acts on the three face-pairs to produce the color charges of SU(3).
proof idea
The declaration is a one-line definition that directly sets axis_perm_count D to Nat.factorial D.
why it matters
This supplies the S3 order used in s3_is_weyl_of_su3 to identify axis permutations with the Weyl group of SU(3) and in three_layer_factorization to factor the cube automorphism order as axis_perm_count 3 times even_sign_flip_count 3 times parity_quotient_order. It completes Layer 1 of the P-014 derivation in which S3 permutes the three directions identified with color charges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.