even_sign_flip_count
plain-language theorem explainer
even_sign_flip_count supplies the order of the even-parity sign-flip subgroup in D dimensions as 2 to the power of D minus one. Researchers deriving the Standard Model gauge group from hyperoctahedral symmetry of the three-cube cite it when isolating the middle layer of the automorphism group. The declaration is a direct closed-form definition that counts the kernel of the parity homomorphism on sign patterns.
Claim. The cardinality of the even sign-flip subgroup of the signed permutation group in dimension $D$ is $2^{D-1}$.
background
This module derives the Standard Model gauge group from the automorphism group of the three-cube. The hyperoctahedral group B_3 decomposes into three layers: axis permutations of order 6, even sign flips, and the parity quotient of order 2. The even sign flips are the kernel of the parity map from (Z/2Z)^D to Z/2Z, consisting of sign patterns with an even number of minus signs.
proof idea
The declaration is a one-line definition returning the closed-form expression 2 raised to (D minus 1). Downstream theorems apply it by direct rewriting followed by numerical simplification.
why it matters
It supplies the factor 4 in the three-layer factorization theorem that decomposes the cube automorphism order as 48 equals 6 times 4 times 2. The parent result even_flips_give_weak_structure invokes it to identify the (Z/2Z)^2 subgroup with the Weyl group of SU(2) times U(1). This completes the gauge-group derivation for D equals 3 in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.