lepton_rungs_forced
plain-language theorem explainer
The lepton rungs are forced to the values 2 for the electron, 13 for the muon, and 19 for the tau by the three-dimensional cubic geometry and the rung assignment rule. Researchers deriving lepton mass hierarchies from the Recognition Science chain would cite this result to fix the structural levels on the phi-ladder. The proof reduces the three equalities to the definitions of the rung function together with the explicit formulas for cube edges and cube faces.
Claim. In the Recognition Science model the rung numbers on the phi-ladder satisfy $r_e=2$, $r_μ=2+(3·2^{2}-1)$, and $r_τ=13+6$, placing the three lepton generations at structural levels 2, 13, and 19 that correspond to distinct residue classes modulo 8.
background
The module T10 establishes necessity for the lepton ladder once the electron mass is fixed by T9. The rung function assigns each fermion an integer level on the phi-ladder; cube_edges(d) counts the edges of the d-dimensional hypercube as d·2^(d-1) and cube_faces(d) counts the faces as 2d. For d=3 these yield the increments 11 and 6 that step from the base rung 2 to 13 and then to 19. The local setting replaces two earlier axioms for muon and tau mass bounds with these geometrically forced rung values, using the eight-tick octave and the cube geometry already derived in AlphaDerivation.
proof idea
The term proof splits the conjunction with constructor, discharges the electron equality by reflexivity, and simplifies the remaining two equalities by unfolding the definitions of rung, cube_edges, and cube_faces.
why it matters
This theorem supplies the rung assignments required by T10 to derive the muon and tau mass bounds from the electron rung and the cube-derived steps. It confirms that the three generations occupy the unique stable residue classes {2,5,3} modulo 8 inside the D=3 torsion constraint, closing the necessity half of the lepton-generations module and linking directly to the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.