mass_tau_PDG_sigma
plain-language theorem explainer
Records the PDG experimental one-sigma uncertainty on the tau lepton mass as the real constant 0.12 (MeV scale used throughout the comparison module). Cited by anyone checking Recognition Science mass-ladder predictions against Particle Data Group tables. The body is a bare numeric definition with no proof obligations.
Claim. The Particle Data Group one-sigma uncertainty on the tau lepton mass is the real number $0.12$ (in the MeV convention of this verification module).
background
The module Machine-Verified PDG Comparison holds experimental CODATA and PDG anchors side-by-side with Recognition Science interval predictions. It is explicitly quarantined from the certified surface: experimental numbers are imported, not derived, and comparisons are informational only.
Sibling constants fix the central PDG masses for the electron, muon, and tau, together with their one-sigma uncertainties, plus the CODATA 2022 inverse fine-structure value and its error. The tau entry pairs with mass_tau_PDG (central value) so that later interval or sigma-band checks can be written without hard-coding floats.
No upstream lemmas are required; the declaration is a pure numeric anchor drawn from PDG 2024 tables.
proof idea
Bare definition: the real constant is set equal to 0.12. No tactics, no lemmas, no reduction.
why it matters
Supplies the experimental error bar needed to judge whether an RS tau-mass prediction (phi-ladder yardstick times a rung/gap correction) lands inside the PDG band. The parent module’s key verified claim is the alpha-inverse containment 137.030 < α⁻¹_RS < 137.039 versus CODATA; the lepton-mass anchors play the analogous role for the mass sector. Because the module is quarantined, this constant never enters the forcing chain (T0–T8) or the Recognition Composition Law; it only supports external consistency checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.