parity_gives_hypercharge
plain-language theorem explainer
The parity quotient of the sign-flip subgroup in the hyperoctahedral group B₃ has order 2, and the hypercharge layer carries fundamental representation dimension 1. This pins the discrete ℤ/2ℤ structure to the U(1) factor in the gauge group extracted from 3-cube symmetries. A researcher reconstructing the Standard Model gauge factors from hyperoctahedral decompositions would cite the result to close the third layer of the 48 = 6 × 4 × 2 factorization. The proof reduces to reflexivity on the explicit layer definitions.
Claim. The parity quotient of the sign-flip group has order 2 and the fundamental representation dimension of the hypercharge layer equals 1.
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 a three-layer decomposition: axis permutations of order 6 (S₃, Weyl group of SU(3)), even sign flips of order 4 ((ℤ/2ℤ)², kernel of the parity map), and the parity quotient ℤ/2ℤ of order 2. The parity quotient is the quotient of the full sign-flip group by its even subgroup and corresponds to U(1) weak hypercharge. The hypercharge layer is defined with fundamental representation dimension 1 and discrete order 2, matching the Weyl group of U(1).
proof idea
The proof is a one-line term-mode wrapper that applies reflexivity to the definitions of the parity quotient order and the fundamental representation dimension of the hypercharge layer.
why it matters
This theorem completes the identification of the third layer in the three-layer factorization of |B₃| = 48 = 6 × 4 × 2, confirming that the U(1) hypercharge arises directly as the parity quotient of the sign-flip group. It supports the module claim that the full gauge group structure is forced by the geometry of the 3-cube. The result closes the discrete-order accounting for the U(1) factor after the SU(3) and SU(2) layers have been assigned.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.