m_tau_rs
plain-language theorem explainer
m_tau_rs defines the tau lepton mass in RS units as E_coh times phi to the 19th power. Researchers deriving lepton mass hierarchies from the phi-ladder cite it when establishing ratios such as m_tau over m_e. It is a direct one-line instantiation of the mass_on_rung definition at rung 19.
Claim. The tau lepton mass in RS units is $m_τ = E_{coh} ⋅ φ^{19}$, where $E_{coh}$ denotes the coherence energy scale and $φ$ is the golden-ratio fixed point from the forcing chain.
background
The LeptonMassLadder module formalizes P-011 on lepton masses, stating that m_e scales as φ², m_μ as φ¹³, and m_τ as φ¹⁹ in E_coh units, with ratios fixed by rung spacings of 11 and 17. The upstream mass_on_rung definition supplies the general expression: mass in RS units equals Anchor.E_coh multiplied by phi raised to rung r. This rests on the phi-ladder construction in MassHierarchy and the constants imported from PhiForcing.
proof idea
One-line definition that applies mass_on_rung to the integer argument 19.
why it matters
This supplies the explicit tau mass required by the downstream theorem lepton_masses_from_ladder, which resolves P-011 by proving the ratios m_μ/m_e = φ¹¹, m_τ/m_e = φ¹⁷, and m_τ/m_μ = φ⁶. It implements the RS mass formula on the phi-ladder and feeds the positivity and ratio lemmas that follow. The construction aligns with the self-similar fixed point and eight-tick octave of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.