leechDimension_eq
plain-language theorem explainer
The equality leechDimension = 24 is established by reflexivity on its definition. Researchers working on sporadic groups in Recognition Science cite it to anchor the 24-dimensional Leech lattice representation for the Conway group Co₁. The proof is a one-line reflexivity that matches the constant definition directly.
Claim. The dimension of the Leech lattice equals 24.
background
In the ConwayGroupStructuralFromRS module the Conway group Co₁ has a canonical 24-dimensional action on the Leech lattice. The sibling definition leechDimension sets this dimension to the natural number 24. The module lists this as one of the structural integer identities used throughout RS sporadic-group work, alongside |Co₀| = 2 · |Co₁| and 24 = 2³ · 3 = |B₃|/2, all proved by decide.
proof idea
The proof is a one-line reflexivity that applies the definition leechDimension := 24 directly to the right-hand side.
why it matters
This equality supplies the leech_dim field inside the conwayCert certificate. It confirms the framework fact that dim(Leech) = 24, one of the integer identities listed in the module for closing the structural description of the Conway group. The module treats these identities as proved by decide, completing the integer scaffolding for RS sporadic-group constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.