conwayCert
plain-language theorem explainer
Assembles a ConwayCert record by supplying the Leech dimension equality to 24, the identification leechFromCube equals that dimension, and the factorization 24 equals 8 times 3. Sporadic group researchers in Recognition Science cite it to fix the integer skeleton of the Co₁ action on the Leech lattice. The definition is a direct structure literal that delegates each field to a prior reflexivity or decide lemma.
Claim. Define the Conway certificate as the record satisfying $d = 24$, $c = d$, and $d = 2^3 · 3$, where $d$ is the dimension of the Leech lattice and $c$ is the cube-derived quantity.
background
In the Recognition Science module on Conway group structure, the Conway group Co₁ is treated through its canonical 24-dimensional action on the Leech lattice. The module records three integer identities: the dimension equals 24, this dimension equals the cube-derived quantity, and 24 factors as 2³ · 3. These facts are presented as structural identities proved by reflexivity and decision procedures, with no axioms or sorry markers.
proof idea
The definition builds the ConwayCert record by assigning the dimension field to the reflexivity theorem leechDimension_eq, the half-B3 field to the decide theorem leech_half_b3, and the factorization field to the decide theorem leechDim_factorisation. It is a direct record construction with no further steps.
why it matters
This definition supplies the ConwayCert instance that packages the integer identities for the Leech lattice dimension required by the Conway group treatment. It directly implements the structural facts listed in the module documentation, including the decomposition 24 = 2³ · 3 that aligns with the eight-tick octave. No downstream theorems are recorded yet, so the certificate remains available for later sporadic-group arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.