sign_flip_count
plain-language theorem explainer
The definition assigns to each natural number D the integer 2^D as the total count of independent sign flips across D coordinate axes. Researchers deriving the Standard Model gauge group from the hyperoctahedral symmetry of the 3-cube cite this count when isolating the sign-flip layer of B3. It is introduced by a direct equational definition with no reduction steps.
Claim. The total number of sign flips over $D$ axes equals $2^D$.
background
The module derives SU(3) × SU(2) × U(1) from the automorphism group B3 of the 3-cube Q3. B3 decomposes as the semidirect product (ℤ/2ℤ)^D ⋊ S_D, where the first factor consists of independent sign changes on each of the D axes. This definition supplies the order of that sign-flip component. For D = 3 the value is 8, which the module then splits into even and odd parity subgroups to recover the Weyl group of SU(2) × U(1). The construction sits after the face-pair derivations in ParticleGenerations and QuarkColors.
proof idea
The declaration is a direct definition that sets the count equal to 2 raised to the power D, with no lemmas applied and no tactics invoked.
why it matters
This definition supplies the cardinality of the full sign-flip subgroup inside the decomposition B3 = (ℤ/2ℤ)^3 ⋊ S3. The downstream theorem sign_flip_count_D3 specializes the count to D = 3 and isolates the even-parity subgroup of order 4. The step fills layer 2 of the module's gauge-group derivation and aligns with the eight-tick octave and D = 3 forced in the T0–T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.