cube_order_factors_as_completion
plain-language theorem explainer
The hyperoctahedral group B₃ (signed permutations of three axes) has order 48, factoring as 6 × 4 × 2. Anyone citing the cube-to-compact-gauge bridge uses this identity as the discrete skeleton of the three Standard Model compact factors. The proof is a one-line wrapper of the three-layer factorization already established in GaugeFromCube.
Claim. The order of the signed-permutation group on three coordinates equals the product of the axis-permutation count $3!$, the even sign-flip subgroup order $2^{3-1}$, and the parity-quotient order $2$: $|B_3| = 6 \times 4 \times 2$.
background
The ambient module records the first bridge from the forced 3-cube automorphism skeleton to the Standard Model compact gauge factors. A signed permutation on $D$ coordinates is a pair (permutation of axes, sign pattern in ${\pm 1}^D$); for $D=3$ this is the hyperoctahedral group $B_3$, the full automorphism group of the cube.
Upstream, GaugeFromCube splits $|B_3|$ into three layers: axis permutations of order $D!=6$, the even sign-flip subgroup of order $2^{D-1}=4$, and the parity quotient $\mathbb{Z}/2\mathbb{Z}$ of order $2$. The three-layer factorization theorem states exactly $48=6\times 4\times 2$, with each factor tied to one gauge layer.
The module keeps recognition-axis counts $(3,2,1)$ (total 6) separate from Lie ranks $(2,1,1)$ (total 4). The present identity is the discrete order statement that the completion rule later maps toward $\mathrm{SU}(3)\times\mathrm{SU}(2)\times\mathrm{U}(1)$.
proof idea
One-line wrapper: exact three_layer_factorization. That upstream theorem rewrites the card of SignedPerm 3 via the cube automorphism order and discharges the numeric identity $48=6\times 4\times 2$ by native_decide. No new algebra is introduced here; the declaration only re-exports the factorization under the completion-module name.
why it matters
This is the order-level anchor for P0-S2-01 (gauge Lie completion from the cube). Downstream it is recorded inside gaugeLieCompletionCert, the certificate packing factor count, recognition-axis counts, and Lie ranks for the compact-completion rule $3\mapsto\mathrm{SU}(3)$, $2\mapsto\mathrm{SU}(2)$, $1\mapsto\mathrm{U}(1)$.
In the forcing chain the ambient dimension is already fixed at $D=3$ (T8), so $B_3$ is the unique cube automorphism group in play. The factorization supplies the discrete skeleton those compact factors complete; it does not yet derive hypercharge embeddings or fermion representations. It is the clean handoff from cube layer counts to the SM compact-factor skeleton.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.