IsSignFlip
The predicate IsSignFlip selects those signed permutations on D coordinates whose axis permutation component is the identity, thereby isolating pure coordinate sign flips inside the hyperoctahedral group. Gauge theorists reconstructing SU(3) × SU(2) × U(1) from the automorphism group of the 3-cube cite this predicate when extracting the (Z/2Z)^D layer. The definition is a direct equality check on the permutation field.
claimLet $g$ be a signed permutation on $D$ coordinates, consisting of a permutation of the axes together with a sign assignment in $(Z/2Z)^D$. Then IsSignFlip$(g)$ holds if and only if the permutation component of $g$ is the identity map.
background
The module derives the full Standard Model gauge group from the automorphism group B3 of the 3-cube Q3, which decomposes as (Z/2Z)^3 ⋊ S3. SignedPerm is the structure whose elements are pairs (permutation of Fin D, sign map Fin D → Fin 2), representing the action on Z^D by signed coordinate changes. The local setting isolates three layers: axis permutations (Layer 1, S3), sign flips (Layer 2), and their even subgroup (Layer 2a). Upstream results include the SignedPerm definition itself and the cube-symmetry constructions for particle generations and quark colors.
proof idea
One-line definition that returns true precisely when the perm field of the input SignedPerm equals the reflexive identity equivalence on Fin D.
why it matters in Recognition Science
This predicate supplies the full sign-flip subgroup used to define IsEvenSignFlip, which isolates the even elements of order 2^(D-1) corresponding to the Weyl group of SU(2) × U(1). It fills Layer 2 in the B3 decomposition required to obtain the complete gauge group from cube automorphisms, with the sign flips providing the weak-isospin factor. The construction connects directly to the eight-tick octave and D = 3 forced by the Recognition Science chain.
scope and limits
- Does not constrain the sign vector component.
- Does not compute the subgroup order 2^D.
- Does not encode the semidirect product with axis permutations.
- Does not map sign flips to explicit gauge boson representations.
formal statement (Lean)
173def IsSignFlip {D : ℕ} (g : SignedPerm D) : Prop :=
proof body
Definition body.
174 g.perm = Equiv.refl _
175
176/-- The number of sign flips is 2^D (= 8 for D = 3). -/