b3Order
plain-language theorem explainer
The definition assigns the integer 48 to the order of the B₃ cubic symmetry group. Researchers working on sporadic groups and Leech lattice constructions in Recognition Science cite this value to relate cubic symmetries to 24-dimensional structures. It is introduced as a direct constant assignment that matches the upstream computation 2³ × 3!.
Claim. The order of the B₃ symmetry group is 48.
background
The ConwayGroupStructuralFromRS module develops integer identities linking the Conway group Co₁ to the Leech lattice in 24 dimensions. It records the relation 24 = 2³ · 3 = |B₃|/2 together with |Co₀| = 2 · |Co₁|. The local setting treats these as structural facts proved by decide, with no axioms or sorrys. The upstream definition in CubicSymmetryGroupFromRS supplies b3Order := 2³ × 3!, which is then shown equal to 48 by a decide tactic.
proof idea
This is a direct definition that sets the constant to the literal 48. It aligns with the algebraic expansion 2³ × 3! already computed in the cubic symmetry module and confirmed by the theorem b3Order_eq_48.
why it matters
The definition supplies the integer 48 required by leechFromCube to obtain the Leech dimension 24 via division by 2. It supports the module's identities for Co₀, Co₁ and the 24-dimensional Leech lattice, consistent with the forcing-chain result that spatial dimension D equals 3. The value also appears inside the CubicSymmetryCert structure that certifies hyperoctahedral order and rank decomposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.