lepton_rungs_unique
plain-language theorem explainer
The theorem states that the only integers satisfying the torsion-stable lepton ladder condition are the rungs 2, 13 and 19. Physicists deriving muon and tau mass bounds from the electron mass in Recognition Science cite this to fix the generational steps. The proof is a direct biconditional: one direction unfolds the stability predicate and extracts the values via simplification on cube edge and face counts plus linear arithmetic; the converse substitutes the triple and verifies the geometric steps by normalization.
Claim. For all integers $r_1,r_2,r_3$, the lepton ladder with rungs $r_1,r_2,r_3$ is torsion-stable if and only if $r_1=2$, $r_2=13$ and $r_3=19$.
background
The lepton ladder is the sequence of three rungs that locate the electron, muon and tau structural masses on the phi-ladder. Torsion stability requires the rung differences to satisfy two step conditions built from the 3-cube geometry: cube_edges counts the edges of the D-hypercube as $D·2^{D-1}$ and cube_faces counts the faces as $2D$. For $D=3$ these evaluate to 12 and 6 respectively and enter the step functions together with the fine-structure constant and the golden ratio fixed at T6. This declaration belongs to the T10 necessity module, whose goal is to replace the two lepton-mass axioms of the parent LeptonGenerations file with inequalities forced from the T9 electron mass and the eight-tick octave.
proof idea
The term-mode proof splits into the two directions of the biconditional. Forward: unfold the stability predicate, simplify the two step hypotheses with the definitions of cube_edges and cube_faces, then apply linarith to recover the three rung equalities. Reverse: substitute the concrete values 2, 13, 19, then construct the six conjuncts of the predicate; the first three are settled by norm_num (distinctness mod 8) and the last two by simp on cube_edges and cube_faces.
why it matters
The result supplies the uniqueness half of the lepton torsion certificate, which is the immediate parent theorem lepton_torsion_verified. It thereby completes one of the two replacements required by the T10 module: once uniqueness is established, the observed rung triple can be inserted into the mass formula yardstick·phi^(rung-8+gap(Z)) to produce the muon and tau predictions without additional axioms. The argument rests on the D=3 geometry fixed at T8 and the phi-ladder lattice structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.