leech_half_b3
plain-language theorem explainer
Equality between the halved b3Order and the Leech lattice dimension holds by direct numerical check. Researchers embedding sporadic groups into Recognition Science cite it to confirm that the 24-dimensional Leech lattice matches the factorisation 24 = 2³ · 3. The proof is a one-line decision procedure that verifies the two natural-number definitions coincide.
Claim. $|B_3|/2 = 24$, where $|B_3|$ denotes b3Order and the right-hand side is the Leech lattice dimension.
background
The module fixes the Leech lattice dimension at 24 via the definition leechDimension := 24 and introduces leechFromCube := b3Order / 2 to encode the identity 24 = 2³ · 3 = |B₃|/2. These integer relations sit alongside |Co₀| = 2 · |Co₁| and support structural facts about the Conway group Co₁ and its 24-dimensional action on the Leech lattice. The upstream definitions leechDimension and leechFromCube supply the two constants whose equality is asserted.
proof idea
The proof is a one-line wrapper that applies the decide tactic directly to the equality leechFromCube = leechDimension. The tactic exhaustively checks the natural-number identity arising from the constant definitions without invoking further lemmas.
why it matters
The theorem supplies the leech_half_b3 field required by the ConwayCert structure, which is instantiated by conwayCert together with the Leech dimension equality and the factorisation leechDimension = 2^3 * 3. It thereby completes the integer scaffolding for Conway-group constructions inside Recognition Science, anchoring the 24-dimensional Leech lattice to the b3 factorisation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.