m_e_rs
plain-language theorem explainer
m_e_rs sets the electron mass to E_coh times phi to the power 2 in RS units. Researchers deriving muon and tau masses from the phi-ladder cite this baseline when forming ratios such as m_mu over m_e. The definition is a direct application of the mass_on_rung helper at rung 2.
Claim. The electron mass in RS units is given by $m_e = E_{coh} phi^2$.
background
mass_on_rung takes an integer rung r and returns Anchor.E_coh multiplied by phi raised to r. The module assigns the electron to rung 2 on the phi-ladder while formalizing P-011 for lepton masses, with m_e proportional to phi^2, m_mu to phi^13, and m_tau to phi^19. Upstream, mass_on_rung is defined as the general mass formula in RS units: E_coh · φ^r where r is the rung.
proof idea
one-line wrapper that applies mass_on_rung with rung 2.
why it matters
This definition supplies the electron baseline for lepton_masses_from_ladder, which resolves P-011 by proving the ratios m_mu_rs / m_e_rs = phi^11 and m_tau_rs / m_e_rs = phi^17. It implements the mass formula on the phi-ladder and connects to the self-similar fixed point phi from the forcing chain T5-T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.