muon_ratio_undershoot
plain-language theorem explainer
The declaration proves that the golden ratio raised to the eleventh power lies strictly below the experimental muon-to-electron mass ratio. Researchers checking Recognition Science lepton mass predictions against PDG 2024 data would cite this bound when confirming the phi-ladder undershoot. The proof is a one-line linear-arithmetic wrapper that combines an upper bound on phi^11 with the documented lower bound on the experimental ratio.
Claim. $phi^{11} < m_mu_exp / m_e_exp$, where $phi$ is the golden ratio and the right-hand side is the experimental muon-electron mass ratio (known to satisfy $206.76 < ratio < 206.77$).
background
The module verifies RS mass predictions against PDG experimental constants, which are imported rather than derived. The lepton-sector formula is $m(Lepton,r) = phi^{57+r}/(2^{22} times 10^6)$ MeV with B_pow = -22 and r0 = 62. Constants is the structure bundling CPM parameters (Knet, Cproj, Ceng, Cdisp) with the non-negativity axiom on Knet. phi11_lt proves Constants.phi^11 < 200 by rewriting to Real.goldenRatio, applying known bounds on phi^8 and phi^3, and using ring normalization. ratio_mu_e_exp is the definition m_mu_exp / m_e_exp, and ratio_mu_e_exp_bounds supplies the tight interval 206.76 < ratio < 206.77.
proof idea
One-line wrapper that applies the linarith tactic to the two facts phi11_lt (yielding phi^11 < 200) and the left conjunct of ratio_mu_e_exp_bounds (yielding 206.76 < ratio).
why it matters
The inequality supplies a concrete numerical check that the RS phi-ladder prediction for the muon-electron ratio lies below the experimental value, consistent with the mass formula in the lepton sector. It forms part of the machine-verified comparison to PDG 2024 data without deriving the experimental constants themselves. No downstream theorems in the module depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.