b3Order
plain-language theorem explainer
b3Order encodes the cardinality of the hyperoctahedral group B3 as 2^3 times 3 factorial. Researchers tracing symmetry groups in the Recognition Science lattice cite it to fix the order of the three-cube symmetry at 48. The definition is a direct arithmetic expression that downstream results evaluate by decision.
Claim. The order of the hyperoctahedral group $B_3$ is given by $|B_3| = 2^3 times 3!$.
background
The module states that the Recognition Science recognition lattice employs the three-dimensional cube $Q_3$, whose symmetry group is the hyperoctahedral group $B_3$. The order satisfies $|B_3| = 2^D times D!$ at spatial dimension $D=3$, yielding the explicit value 48. An upstream definition in ConwayGroupStructuralFromRS supplies the same quantity as the constant 48.
proof idea
The declaration is a one-line definition that directly encodes the formula $2^3 times 3!$. No lemmas or tactics appear inside the definition itself; the downstream theorem b3Order_eq_48 discharges equality to 48 by the decide tactic.
why it matters
This definition supplies the numeric anchor for b3Order_eq_48 and for the structure CubicSymmetryCert that records b3_order = 48 together with the rank decomposition. It realizes the framework step that spatial dimension equals 3, producing the order 48 that appears in the eight-tick octave and in the Conway-group structural results. The parent theorem in ConwayGroupStructuralFromRS provides the matching constant, closing the certification loop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.