pdg_tau
plain-language theorem explainer
Numeric PDG anchor for the tau lepton mass, fixed at 1776.86 (MeV units). Downstream residual and sign lemmas for the lepton gen-2/3 step cite it when comparing the observed τ/μ ratio to a pure φ-ladder step. The body is a bare real literal; no derivation is claimed.
Claim. The Particle Data Group reference value for the tau lepton mass is the real constant $m_\tau^{\mathrm{PDG}} = 1776.86$ (MeV).
background
Item 8 Closure Target builds a minimal theorem layer for sub-leading mass corrections across sectors. Residuals compare PDG mass ratios to pure φ-ladder steps (powers of the golden ratio fixed by the RS forcing chain), then feed a refined family with coefficients $(c,\eta)$.
Sibling anchors (pdg_muon, etc.) play the same role for other generations. Here pdg_tau is the experimental numerator in the τ/μ ratio. The module already proves structural facts about ratio families (consistency forcing a vanishing weighted sum, closed-form η, unique solvability per sign class) and documents where raw PDG data break the uncorrected family.
Upstream constant edges are incidental Mathlib/field constructors, not physics inputs; the only content is the PDG float.
proof idea
Definitional abbreviation: the real literal 1776.86 is assigned with no proof obligations, tactics, or lemmas. Downstream code unfolds it under norm_num when comparing ratios to powers of φ.
why it matters
Feeds leptonGen23Residual, defined as the rung residual of pdg_tau / pdg_muon against a six-rung φ step, and the theorem leptonGen23Residual_neg, which shows that residual is negative because the observed ratio lies strictly below $φ^6$. Those objects sit inside the Item 8 program: closing a unique refined-family fit for lepton gen-2/3 data and making the all-sector sub-leading correction falsifiable. The constant itself is not an RS prediction; it is the external mass yardstick against which ladder residuals and η corrections are measured. Landmarks touched only indirectly: the φ-ladder mass formula and the open quark sub-leading item the module targets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.