r_lepton_values
plain-language theorem explainer
The theorem fixes the lepton rung integers at 2 for the electron, 13 for the muon and 19 for the tau on the Recognition Science phi-ladder. Mass hierarchy and electron-mass derivations cite these fixed values to locate each generation. The proof is a direct term-mode simplification that unfolds r_lepton against the cube-edge, passive-field and wallpaper constants then reduces the arithmetic.
Claim. The lepton rung function satisfies $r(e)=2$, $r(mu)=13$ and $r(tau)=19$, where the arguments label the three charged-lepton generations.
background
The Masses.Anchor module centralises parameter-free constants derived from D=3 cube geometry. Total edges equal cube_edges(3)=12, passive field edges equal 11, the active edge per tick equals 1, and the wallpaper-group count equals 17. These numbers enter the sector formulas for B_pow and r0 that locate every species on the phi-ladder; r_lepton simply returns the pre-computed rung integers for each lepton label.
proof idea
The proof is a term-mode simplification. It unfolds r_lepton together with the constants tau, E_passive, W, passive_field_edges, cube_edges, active_edges_per_tick, D and wallpaper_groups, then applies norm_num to finish the arithmetic reduction.
why it matters
The result supplies the rung values required by the mass-hierarchy theorems. It is cited directly by r_electron, r_muon and r_tau in MassHierarchy and by m_e_rs_eq in ElectronMass. The increments 2, 2+11 and 2+17 encode the geometric structure of the D=3 cube and the crystallographic constant 17 that appear throughout the Recognition forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.