b3Order_eq_48
plain-language theorem explainer
The order of the hyperoctahedral group B₃ equals 48. Researchers modeling the 3-cube symmetry in the Recognition Science lattice cite this to fix the group cardinality. The proof is a one-line decision procedure that evaluates the expression 2³ times 3 factorial directly.
Claim. The order of the hyperoctahedral group $B_3$ of the 3-cube satisfies $|B_3| = 48$.
background
The module derives the cubic symmetry group from Recognition Science applied to the 3-cube Q₃. The hyperoctahedral group B₃ is defined as the symmetry group of this cube, with order given by the formula 2^D times D factorial at D=3. An upstream definition in ConwayGroupStructuralFromRS sets the order directly to 48, while the local definition in this module uses the explicit factorial expression.
proof idea
The proof applies the decide tactic to evaluate the arithmetic equality 2^3 * Nat.factorial 3 = 48 directly.
why it matters
This theorem supplies the b3_order field inside the cubicSymmetryCert definition that certifies symmetry properties for the RS recognition lattice. It aligns with the framework landmark T8 that forces D=3 spatial dimensions and yields the eight-tick octave order 48. The result closes the cardinality computation for B₃ before the full certification is assembled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.