m_tau_exp
plain-language theorem explainer
Records the PDG 2024 experimental tau lepton mass as the real constant 1776.86 MeV. Mass-verification and ratio lemmas cite it as the experimental denominator when checking RS phi-ladder predictions against data. The body is a bare numeric definition, not a derived claim.
Claim. The experimental tau mass is the real number $m_\tau^{\mathrm{exp}} = 1776.86$ MeV (PDG 2024 central value, with reported uncertainty $0.12$ MeV).
background
The MassComparison module is quarantined from the certified RS surface: it imports PDG experimental numbers and compares them to RS mass predictions built from the phi-ladder. Predictions take the form $m(\mathrm{species}) = \mathrm{yardstick}(\mathrm{sector}) \times \varphi^{r_0 + r_{\mathrm{species}}}$, with coherence energy $E_{\mathrm{coh}} = \varphi^{-5}$ and sector yardsticks fixed by cube geometry.
Sibling constants fix the other charged-lepton and light-quark PDG anchors ($m_e^{\mathrm{exp}}$, $m_\mu^{\mathrm{exp}}$, etc.). This entry is the tau anchor. Upstream, the same numeric literal appears in Masses.Verification so both modules share one experimental reference.
Comparisons are relative: absolute RS MeV values are divided by these experimental constants to obtain percent-level residuals and mass ratios such as $m_\tau/m_e$.
proof idea
No proof. The declaration is a definition equating the identifier to the real literal 1776.86. Downstream theorems unfold it and discharge numeric goals with norm_num.
why it matters
Supplies the experimental tau mass used throughout the verification layer. phi_ladder_verified asserts $|\tau_{\mathrm{pred}} - m_\tau^{\mathrm{exp}}|/m_\tau^{\mathrm{exp}} < 0.03$; tau_relative_error proves the same bound for the lepton rung-19 prediction; ratio_tau_e_exp and ratio_tau_e_exp_bounds build the experimental ratio $m_\tau/m_e \in (3477, 3478)$. MassVerificationCert packages the tau window among the certificate fields.
In the broader RS picture this is not a forcing-chain step (T0–T8). It is the empirical side of the mass-ladder check: RS predicts masses on the $\varphi$-ladder from the electron anchor; this constant is what those predictions are scored against. The module remains quarantined precisely because such PDG inputs are external to the derived core.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.