tau_electron_ratio
plain-language theorem explainer
The ratio of the tau lepton mass to the electron mass in RS units equals phi to the seventeenth power. Researchers assembling lepton mass hierarchies from the phi-ladder cite this when confirming the full set of ratios for muons and taus. The proof is a direct algebraic reduction that unfolds the rung definitions and simplifies the exponent difference via field simplification and norm_num.
Claim. The ratio of the tau mass to the electron mass in Recognition Science units satisfies $m_τ / m_e = φ^{17}$.
background
In the LeptonMassLadder module, masses are assigned via mass_on_rung, defined as Anchor.E_coh multiplied by phi raised to an integer rung. The electron occupies rung 2 so that m_e_rs equals mass_on_rung 2, while the tau occupies rung 19 so that m_tau_rs equals mass_on_rung 19. This placement follows the module's RS derivation in which m_e scales as phi^2, m_mu as phi^13, and m_tau as phi^19 in E_coh units, producing the ratio m_tau/m_e as phi^17.
proof idea
The term proof unfolds m_tau_rs and m_e_rs to their mass_on_rung expressions, applies field_simp with phi_ne_zero to clear the denominator, rewrites the zpow difference via Real.zpow_sub, and finishes with norm_num to obtain the exponent 17.
why it matters
This supplies the second conjunct of lepton_masses_from_ladder, the theorem that resolves P-011 by stating the lepton masses follow from phi-ladder rungs with explicit ratios m_mu/m_e = phi^11, m_tau/m_e = phi^17, and m_tau/m_mu = phi^6. It confirms the rung spacing fixed by cube geometry that yields the numerical hierarchy phi^17 approximately 3571.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.