IsEvenSignFlip
Defines the even sign-flip subgroup inside the hyperoctahedral group B_D as those signed permutations whose permutation part is the identity and whose sign vector has even parity. Gauge theorists deriving the Standard Model from discrete cube symmetries cite this for the (Z/2Z)^2 factor that supplies the SU(2) weak isospin structure. The definition is a direct conjunction of the IsSignFlip predicate with an even-sum check on the sign coordinates.
claimFor $D : ℕ$ and $g$ a signed permutation on $D$ coordinates, $g$ belongs to the even sign-flip subgroup when its permutation component is the identity and the sum of its sign values is even: $g.perm = id$ and $∑_{i=1}^D val(g.signs(i)) ≡ 0 mod 2$.
background
SignedPerm D is the structure whose elements are pairs (perm, signs) with perm an element of the symmetric group on Fin D and signs a function Fin D → Fin 2; it realizes the hyperoctahedral group B_D acting on Z^D by signed coordinate permutations. IsSignFlip isolates the pure sign-flip elements (identity permutation, arbitrary signs) whose order is 2^D. The module GaugeFromCube decomposes B_3 into three layers: axis permutations S_3 (SU(3) color), the full sign-flip group (Z/2Z)^3, and its even-parity subgroup of index 2.
proof idea
One-line wrapper that applies IsSignFlip and checks Even on the sum of the sign values over Fin D.
why it matters in Recognition Science
Supplies the explicit definition of Layer 2a in the three-layer decomposition of B_3 that yields the Weyl group of SU(2) × U(1). It sits inside the derivation of SU(3) × SU(2) × U(1) from Aut(Q_3) and feeds the spectral emergence claim that the cube simultaneously forces the full gauge content together with three generations and 24 chiral fermions. The construction uses the parity homomorphism whose kernel is this subgroup, closing the gap between the full sign-flip group and the even subgroup required for the weak sector.
scope and limits
- Does not prove that the defined set forms a subgroup of B_D.
- Does not exhibit the isomorphism to (Z/2Z)^2.
- Does not derive the Lie-algebra structure of SU(2) from the generators.
- Does not compute the action on fermion representations.
formal statement (Lean)
187def IsEvenSignFlip {D : ℕ} (g : SignedPerm D) : Prop :=
proof body
Definition body.
188 IsSignFlip g ∧ Even (∑ i : Fin D, (g.signs i).val)
189
190/-- The parity of a sign-flip element: the total number of flipped signs mod 2. -/