mass_tau_PDG
plain-language theorem explainer
Records the PDG 2024 central value of the tau lepton mass as 1776.86 MeV for side-by-side comparison with Recognition Science mass-ladder predictions. Anyone checking lepton-sector numerics against experiment cites this constant. It is a bare real literal, not a derived claim.
Claim. The Particle Data Group central value for the $\tau$ lepton rest mass is $m_\tau^{\mathrm{PDG}} = 1776.86\,\mathrm{MeV}$ (uncertainty $0.12\,\mathrm{MeV}$ is recorded separately).
background
The module Verification.PDGComparison is quarantined from the certified RS surface: it imports external experimental numbers so that machine-checked interval comparisons can be stated, without those numbers entering the proof chain.
Sibling constants fix the electron and muon PDG masses and the CODATA 2022 inverse fine-structure value. The RS side of the comparison uses the phi-ladder mass formula (yardstick times $\phi$ raised to a rung offset by the gap weight) and the forced RS band $137.030 < \alpha^{-1}_{\mathrm{RS}} < 137.039$.
Units here are MeV for lepton masses; the companion sigma definition holds the quoted $0.12,\mathrm{MeV}$ uncertainty.
proof idea
No proof. The declaration is a definition equal to the real literal $1776.86$, matching the PDG 2024 central value cited in the module header (Navas et al., Phys. Rev. D 110, 030001).
why it matters
Gives the experimental anchor for the heaviest charged lepton in the PDG comparison layer. Downstream numerical checks (when present) can test whether an RS mass-ladder prediction for the tau lands inside the PDG window. The module's key certified result is the alpha-inverse containment; lepton mass constants sit beside that as informational benchmarks, not as steps in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.