m_tau_exp
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.