tau_relative_error
plain-language theorem explainer
The Recognition Science mass prediction for the tau lepton at rung 19 satisfies a relative deviation below three percent from the experimental value 1776.86 MeV. Particle physicists checking discrete phi-ladder consistency with PDG data cite this bound for the lepton sector. The proof rewrites the prediction to an auxiliary quantity, imports its explicit interval bounds, rewrites the relative-error claim via division and absolute-value lemmas, and discharges the resulting inequalities with linear arithmetic.
Claim. Let $m_τ^pred = 2^{B} ϕ^{-5} ϕ^{r_0} ϕ^{19} / 10^6$ be the Recognition Science mass in MeV for the lepton sector at rung 19, with sector parameters $B = B_{pow}$ and $r_0 = r0$. Then $|m_τ^pred - 1776.86| / 1776.86 < 0.03$.
background
In the Masses.Verification module experimental lepton masses enter as imported constants, not outputs of the Recognition Science derivation. The function rs_mass_MeV evaluates the integer-rung mass formula in MeV: $2^{B_{pow}(s)} ϕ^{-5} ϕ^{r0(s)} ϕ^r / 10^6$ for sector $s$ and rung $r$. Module documentation states that the lepton sector uses $B_{pow} = -22$ and $r0 = 62$, which collapses to $ϕ^{57+r} / (2^{22} × 10^6)$ MeV. The upstream theorem tau_mass_bounds records the concrete interval $1821 < tau_pred < 1823$ for the auxiliary prediction at rung 19, while m_tau_exp is fixed at the numerical constant 1776.86.
proof idea
The tactic proof begins by rewriting the left-hand side via tau_pred_eq, which equates rs_mass_MeV .Lepton 19 to the auxiliary tau_pred. It obtains the interval bounds hb from tau_mass_bounds and proves positivity of m_tau_exp by norm_num. The target inequality is rewritten with div_lt_iff₀ and abs_lt; after unfolding m_tau_exp the two-sided comparison is discharged by nlinarith applied directly to the components of hb.
why it matters
The result is invoked by row_tau_pct to document three-percent agreement for the tau and is packaged inside mass_verification_cert_exists together with the electron and muon counterparts. It also appears in the conjunction asserted by phi_ladder_verified, which states that the full set of lepton relative errors lies inside the stated tolerances. Within the Recognition Science framework this supplies one concrete check that the phi-ladder mass formula reproduces PDG values for the lepton sector at the documented precision.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.