signed_perm_card
plain-language theorem explainer
The order of the hyperoctahedral group B_D equals 2^D D!. Gauge theorists extracting the Standard Model from cube symmetries cite this when fixing |Aut(Q_3)|. The proof reduces the count to the product of a permutation group and a sign map via Fintype equivalences and standard cardinality simplifications.
Claim. The cardinality of the hyperoctahedral group $B_D$ realized by signed permutations on $D$ coordinates satisfies $|B_D| = 2^D D!$.
background
In module P-014 the structure SignedPerm D encodes the hyperoctahedral group B_D: each element consists of a permutation of Fin D together with an independent sign assignment in Fin 2 for each coordinate. This group acts on Z^D by signed coordinate changes and is the automorphism group of the D-cube. The module extends earlier results on three particle generations and three quark colors from the face-pairs of Q_3 to the full gauge group SU(3) x SU(2) x U(1) via the decomposition of B_3 into S_3 and (Z/2Z)^2 layers.
proof idea
The term proof invokes Fintype.ofEquiv_card on the equivalence of SignedPerm D to Equiv.Perm (Fin D) times (Fin D to Fin 2). It then applies Fintype.card_prod, Fintype.card_perm, Fintype.card_fun and Fintype.card_fin, followed by ring to reach the closed expression 2^D * D!.
why it matters
cube_aut_order invokes this result to obtain |Aut(Q_3)| = 48. The cardinality supplies the concrete size needed for the three-layer decomposition in the module: axis permutations S_3 yield the SU(3) factor while even sign flips yield the SU(2) x U(1) factor. This step aligns with the Recognition Science derivation of D = 3 from the eight-tick octave and completes the gauge content forced by Q_3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.