Mathematics Conway Group Structural From Rs Leech Dim Factorisation

The Leech dimension identity

The Leech lattice is a 24-dimensional packing of points in space, famous in mathematics for its unusually dense sphere packing and its connection to sporadic simple groups. One of its key structural facts is that its dimension is 24. The declaration leechDim_factorisation records the elementary arithmetic identity that 24 equals 2 cubed times 3, or 2³ × 3.

This identity is proved by direct computation, a method mathematicians call decide, which verifies the equality by evaluating both sides. The machine-checked library of formal theorems confirms the statement with no gaps in reasoning and no additional assumptions. The same file also records that the order of the binary tetrahedral group is 48, and that half of 48 equals the Leech dimension, another way of seeing the 24.

In Recognition Science, this integer identity appears as a structural anchor. The framework models the Leech lattice as a 24-dimensional object, and the factorisation 2³ × 3 is part of a certificate that bundles several such facts together. The certificate, called ConwayCert, packages the dimension, the half-order relation, and the factorisation into a single unit that later sporadic-group work can reference.

What the declaration does not claim is more important than what it does. It does not prove that the Leech lattice exists, that it has the sphere-packing property, or that the Conway group Co₁ acts on it. Those are deeper facts from the mathematical literature. The declaration only certifies the arithmetic identity 24 = 2³ × 3, nothing more.

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

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

def b3Order : ℕ := 48

theorem leech_half_b3 : leechFromCube = leechDimension := by decide

What this page does not claim

This declaration does not prove the Leech lattice exists or has the sphere-packing property. It does not establish that the Conway group Co₁ acts on the lattice. It does not derive the dimension 24 from Recognition Science principles; it merely records the arithmetic identity.

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: