ratio_tau_e_exp_bounds
plain-language theorem explainer
Experimental data place the tau-to-electron mass ratio strictly between 3477 and 3478. Researchers checking Recognition Science lepton mass predictions against PDG values cite this bound when comparing to the phi-ladder formula. The proof is a one-line wrapper that unfolds the ratio and mass definitions then applies norm_num to confirm the inequalities.
Claim. $3477 < m_τ^exp / m_e^exp < 3478$, where $m_e^exp := 0.51099895069$ and $m_τ^exp := 1776.86$ are the imported PDG experimental constants.
background
In the Masses.Verification module experimental masses are imported constants rather than RS-derived quantities. The electron mass is defined as m_e_exp := 0.51099895069 and the tau mass as m_tau_exp := 1776.86. Their ratio is introduced by the definition ratio_tau_e_exp := m_tau_exp / m_e_exp. The module documentation states that these values remain quarantined from the certified surface of Recognition Science derivations.
proof idea
The proof is a one-line wrapper. It unfolds the definitions of ratio_tau_e_exp, m_tau_exp and m_e_exp. Constructor splits the conjunction and norm_num discharges each numerical inequality.
why it matters
This bound supplies the numerical anchor for comparing the experimental tau-electron ratio to the RS prediction phi^17. It is invoked in tau_ratio_overshoot to prove the experimental value lies below phi^17 and in tau_electron_ratio_error to bound the relative error below 0.03. The result supports verification of the lepton-sector mass formula m(Lepton, r) = phi^{57+r} / (2^22 × 10^6) MeV against PDG data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.