sign_flip_count_D3
plain-language theorem explainer
sign_flip_count_D3 establishes that the total number of coordinate sign flips in three dimensions equals eight. Researchers deriving the Standard Model gauge group from the hyperoctahedral group of the 3-cube cite this specialization when counting the order of the sign-flip layer. The proof reduces to direct arithmetic evaluation of the power function at three.
Claim. The sign flip count in three dimensions satisfies $2^3 = 8$.
background
The module derives the Standard Model gauge group SU(3) × SU(2) × U(1) from the automorphism group of the 3-cube Q₃, which decomposes as (ℤ/2ℤ)³ ⋊ S₃. The sign flip count is defined as two raised to the dimension D and therefore counts the elements of the group (ℤ/2ℤ)^D of independent sign flips on the coordinate axes. The upstream definition sign_flip_count D := 2^D supplies the general formula, which this theorem specializes to D = 3. The local setting decomposes the full group into axis permutations (order 6) and sign flips (order 8) to recover the gauge factors.
proof idea
The proof is a one-line wrapper that invokes native_decide on the definition of sign_flip_count at argument three, which evaluates the power 2^3 directly to the numeral eight.
why it matters
This result supplies the order of the full sign-flip group in the layer decomposition of Aut(Q₃) that isolates the even subgroup of order four for the SU(2) factor. It supports the overall claim that the 3-cube symmetry forces the gauge content of the Standard Model and aligns with the Recognition Science forcing of three spatial dimensions. The specialization closes the count needed for the 24 chiral fermion flavors listed in the SpectralEmergence structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.