m_mu_rs
plain-language theorem explainer
Muon mass in RS units is defined as E_coh multiplied by phi to the 13th power. Researchers deriving lepton mass hierarchies from the phi-ladder cite this when computing ratios such as m_mu over m_e. The definition is a direct one-line application of mass_on_rung at rung index 13.
Claim. $m_μ^{RS} := E_{coh} φ^{13}$
background
In the Recognition Science framework masses sit on a phi-ladder scaled by the coherent energy E_coh. The upstream definition mass_on_rung(r) returns E_coh * phi^r for integer rung r. Module P-011 assigns the muon to rung 13, the electron to rung 2 and the tau to rung 19, yielding the fixed ratios m_μ/m_e = phi^11 and m_τ/m_μ = phi^6.
proof idea
One-line definition that applies mass_on_rung to the integer 13.
why it matters
Supplies the muon mass value required by lepton_masses_from_ladder, which resolves P-011. The definition anchors the phi-ladder spacing used for all three lepton ratios and feeds the positivity and ratio theorems that follow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.