IsAxisPermutation
IsAxisPermutation selects the subgroup of signed permutations on D coordinates whose sign vector is identically zero, isolating pure axis permutations inside the hyperoctahedral group B_D. Gauge theorists reconstructing the Standard Model from the 3-cube automorphism group cite this predicate when extracting the S3 factor that supplies the color symmetry of SU(3). The definition is realized by a direct predicate on the signs field of the input SignedPerm structure.
claimLet $g$ be a signed permutation of the integer lattice $Z^D$, consisting of an axis permutation together with a sign vector in $(Z/2Z)^D$. Then $g$ belongs to the axis-permutation subgroup if and only if every component of its sign vector equals zero.
background
The module derives the Standard Model gauge group SU(3) × SU(2) × U(1) from the automorphism group of the 3-cube Q3. The hyperoctahedral group B_D acts on Z^D by signed permutations: each element is a pair consisting of a permutation of the D axes and an independent sign choice for each axis. SignedPerm is the Lean structure that packages this data, with fields perm : Equiv.Perm (Fin D) and signs : Fin D → Fin 2. The module decomposes B3 into three layers; Layer 1 consists exactly of the axis permutations (S3) that leave all signs positive and permute the three face-pairs of the cube.
proof idea
The definition is a one-line predicate that inspects the signs component of the supplied SignedPerm value and requires it to be the constant zero function on Fin D.
why it matters in Recognition Science
This definition supplies the concrete S3 subgroup that the module identifies as the Weyl group of SU(3) and therefore as the source of the color factor in the gauge group. It forms the first layer in the explicit decomposition B3 = (Z/2Z)^3 ⋊ S3 used to obtain the full Standard Model gauge structure from cube automorphisms. The construction aligns with the Recognition Science program of obtaining gauge symmetries from the discrete symmetry group of the 3-cube rather than from postulated Lie algebras.
scope and limits
- Does not restrict the dimension D to equal 3.
- Does not include any sign-flip generators from the full hyperoctahedral group.
- Does not compute the cardinality of the resulting subgroup.
- Does not map the permutation to any specific gauge field or particle representation.
formal statement (Lean)
162def IsAxisPermutation {D : ℕ} (g : SignedPerm D) : Prop :=
proof body
Definition body.
163 ∀ i, g.signs i = 0
164
165/-- The number of axis permutations is D! (= 6 for D = 3). -/