tau_electron_ratio_error
plain-language theorem explainer
The theorem shows that the experimental tau-to-electron mass ratio differs from phi^17 by less than 3 percent relative error. Particle physicists checking Recognition Science lepton mass predictions against PDG data would cite this bound. The proof reduces the target inequality to interval comparisons via positivity, absolute-value rewriting, and nlinarith on precomputed bounds for phi^17 and the experimental ratio.
Claim. $\left|\phi^{17} - \frac{m_\tau^\text{exp}}{m_e^\text{exp}}\right| \Big/ \frac{m_\tau^\text{exp}}{m_e^\text{exp}} < 0.03$, where $\phi$ denotes the golden ratio appearing in Constants.
background
The module compares Recognition Science mass predictions to PDG experimental values while treating the latter as imported constants. For leptons the integer-rung formula is m(Lepton, r) = phi^(57+r) / (2^22 * 10^6) in MeV. Constants is the abstract bundle containing Knet, Cproj and the golden-ratio value phi. ratio_tau_e_exp is defined as m_tau_exp / m_e_exp. The supporting lemmas establish 3569 < phi^17 < 3574 and 3477 < ratio_tau_e_exp < 3478.
proof idea
Tactic proof. Obtain the experimental-ratio bounds, prove positivity, rewrite the target via div_lt_iff_0 and abs_lt, then close both sides with nlinarith on phi17_gt, phi17_lt and the two ratio bounds.
why it matters
Supplies the numerical check that feeds row_tau_electron_ratio_pct in QuarkScoreCard and the overall mass_verification_cert_exists certificate. It closes one concrete instance of the phi-ladder mass formula against experiment inside the lepton sector (B_pow = -22, r0 = 62). The result sits downstream of the phi fixed-point construction (T6) and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.