leechDim_factorisation
plain-language theorem explainer
The Leech lattice dimension of 24 factors as eight times three. Researchers constructing the Conway group certificate in Recognition Science cite this identity to assemble structural facts for the 24-dimensional action. The proof is a direct arithmetic verification that succeeds by computation.
Claim. The Leech lattice dimension equals $2^3 · 3$.
background
The ConwayGroupStructuralFromRS module assembles integer identities for the Conway group Co₁ and its canonical action on the Leech lattice. The upstream definition sets the Leech dimension to the constant 24. Module documentation records the relations 24 = 2³ · 3 and 24 = |B₃|/2 as structural facts required for sporadic-group work.
proof idea
The proof is a one-line wrapper that applies the decide tactic to confirm the numerical equality 24 = 8 · 3.
why it matters
This factorization is bundled into the conwayCert definition alongside the Leech dimension equality and the half-B3 relation. It supplies one of the integer identities that certify the Conway group structure in Recognition Science, supporting the 24-dimensional representation of Co₁.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.