leechFromCube
plain-language theorem explainer
This definition sets the Leech lattice dimension to half the order of the cubic symmetry group B3. Researchers linking sporadic groups to Recognition Science would cite it when establishing the 24-dimensional action of Co1. The definition is a direct arithmetic reduction from the upstream b3Order constant of 48.
Claim. The Leech dimension is defined as half the order of the cubic symmetry group B₃, i.e., $ |B_3| / 2 $, where this evaluates to 24.
background
The ConwayGroupStructuralFromRS module records integer identities for the Conway group Co₁ and its 24-dimensional action on the Leech lattice, including |Co₀| = 2 · |Co₁| and dim(Leech) = 24. The upstream b3Order is defined as 48 in this module and equivalently as 2³ · 3! in CubicSymmetryGroupFromRS, matching the order of the cubic symmetry group B₃. The local setting treats these as structural facts proved by decide, with zero axioms or sorrys.
proof idea
This is a one-line definition that applies division by 2 to the upstream b3Order constant.
why it matters
The definition supplies the integer 24 used in the ConwayCert structure and the leech_half_b3 theorem, which certify leechFromCube = leechDimension together with the factorisation 24 = 2³ · 3. It supports the module's structural facts for the Conway group Co₁ and its canonical action on the Leech lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.