r_lepton
plain-language theorem explainer
Rung integers for charged leptons are supplied as 2 for the electron, 13 for the muon and 19 for the tau. Mass calculations in RS units cite this when placing fermions on the phi-ladder. Researchers computing lepton masses or dissolving the hierarchy problem cite the values directly. It is realized as a one-line alias to the underlying Integers definition.
Claim. The lepton rung function maps lepton names to integers on the phi-ladder: $r(e)=2$, $r(mu)=13$, $r(tau)=19$.
background
In the Anchor module the lepton rung function is defined by adding increments generated by the tau function to the baseline rung 2. The tau increments (11 for the first, 17 for the second) arise from the passive-field edges of the eight-tick octave. AnchorPolicy re-exports this function so that sector-aware policies can retrieve lepton rungs without explicit pattern matching on Sector.Lepton.
proof idea
One-line alias that re-exports the lepton rung definition from the Anchor module.
why it matters
The definition supplies the lepton rungs used in electron mass computation m_e_rs = E_coh * phi^2 and in the geometric hierarchy theorem that shows the muon-to-electron ratio equals phi^11. It supports dissolution of the hierarchy problem by fixing mass ratios to powers of phi. The values tie directly to the T5 J-uniqueness and T7 eight-tick structure that generate the tau increments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.