axis_perm_count
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not include the sign-flip components of the hyperoctahedral group.
- Does not compute the action on the cube's vertices or faces.
- Does not derive the Lie algebra structure of SU(3).
- Does not address higher-dimensional cases beyond the factorial formula.
Lean usage
simp [axis_perm_count]formal statement (Lean)
166def axis_perm_count (D : ℕ) : ℕ := Nat.factorial D
proof body
Definition body.
167