pith. sign in
module module high

IndisputableMonolith.Physics.LeptonGenerations.Necessity

show as:
view Lean formalization →

The Necessity module proves the lepton ladder rungs at 2, 13 and 19 are the unique stable solutions to the three-generation torsion constraint in D=3. Researchers deriving Standard Model spectra from first principles cite it to extend the T9 electron mass to muon and tau via the phi-ladder. The argument composes the base rung with the E-passive increment of 11 and the cube-face increment of 6, confirming uniqueness through residue classes modulo 8.

claimThe unique stable solutions to the three-generation torsion constraint in $D=3$ are the lepton rungs $r_1=2$, $r_2=13$, $r_3=19$, corresponding to the residue classes $\{2,5,3\} \pmod{8}$ that label the three distinct directions of the cubic voxel.

background

This module belongs to the lepton sector of Recognition Science, which derives all constants from the J-functional equation and the phi-ladder after the T0-T8 forcing chain fixes $D=3$ and the eight-tick octave. It imports the electron mass definitions (T9) that place the base rung at 2 and the lepton generation definitions that encode the torsion constraint. Upstream, AlphaDerivation supplies the 4π factor from Gauss-Bonnet on the cubic vertex deficits, while PhiSupport encodes the relation $\phi^2=\phi+1$.

proof idea

The module organises its argument by first fixing the electron base rung from ElectronMass.Necessity, then applying the forced E-passive step of 11 and the cube-face step of 6 derived from cubic geometry. Uniqueness follows from verifying that the resulting residues modulo 8 are distinct and exhaust the three independent directions of the voxel; torsion minimality is checked via the sibling declarations lepton_rungs_unique and torsion_minimality_forced.

why it matters in Recognition Science

The module supplies the rung positions required by the T10 lepton generations module and the unified hierarchy in Physics.Hierarchy. It closes the parameter-free chain from the cubic ledger to the three lepton masses, consistent with the alpha band and the RS-native constants $c=1$, $\hbar=\phi^{-5}$. Downstream ParticleSummary and RRF.Physics.LeptonGenerations import these rungs to assemble the full fermion spectrum.

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