hyperoctahedral_D3
plain-language theorem explainer
The order of the hyperoctahedral group B_3 equals 48. Researchers confirming the symmetry of the Recognition Science 3-cube lattice would cite this when assembling the cubic symmetry certificate. The proof is a one-line decision procedure that evaluates the order formula at dimension 3.
Claim. The order of the hyperoctahedral group $B_3$ is 48, i.e., $2^3 times 3! = 48$.
background
The Recognition Science lattice is built on the 3-cube $Q_3$ whose symmetry group is the hyperoctahedral group $B_3$. The module defines the order via the closed formula $2^D times D!$. The rank function from PreTemporalForcingOrder assigns integer priorities to forcing stages (distinction at 0, recognition interface at 1, up to composition consistency at 4). A parallel rank definition in OrderPreservation counts states with strictly lower J-cost, preserving order under monotone maps.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the definition hyperoctahedralOrder 3, which expands to $2^3 times 3!$ and evaluates directly to 48.
why it matters
This supplies the concrete order 48 required by the downstream cubicSymmetryCert, which packages b3Order_eq_48, the hyperoctahedral property, and rank_sum into a single certificate. It realizes the D=3 case of the forcing chain (T8) and the eight-tick octave structure of the RS lattice. The result closes the computational step for the cube symmetry group without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.