row_tau_pct
plain-language theorem explainer
The theorem asserts that the Recognition Science mass prediction for the tau lepton at rung 19 differs from the experimental value 1776.86 MeV by a relative error under 3 percent. Physicists checking the phi-ladder mass formula against measured lepton masses would cite this bound. The proof consists of a direct one-line reference to the tau_relative_error theorem in the Verification module.
Claim. $|rs_mass_MeV(Lepton, 19) - 1776.86| / 1776.86 < 0.03$, where $rs_mass_MeV$ is the Recognition Science mass formula in MeV for sector and rung.
background
The QuarkScoreCard module consolidates theorem-grade facts for the quark sector and related fermions, recording ZOf assignments including ZOf = 1332 for charged leptons. The rs_mass_MeV function from Verification computes the predicted mass via $2^{B_pow s} * phi^{-5} * phi^{r0 s} * phi^r / 10^6$ for sector s and rung r. The experimental value m_tau_exp is fixed at 1776.86. This result depends on the upstream Lepton inductive type and the tau_relative_error theorem, which establishes the identical bound by rewriting to tau_pred_eq and applying tau_mass_bounds.
proof idea
The proof is a one-line wrapper that applies the tau_relative_error theorem from the Verification module.
why it matters
This supplies the tau mass error bound required by quarkScoreCardCert_holds, which aggregates ZOf_up, ZOf_down, ZOf_lep together with the charm/up and top/charm ratio theorems. It also feeds row_tau_rel in ChargedLeptonMassScoreCard. In the Recognition framework it confirms the phi-ladder prediction for the tau at rung 19 lies inside the 3 percent tolerance, consistent with the mass formula and eight-tick octave while leaving the gap(ZOf) correction open per the module status.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.