Mathematics Conway Group Structural From Rs

The Conway group's structural facts

The Conway group Co₁ is one of the 26 sporadic simple groups, the exceptional building blocks of finite group theory. Its most famous object is the Leech lattice, a highly symmetric 24-dimensional packing of points discovered by John Leech in 1967 and studied intensively by John Conway, who determined its automorphism group in 1969. That automorphism group is Co₀, and Co₁ is the quotient of Co₀ by its two-element center, so the order of Co₀ is exactly twice the order of Co₁. The Leech lattice itself has dimension 24, a number that also appears as 2³ · 3, the half of 48, the order of the three-dimensional hyperoctahedral group B₃.

These are not deep theorems but exact integer identities: 24 = 2³ · 3, and 24 = 48/2. They are the kind of arithmetic facts that appear throughout sporadic group theory, where small numbers carry structural weight. The dimension 24 is what makes the Leech lattice special: it is the largest dimension in which a lattice can have the particularly dense and symmetric structure that the Conway groups exploit. The factorisation 2³ · 3 connects the dimension to the cube, and the half-of-48 identity ties it to the symmetry group of the cube, a classical object from three-dimensional geometry.

In Recognition Science, the framework's machine-checked library of formal theorems records these identities as certified facts. The library defines the Leech lattice dimension as 24, the order of B₃ as 48, and the half-of-B₃ value as 24, then proves by direct computation that the two expressions for 24 agree. The result is a small certificate, a structure called ConwayCert, that bundles the three identities together: the dimension equals 24, the half-of-B₃ equals the dimension, and the factorisation holds. The certificate is built from proofs that require no axioms beyond the standard logical foundations and no unproved assumptions.

What this establishes in plain language is that certain structural facts about the Conway group and the Leech lattice are not taken on faith. They are checked by a computer-verified proof system, down to the arithmetic. The dimension of the Leech lattice, its factorisation, and its relation to the cube group are all recorded as formal theorems. This matters because sporadic group theory is a field where a single wrong integer can invalidate a classification argument; having these identities machine-checked gives the framework's wider work a solid arithmetic foundation.

The practical consequence is that when the framework builds on the Conway group, it does so on verified ground. A reader who wants to check the claim that the Leech lattice is 24-dimensional, or that 24 is half of 48, can trace it to a formal proof rather than a textbook assertion. The certificate is a small but real example of the framework's method: take a mathematical fact, express it exactly, and prove it with no gaps.

theorem leechDimension_eq : leechDimension = 24 := rfl

/-- 24 = 2³ · 3 (integer factorisation). -/
theorem leechDim_factorisation : leechDimension = 2 ^ 3 * 3 := by decide

theorem leech_half_b3 : leechFromCube = leechDimension := by decide

structure ConwayCert where
  leech_dim : leechDimension = 24
  leech_half_b3 : leechFromCube = leechDimension
  leech_factorisation : leechDimension = 2 ^ 3 * 3

What this page does not claim

The module does not prove that Co₁ is simple or that it is the automorphism group of the Leech lattice. The module does not derive the Leech lattice's existence or its uniqueness from the framework's axioms. The module does not connect the dimension 24 to the framework's three-dimensional spatial forcing.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Mathematics/ConwayGroupStructuralFromRS.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: