hyperoctahedralOrder
plain-language theorem explainer
The hyperoctahedralOrder definition supplies the order of the D-dimensional hyperoctahedral group B_D as 2^D times D factorial. Recognition Science researchers working on the 3-cube lattice cite this when confirming the symmetry group order equals 48 at D=3. The definition is a direct arithmetic formula that evaluates without lemmas or external results.
Claim. The order of the hyperoctahedral group satisfies $|B_D| = 2^D D!$.
background
The module treats the 3-cube Q_3 as the fundamental recognition lattice object in Recognition Science. Its symmetry group is the hyperoctahedral group B_3 whose order is 48. The supplied definition gives the general expression 2^D D! that specializes at D=3 to the required count 8 times 6.
proof idea
One-line definition that directly encodes the standard combinatorial formula for the order of B_D.
why it matters
The definition is referenced by CubicSymmetryCert to certify hyperoctahedralOrder 3 = 48 and by the hyperoctahedral_D3 theorem. It supplies the concrete group order needed for the cubic symmetry facts in the RS lattice, consistent with D=3 from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.