m_tau_exp
The declaration supplies the experimental tau lepton mass in MeV as a fixed real constant for scorecard comparisons. Researchers verifying the phi-ladder mass formula against PDG data cite this value when checking the rung-19 prediction for the tau. It enters as a direct numeric assignment drawn from external measurement tables.
claimThe experimental tau lepton mass is the constant $m_τ^{exp} = 1776.86$ MeV.
background
In the Masses.Verification module experimental masses function as imported benchmarks, explicitly quarantined from the certified RS surface. The local lepton formula is $m(Lepton, r) = φ^{57+r} / (2^{22} × 10^6)$ MeV with B_pow = -22 and r0 = 62. Upstream, Mass is the real-number type and Rung is the rational position on the phi-ladder.
proof idea
One-line definition that directly assigns the numeric literal 1776.86. No lemmas or tactics are invoked; the value is hardcoded from PDG 2024.
why it matters in Recognition Science
This constant populates the tau row of ChargedLeptonMassScoreCardCert and MassVerificationCert, enabling the 3-percent tolerance check |rs_mass_MeV .Lepton 19 - m_tau_exp| / m_tau_exp < 0.03. It closes the experimental anchor for the integer-rung predictions that descend from the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain.
scope and limits
- Does not derive the value from the Recognition Composition Law or J-cost functional equation.
- Does not include PDG uncertainty intervals or error propagation.
- Does not apply to quark or other non-lepton sectors.
- Does not assert exact equality with any RS-native prediction.
Lean usage
example : |rs_mass_MeV .Lepton 19 - m_tau_exp| / m_tau_exp < 0.03 := row_tau_pctformal statement (Lean)
38def m_tau_exp : ℝ := 1776.86
proof body
Definition body.
39
40/-! ## Integer-Rung Mass Formula -/
41