parity_quotient_order
plain-language theorem explainer
The definition assigns the natural number 2 to the order of the parity quotient group obtained from the sign-flip subgroup of the hyperoctahedral group B₃. Gauge theorists reconstructing the Standard Model factors SU(3) × SU(2) × U(1) from 3-cube automorphisms cite this constant when completing the layer decomposition 48 = 6 × 4 × 2. It is introduced by direct assignment with no further reduction steps required.
Claim. Let $Q$ denote the quotient of the sign-flip group $(ℤ/2ℤ)^3$ by its even subgroup. Then the order of $Q$ equals 2. This supplies the $U(1)$ factor associated with weak hypercharge.
background
The module derives the Standard Model gauge group SU(3) × SU(2) × U(1) from the automorphism group B₃ of the 3-cube Q₃. B₃ admits the decomposition B₃ = (ℤ/2ℤ)³ ⋊ S₃ with |B₃| = 48 and a natural three-layer splitting: axis permutations (order 6), even sign flips (order 4), and the parity quotient (order 2). The parity quotient is the image of the parity homomorphism ε : (ℤ/2ℤ)³ → ℤ/2ℤ, yielding exactly ℤ/2ℤ. This layer is identified with the U(1) weak hypercharge factor.
proof idea
Direct constant definition that sets the value to 2. No lemmas or tactics are invoked; the declaration simply names the integer for reference in later statements about gauge-layer correspondences.
why it matters
The definition completes the third factor in the three-layer factorization theorem, which asserts that the order of B₃ equals axis_perm_count 3 times even_sign_flip_count 3 times this order. It is invoked by even_flips_give_weak_structure and parity_gives_hypercharge to map the even-flip subgroup to SU(2) and the parity layer to U(1) hypercharge. Within the Recognition framework the construction supplies the U(1) piece once D = 3 has fixed the cube symmetry, closing one step in the gauge-group derivation from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.