muon_electron_ratio
plain-language theorem explainer
The theorem states that the muon-to-electron mass ratio equals phi to the eleventh power in RS units. Physicists deriving lepton spectra from the phi-ladder cite it to fix the rung spacing between electron and muon. The proof unfolds the mass-on-rung definitions for rungs 13 and 2, cancels the common E_coh prefactor, subtracts the exponents, and normalizes the difference to 11.
Claim. In RS units the muon-to-electron mass ratio satisfies $m_μ / m_e = φ^{11}$, where $m_e = E_{coh} φ^2$ and $m_μ = E_{coh} φ^{13}$.
background
The module formalizes P-011, deriving lepton masses from the phi-ladder. Electron mass sits on rung 2 and muon mass on rung 13, each given by the mass_on_rung definition: Anchor.E_coh multiplied by phi to the rung power. This rests on the phi fixed point from the forcing chain and the general mass formula in RS units.
proof idea
The term proof unfolds m_mu_rs and m_e_rs to their mass_on_rung expressions, applies field_simp to cancel E_coh while using phi_ne_zero to justify the operations, rewrites via Real.zpow_sub to subtract the exponents, and finishes with norm_num to obtain the exact difference of 11.
why it matters
This supplies the first conjunct of lepton_masses_from_ladder, which resolves P-011 by fixing the ratios m_μ/m_e = φ^11, m_τ/m_e = φ^17. It is instantiated in AnchorPolicy for fermion masses at anchors and used to derive muonic Bohr radius properties in ProtonRadius. The result realizes the 11-step rung spacing on the phi-ladder, consistent with self-similar structure and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.