even_flips_give_weak_structure
plain-language theorem explainer
The even sign-flip subgroup of the hyperoctahedral group B_3 in three dimensions has order 4, satisfying the arithmetic identity 4 = 2 times the parity quotient order. Gauge theorists deriving the Standard Model group from discrete cube symmetries cite this result to fix the (Z/2Z)^2 layer. The proof is a direct term-mode verification that applies reflexivity to the outer equalities and numerical normalization to the middle step.
Claim. For dimension $D=3$, the order of the even sign-flip subgroup equals $2^{D-1}=4$, and this order equals twice the parity quotient order.
background
The module derives the Standard Model gauge group SU(3) x SU(2) x U(1) from the automorphism group B_3 of the 3-cube. B_3 decomposes as (Z/2Z)^3 ⋊ S_3 with three layers: axis permutations (order 6) for SU(3), even sign flips (order 4) for SU(2) x U(1), and the parity quotient (order 2) for U(1). The even sign-flip count is defined as 2^(D-1) for general D; for D=3 this yields the kernel of the parity map on (Z/2Z)^3. The parity quotient order is the constant 2, identified with the remaining Z/2Z factor.
proof idea
The proof is a term-mode triple of conjuncts. Reflexivity discharges the first equality (even sign-flip count 3 = 2^(3-1)) and the third (4 = 2 * parity quotient order). The middle numerical step 2^(3-1) = 4 is discharged by norm_num.
why it matters
This result fixes the order of the even sign-flip layer, which the module doc-comment identifies as the Weyl group of SU(2) x U(1). It supplies the middle factor in the three-layer factorization |B_3| = 6 x 4 x 2. Within the Recognition Science chain the lemma closes the discrete symmetry origin of the weak sector after the S_3 layer for color has already been established.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.