pdg_muon
plain-language theorem explainer
Fixes the PDG muon rest mass at 105.658 MeV/c² as a real constant for Item 8 residual arithmetic. Downstream lepton residual defs and sign theorems cite it when forming μ/e and τ/μ mass ratios against φ-ladder steps. The body is a bare numeric assignment, not a derived claim.
Claim. The Particle Data Group muon rest mass used in this module is the real constant $m_\mu^{\mathrm{PDG}} = 105.658$ (MeV units).
background
Item 8 Closure Target builds a minimal theorem layer for the open quark sub-leading mass correction and its all-sector generalization. Residuals compare observed mass ratios to pure φ-ladder steps: a residual is the logarithmic excess of a PDG ratio over φ raised to a fixed rung count.
Lepton generation steps used here are 11 (μ/e) and 6 (τ/μ). The muon mass enters both ratios, so a single shared numeric anchor keeps gen12 and gen23 residuals consistent with the same PDG table. Companion constants (electron, tau) play the same role for the other legs of those ratios.
The module already proves structural rigidity of the sign-split ratio family, closed-form η absorption of consistency violations, and unique solvability of the refined family per sector. Numeric PDG anchors are the data side of those residual pairs.
proof idea
No proof. The declaration is a definitional abbreviation equal to the literal real 105.658. Downstream code unfolds it under norm_num or ratio comparisons against powers of φ.
why it matters
Supplies the shared muon mass for leptonGen12Residual (rung residual of μ/e vs φ¹¹) and leptonGen23Residual (τ/μ vs φ⁶), and for the sign theorems that μ/e exceeds φ¹¹ while τ/μ lies below φ⁶. Those residuals feed the Item 8 refined-family closure story: unique (c, η) per sector once residual pairs are fixed.
In the broader RS mass picture, charged-lepton masses sit on the φ-ladder with a yardstick and rung offsets; sub-leading corrections are exactly the residuals this module isolates. Anchoring PDG numbers as named reals makes the falsifiable comparison between ladder prediction and data fully explicit inside Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.