pith. sign in
module module moderate

IndisputableMonolith.Mathematics.ConwayGroupStructuralFromRS

show as:
view Lean formalization →

The module derives Leech lattice dimension and Conway group structural properties from Recognition Science constants. Researchers connecting sporadic groups to fundamental physics would cite it. Content consists of definitions and equalities obtained via integer factorizations tied to the RS time quantum.

claimThe Leech lattice dimension satisfies $\dim(\Lambda_{24}) = 24 = 2^3 \cdot 3$.

background

The module imports Mathlib and Constants, where the latter defines the fundamental RS time quantum $\tau_0 = 1$ tick. It introduces sibling objects including leechDimension, b3Order, leechFromCube, and ConwayCert, all operating inside the Recognition Science framework that uses the phi-ladder and eight-tick octave.

proof idea

This is a definition module whose equalities are obtained by direct algebraic reduction from the imported RS time quantum; no multi-step tactic sequences appear.

why it matters in Recognition Science

The module supplies the 24-dimensional factorization that links Recognition Science to the Conway group and Leech lattice. It fills the structural step connecting T7 (eight-tick octave) to sporadic group constructions, even though no downstream uses are recorded.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)