ratio_mu_e_exp_bounds
plain-language theorem explainer
Experimental data places the muon-to-electron mass ratio strictly between 206.76 and 206.77. Verification of Recognition Science lepton mass predictions against PDG values relies on this numerical bound. The proof is a one-line wrapper that unfolds the ratio definition and discharges the inequalities with norm_num.
Claim. Let $m_e^{exp} = 0.51099895069$ and $m_μ^{exp} = 105.6583755$. Then $206.76 < m_μ^{exp}/m_e^{exp} < 206.77$.
background
The Masses.Verification module imports experimental lepton masses as fixed real constants from PDG 2024 for comparison against RS predictions. The electron mass is defined as 0.51099895069 MeV and the muon mass as 105.6583755 MeV, with their ratio formed directly as the quotient. This setup quarantines experimental inputs from certified RS derivations, allowing machine-checked numerical checks against the phi-ladder formula for leptons with B_pow = -22 and r0 = 62.
proof idea
The proof is a one-line wrapper. It unfolds ratio_mu_e_exp, m_mu_exp, and m_e_exp to expose the division, then applies constructor to split the conjunction and norm_num to confirm both inequalities hold for the given decimal expansions.
why it matters
The bound supplies the numerical anchor for downstream comparisons in the same module. muon_electron_ratio_error invokes it to bound the relative deviation from phi^11 by 0.04, while muon_ratio_undershoot uses the lower bound to establish phi^11 < ratio_mu_e_exp. This supports the framework's prediction that the muon-electron ratio approximates the 11th power of the golden ratio phi, as required by the mass formula m(Lepton, r) = phi^(57+r) / (2^22 * 10^6) in MeV.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.