even_sign_flip_count_D3
plain-language theorem explainer
The even sign-flip subgroup of the signed permutation group on three axes has cardinality 4. Researchers deriving the Standard Model gauge group from the automorphism group of the 3-cube cite this when identifying the Weyl group of SU(2) × U(1). The proof evaluates the closed-form expression 2^(D-1) at D = 3 via native computation.
Claim. For spatial dimension $D=3$, the order of the even sign-flip subgroup of $(ℤ/2ℤ)^3$ is $4$.
background
In the Recognition Science derivation of the Standard Model gauge group from the 3-cube Q₃, the automorphism group B₃ decomposes into three layers. Layer 1 is the axis permutations S₃ of order 6, accounting for the SU(3) color factor. Layer 2 is the even sign-flip subgroup of (ℤ/2ℤ)³, which has order 4 and is isomorphic to (ℤ/2ℤ)². This subgroup is defined as the kernel of the parity map on sign flips and corresponds to the Weyl group of SU(2) × U(1). The general count even_sign_flip_count(D) equals 2^(D-1), so the D=3 case yields 4. Upstream results on spectral emergence from Q₃ simultaneously force the full gauge content SU(3)×SU(2)×U(1) along with three generations.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the definition even_sign_flip_count D := 2^(D-1) at D=3, confirming the order is 4.
why it matters
This result supplies the order-4 subgroup that completes the gauge group derivation in GaugeFromCube. It fills the Layer 2 component in the module's three-layer decomposition of B₃, directly yielding the '2' factor in SU(2) from the even sign flips. The parent structure is the spectral emergence theorem that extracts SU(3)×SU(2)×U(1) from Q₃ symmetry, consistent with D=3 forced by the eight-tick octave in the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.