Pith. sign in
module module high

IndisputableMonolith.Physics.LeptonGenerations.Necessity

show as:
view Lean formalization →

The lepton ladder rungs {2, 13, 19} are the unique stable solutions of the three-generation torsion constraint in three spatial dimensions. Generation 1 sits at base rung 2 (from the electron link); generation 2 adds the passive energy step 11 to reach 13; generation 3 adds the six cube faces to reach 19. Residues modulo 8 are {2, 5, 3}, the three distinct cubic-voxel directions. Downstream hierarchy and T10 mass work cite this uniqueness package.

claimIn $D=3$, the only stable three-generation lepton ladder is the integer rung set $\{2,13,19\}$, built as base $2$ (electron link), then $2+E_p=2+11=13$, then $13+F=13+6=19$. These rungs lie in distinct residue classes $\{2,5,3\}\pmod{8}$, the three inequivalent directions of the cubic voxel under the torsion-minimality constraint.

background

Recognition Science places fermion masses on a $\varphi$-ladder whose integer rungs are fixed by cube geometry and the eight-tick octave (period $2^3$). The electron sector (T9) already forces the base rung $2$. This module extends that link to the full three-generation lepton ladder.

The generation steps are combinatorial, not free parameters: the passive energy offset $E_p=11$ and the six faces of the cube supply the increments $2\to 13\to 19$. Alpha-seed geometry ($4\pi\cdot 11$ from the cubic ledger) and $\varphi$-support identities sit upstream as numerical and algebraic infrastructure; interval power bounds certify the local inequalities used in torsion checks.

Stability means a torsion certificate on the ladder: residues modulo 8 must be pairwise distinct, matching the three inequivalent orientations of a cubic voxel. The sibling predicate is_stable_lepton_ladder packages that constraint; uniqueness is the claim that only ${2,13,19}$ satisfies it among admissible integer ladders.

proof idea

The module is a necessity package, not a single one-liner. Exact identities pin the geometric constants ($E_p=11$, cube faces $=6$, and the related $W$ factor). Local interval comparisons bound $\pi$ against the $d_6$ scale where needed for torsion numerics.

A torsion certificate is assembled and verified for the candidate ladder. Residues of $2,13,19$ modulo 8 are shown pairwise distinct. Minimality of torsion then forces any stable three-generation ladder to match this rung set, yielding uniqueness (lepton_rungs_forced / lepton_rungs_unique). Electron-mass necessity supplies the base rung; definitions from the lepton-generations layer fix the ladder type.

why it matters in Recognition Science

Without forced rungs, muon and tau masses on the $\varphi$-ladder remain optional insertions. This module closes that gap for the lepton sector: the three-generation torsion constraint in $D=3$ admits only ${2,13,19}$.

It is imported by the T10 lepton-generations layer, which extends the electron ladder to muon and tau masses, and by the unified generation hierarchy that aligns discrete ladder positions across fermion sectors. The hierarchy note is careful: quark quarter-ladder steps live in a separate hypothesis lane; the integer-rung lepton core here is the parameter-free piece.

Framework landmarks in play are T8 ($D=3$), the eight-tick octave (residues mod 8), and the cube-combinatorial seed structure behind $E_p=11$ and the six faces. The result is the structural backbone for citing three-and-only-three charged-lepton generations on the RS ladder.

scope and limits

used by (2)

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