three_layer_factorization
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 in Recognition Science
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.
scope and limits
- Does not construct explicit homomorphisms from the layers to SU(3), SU(2), or U(1).
- Does not extend the factorization to dimensions other than 3.
- Does not derive dynamical consequences or particle masses from the factorization.
- Does not relate the orders to Recognition Science constants such as phi or alpha.
formal statement (Lean)
216theorem three_layer_factorization :
217 Fintype.card (SignedPerm 3) =
218 axis_perm_count 3 * even_sign_flip_count 3 * parity_quotient_order := by
proof body
Term-mode proof.
219 rw [cube_aut_order]
220 native_decide
221
222/-- The factorization in terms of the Standard Model structure. -/