three_layer_factorization
plain-language theorem explainer
The hyperoctahedral group B_3 of order 48 on three coordinates factors as the product of axis permutations of order 6, the even sign-flip subgroup of order 4, and the parity quotient of order 2. Researchers deriving the Standard Model gauge factors from cube symmetry would cite this when mapping the layers to SU(3), SU(2) x U(1), and U(1). The proof reduces the equality to the known cardinality 48 and confirms the arithmetic by decision procedure.
Claim. $|B_3| = 3! × 2^{2} × 2$, where $B_3$ is the hyperoctahedral group of signed permutations on three coordinates, $3!$ counts axis permutations, $2^{2}$ counts even sign flips, and the final factor 2 is the parity quotient order.
background
The module derives the Standard Model gauge group SU(3) × SU(2) × U(1) from the automorphism group of the 3-cube Q_3. SignedPerm D is the structure whose elements are permutations of Fin D together with sign assignments in Fin 2; its cardinality is the order of the hyperoctahedral group B_D. The upstream theorem cube_aut_order states that Fintype.card (SignedPerm 3) = 48. The sibling definition axis_perm_count D returns Nat.factorial D, while even_sign_flip_count D returns 2^(D-1). The module document decomposes B_3 = (Z/2Z)^3 ⋊ S_3 into three layers, with the even-sign-flip kernel of the parity map supplying the middle factor of 4.
proof idea
The proof rewrites the left-hand side via the theorem cube_aut_order to obtain the literal equality 48 = axis_perm_count 3 * even_sign_flip_count 3 * parity_quotient_order, then applies native_decide to discharge the numerical check.
why it matters
This result supplies the explicit three-layer order factorization required by the module's derivation of the gauge group from cube symmetry. It rests on the prior cardinality theorem cube_aut_order and the layer-count definitions, completing the combinatorial step that assigns S_3 to the SU(3) color factor, (Z/2Z)^2 to the SU(2) × U(1) structure, and the remaining Z/2Z to U(1). In the Recognition Science setting it furnishes the discrete symmetry origin for the gauge factors inside the forcing chain that produces D = 3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.