cube_aut_order
plain-language theorem explainer
The automorphism group of the 3-cube equals the hyperoctahedral group B_3 of order 48. Researchers deriving Standard Model gauge factors from cube symmetries cite this cardinality. The proof reduces the claim via rewrite to the signed-permutation cardinality lemma and evaluates the resulting numeral.
Claim. The cardinality of the hyperoctahedral group $B_3$ satisfies $|B_3| = 48$, where $B_3$ consists of all signed permutations of three coordinates acting on $Z^3$ by $x_imapsto epsilon_i x_{sigma(i)}$.
background
The module derives the Standard Model gauge group SU(3) x SU(2) x U(1) from the automorphism group of the 3-cube Q_3. SignedPerm D is the structure whose elements are a permutation of Fin D together with a sign map Fin D to Fin 2; it realizes the hyperoctahedral group B_D acting on Z^D by independent axis permutations and sign flips. The module decomposes B_3 into three layers whose orders multiply to 48 and map to the gauge ranks (3,2,1).
proof idea
The term proof rewrites the target with the signed_perm_card lemma, which supplies the general formula for the cardinality of SignedPerm D, then applies norm_num to confirm the concrete value 48.
why it matters
This cardinality supplies the total order used by gauge_group_certificate, gauge_order_product, and three_layer_factorization. It confirms the factorization 48 = 6 x 4 x 2 that assigns the S_3 layer to SU(3) color, the even-sign-flip subgroup to SU(2) x U(1), and closes the order step of P-014.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.