m_tau_exp
plain-language theorem explainer
m_tau_exp supplies the PDG 2024 experimental tau lepton mass as a benchmark constant for RS mass verification. Scorecard authors and verification pipelines cite it when checking the tau row against the phi-ladder formula. It enters as a one-line definition that hardcodes the measured value without derivation from the Recognition framework.
Claim. Let $m_τ^{exp}$ denote the experimental mass of the tau lepton in MeV. Then $m_τ^{exp} := 1776.86$.
background
In the Masses.Verification module experimental mass values are quarantined imported constants, not derived from RS. The module states the lepton-sector formula $m(Lepton, r) = φ^{57+r} / (2^{22} × 10^6)$ in MeV with B_pow = -22 and r0 = 62, referencing PDG 2024. Upstream, Mass is an abbreviation for the real numbers and Rung is a rational number on the phi-ladder.
proof idea
One-line definition that directly assigns the numerical value 1776.86 drawn from PDG 2024.
why it matters
This constant anchors the tau clause in ChargedLeptonMassScoreCardCert (requiring relative error < 0.03) and appears in MassVerificationCert and phi_ladder_verified. It supplies the experimental benchmark that lets the integer-rung predictions (T6 phi fixed point, T7 eight-tick octave) be compared directly to observation while remaining outside the certified RS derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.