tau_mass_bounds
plain-language theorem explainer
The theorem shows that the Recognition Science tau lepton mass prediction lies strictly between 1821 and 1823 MeV. Researchers checking the phi-ladder mass formula against PDG data would cite this bound inside the lepton verification certificate. The proof unfolds the prediction definition then applies the pre-established phi^76 interval bounds together with direct numerical scaling to close both sides of the inequality.
Claim. Let $m_τ^{pred} = φ^{76} / 4194304000000$. Then $1821 < m_τ^{pred} < 1823$.
background
In the lepton sector the Recognition Science mass formula is $m(Lepton, r) = φ^{57+r} / (2^{22} × 10^6)$ in MeV, with $B_{pow} = -22$ and $r_0 = 62$. For the tau the relevant rung yields the concrete definition $τ_{pred} = φ^{76} / 4194304000000$. The Constants structure supplies the golden-ratio base $φ$ together with the auxiliary lemmas $φ^{76} > 7638724000000000$ and $φ^{76} < 7646046000000$ that anchor the numerical interval.
proof idea
Unfold the definition of tau_pred. Apply constructor to split the conjunction. For the lower bound rewrite with lt_div_iff and reduce the scaled comparison to the known phi76_gt lemma via a short calc block. For the upper bound rewrite with div_lt_iff and reduce the scaled comparison to phi76_lt via a symmetric calc block, closing each side with norm_num.
why it matters
This bound is invoked directly by mass_verification_cert_exists to populate the tau_in_range field of the MassVerificationCert and by tau_relative_error to control the relative deviation from the experimental value. It therefore completes the machine-checked comparison of the phi-ladder prediction against PDG 2024 data for the third lepton generation, closing one concrete instance of the mass formula verification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.