pith. sign in
module module high

IndisputableMonolith.Physics.LeptonGenerations.Necessity

show as:
view Lean formalization →

Module Necessity proves the lepton ladder positions 2, 13 and 19 are the unique stable solutions to the three-generation torsion constraint in D=3. Researchers deriving fermion spectra from Recognition Science cite it to fix the muon and tau rungs after the electron base. The argument chains the base rung from T9 electron necessity, then applies the E_p increment of 11 and the six cube-face steps.

claimThe rung positions $r_1=2$, $r_2=13$, $r_3=19$ are the unique stable solutions of the three-generation torsion constraint in three spatial dimensions, with residues $\{2,5,3\}$ modulo 8.

background

The module extends the T9 electron mass definitions and sits inside the lepton sector of Recognition Science. It imports the RS time quantum, the alpha derivation from cubic ledger geometry via Gauss-Bonnet, phi-support identities, and the electron mass necessity module. The local setting assumes the forcing chain through T8 (D=3) together with the Recognition Composition Law and the phi-ladder mass formula.

Upstream results supply the structural 4π derivation and interval bounds on powers. The doc-comment states the rungs correspond to the three unique directions of the cubic voxel.

proof idea

The module assembles necessity lemmas that first fix the base rung at 2 via the T9 electron link, then add the E_p step of 11 and the six cube-face increments. Uniqueness follows from residue-class distinctness modulo 8 and torsion-minimality constraints already established in the electron mass necessity module.

why it matters in Recognition Science

This module supplies the rung positions required by the unified generation hierarchy and by the T10 lepton generations formalization. It closes the parameter-free derivation of the three lepton masses from cube geometry and feeds directly into the particle summary. The doc-comment identifies the result as the T10 step after T9 electron linking.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.

declarations in this module (110)

… and 30 more