Pith. sign in
module module high

IndisputableMonolith.Mathematics.ConwayGroupStructuralFromRS

show as:
view Lean formalization →

The module derives the Leech lattice dimension and Conway group structural factorizations from Recognition Science constants. Group theorists studying sporadic groups cite it for the RS-native account of the 24-dimensional Leech lattice via the eight-tick octave. It consists of definitions and equalities establishing factorizations such as 24 = 2³ · 3.

claimThe Leech lattice dimension satisfies $24 = 2^{3} \cdot 3$, with related Conway group order factorizations and certificates derived from RS constants in the forcing chain.

background

Recognition Science derives all physics from one functional equation, with the forcing chain (T0 to T8) yielding T7 (eight-tick octave, period 2³) and T8 (D = 3). This module imports the fundamental RS time quantum τ₀ = 1 tick from Constants. It introduces sibling definitions for leechDimension, b3Order, leechFromCube, leech_half_b3, ConwayCert and related equalities that link these to the Leech lattice and Conway group.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the group-theoretic structures for the Conway group and Leech lattice that connect the unified forcing chain (T7 eight-tick octave, T8 D=3) to sporadic mathematics in Recognition Science. It fills the integer factorization step highlighted in the module doc-comment and supports potential downstream theorems on ConwayCert, though no used_by edges are currently recorded.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)