muon_electron_ratio_error
plain-language theorem explainer
The declaration delivers a verified bound showing the experimental muon-to-electron mass ratio differs from phi to the eleventh power by a relative error below 0.04. Researchers auditing Recognition Science lepton mass predictions against PDG data would cite this result to populate verification scorecards. The short tactic proof obtains pre-established bounds on the ratio and on phi^11, rewrites the inequality, and discharges both sides via linear arithmetic.
Claim. $ |φ^{11} - r| / r < 0.04 $, where $ r $ is the experimental muon-electron mass ratio $ m_μ^exp / m_e^exp $ and $ φ $ is the golden ratio constant from the CPM bundle.
background
The Masses.Verification module compares Recognition Science mass predictions to PDG experimental values, treating the latter as quarantined imported constants rather than derived quantities. For the lepton sector the integer-rung formula is $ m(Lepton, r) = φ^{57+r} / (2^{22} × 10^6) $ in MeV. The muon-electron ratio is defined directly as the quotient of the two experimental masses, and a companion theorem supplies the tight numerical interval 206.76 < ratio < 206.77. Separate lemmas establish the companion bounds 198.9 < φ^11 < 200 by reducing to the golden-ratio definition and applying known power inequalities.
proof idea
The proof obtains the experimental ratio bounds, proves positivity of the ratio by linarith, rewrites the target inequality via div_lt_iff₀ and abs_lt, and discharges both resulting goals by nlinarith applied to the phi^11 bounds together with the ratio interval endpoints.
why it matters
The result is invoked verbatim by row_muon_electron_ratio_pct in QuarkScoreCard, which states that the muon-electron PDG mass ratio matches φ^11 within 4 percent. It also feeds mass_verification_cert_exists, which assembles the full lepton mass certificate. In the Recognition framework the bound supports the phi-ladder mass assignments for leptons, consistent with the self-similar fixed point φ forced at T6 and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.