sm_factorization
plain-language theorem explainer
The hyperoctahedral group B₃ of order 48 factors as 6 × 4 × 2, matching the layer orders S₃ for SU(3), (ℤ/2ℤ)² for SU(2), and ℤ/2ℤ for U(1) in the cube-derived gauge structure. Researchers tracing geometric origins of the Standard Model gauge group would cite this identity. The proof reduces directly to numerical normalization of the product.
Claim. The order of the automorphism group of the 3-cube equals 48 and factors as $6 × 4 × 2$, where 6 is the order of the axis-permutation subgroup $S_3$, 4 is the order of the even-sign-flip subgroup isomorphic to $(ℤ/2ℤ)^2$, and 2 accounts for the remaining parity factor in the decomposition that yields the gauge group $SU(3) × SU(2) × U(1)$.
background
The module derives the full Standard Model gauge group $SU(3) × SU(2) × U(1)$ from the automorphism group B₃ of the 3-cube Q₃. This group decomposes as $(ℤ/2ℤ)^3 ⋊ S_3$ with total order 48. The three layers are axis permutations (S₃, order 6) mapping to SU(3) color, even sign flips ((ℤ/2ℤ)², order 4) mapping to SU(2) × U(1), and the residual parity factor of 2. The gauge rank is defined as the number of independent generators for each Lie group factor, with fundamental representation dimensions supplied by the cube layers (3 for SU(3), 2 for SU(2), 1 for U(1)). Upstream structures such as the J-cost calibration in PhiForcingDerived and the ledger factorization supply the Recognition Science units and forcing order used to embed this symmetry into the broader framework.
proof idea
The proof is a one-line wrapper that applies the norm_num tactic to verify the arithmetic identity 48 = 6 × 4 × 2 by direct computation.
why it matters
This identity supplies the numerical backbone for the gauge-rank correspondence in the cube symmetry derivation of SU(3) × SU(2) × U(1). It completes the layer accounting begun in the module's Part 5 section on gauge rank, where S₃ supplies the rank-2 structure for SU(3) and (ℤ/2ℤ)² supplies the rank-1 structure for SU(2) × U(1). The result sits inside the T0–T8 forcing chain by fixing the discrete symmetry that forces D = 3 spatial dimensions and the eight-tick octave. No open scaffolding remains for this arithmetic step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.