leechDimension
plain-language theorem explainer
The declaration defines the Leech lattice dimension as the natural number 24. Researchers working on sporadic groups in Recognition Science cite this constant when verifying the Conway group Co₁ action on the lattice. It is supplied as a direct definition with no computation or proof obligations.
Claim. The dimension of the Leech lattice is defined to be the natural number $24$.
background
The module records structural integer facts for the Conway group Co₁, which admits a canonical 24-dimensional action on the Leech lattice. The documentation lists the identities |Co₀| = 2 · |Co₁|, 24 = 2³ · 3 = |B₃|/2, and dim(Leech) = 24 as basic facts for RS sporadic-group work. These identities are treated as direct integer relations established by computation.
proof idea
The declaration is a direct definition that assigns the constant value 24 to the Leech dimension in the natural numbers.
why it matters
This definition supplies the dimension value required by the ConwayCert structure and the theorems leechDimension_eq, leechDim_factorisation, and leech_half_b3. It anchors the integer identity dim(Leech) = 24 listed in the module documentation. In the Recognition Science framework it provides the 24-dimensional input for Conway group constructions that sit alongside the forcing chain T0-T8 and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.