tau_electron_ratio_error
The theorem establishes that the experimental tau-to-electron mass ratio differs from phi to the 17th power by a relative error below 3 percent. Researchers checking Recognition Science lepton mass predictions against PDG data would cite this bound. The proof obtains positivity of the experimental ratio, rewrites the target inequality via div_lt_iff₀ and abs_lt, then closes it with nlinarith on the supplied phi^17 and ratio bounds.
claim$|r - m_τ^exp / m_e^exp| / (m_τ^exp / m_e^exp) < 0.03$ where $r = φ^{17}$ and $φ$ is the golden ratio (with experimental masses treated as imported constants).
background
The Masses.Verification module imports experimental lepton masses as constants from PDG 2024 and quarantines them from RS derivations. ratio_tau_e_exp is defined as m_tau_exp / m_e_exp with theorem ratio_tau_e_exp_bounds giving the interval (3477, 3478). Upstream lemmas phi17_gt and phi17_lt bound Constants.phi ^ 17 between 3569 and 3574 using phi_eq_goldenRatio together with numerical bounds on Real.goldenRatio powers. The module setting compares the RS lepton formula m(Lepton, r) = φ^{57+r} / (2^{22} × 10^6) MeV to these experimental values.
proof idea
The proof first derives positivity of ratio_tau_e_exp from ratio_tau_e_exp_bounds via linarith. It rewrites the absolute-value relative-error goal with div_lt_iff₀ and abs_lt. The closing step applies nlinarith to the conjunction of phi17_gt, phi17_lt, and the two experimental bounds.
why it matters in Recognition Science
The result is invoked verbatim by row_tau_electron_ratio_pct in QuarkScoreCard to certify the tau-electron PDG ratio match within 3 percent, and it contributes to mass_verification_cert_exists which assembles the full lepton verification certificate. It supports the phi-ladder mass formula in the lepton sector, consistent with phi as the self-similar fixed point.
scope and limits
- Does not derive experimental mass values from RS principles.
- Does not claim exact equality between the ratio and phi^17.
- Does not extend the bound to quark or boson sectors.
- Does not incorporate measurement uncertainties beyond the stated 3 percent threshold.
Lean usage
theorem row_tau_electron_ratio_pct : |Constants.phi ^ (17 : ℕ) - Verification.ratio_tau_e_exp| / Verification.ratio_tau_e_exp < 0.03 := Verification.tau_electron_ratio_errorformal statement (Lean)
244theorem tau_electron_ratio_error :
245 |Constants.phi ^ (17 : ℕ) - ratio_tau_e_exp| / ratio_tau_e_exp < 0.03 := by
proof body
Tactic-mode proof.
246 have hr := ratio_tau_e_exp_bounds
247 have hexp_pos : (0 : ℝ) < ratio_tau_e_exp := by linarith [hr.1]
248 rw [div_lt_iff₀ hexp_pos, abs_lt]
249 constructor <;> nlinarith [phi17_gt, phi17_lt, hr.1, hr.2]
250
251/-! ## Summary Certificate -/
252