pdg_electron
plain-language theorem explainer
Fixes the PDG electron rest mass at 0.510999 (MeV) as a numeric anchor for lepton ratio residuals. Anyone computing μ/e or related generation-step residuals against the φ-ladder cites this constant. It is a bare real literal with no proof content.
Claim. The electron rest mass is the real constant $m_e = 0.510999$ (PDG value, MeV).
background
Item 8 Closure Target builds a minimal theorem layer for sub-leading mass corrections across sectors, so that quark and lepton residuals against the φ-ladder become falsifiable. Masses enter only through observed ratios; the ladder prediction for a generation step is a pure power of φ, and the residual measures the log-gap between data and that power.
The electron mass is the denominator of the first lepton generation ratio. Downstream, the μ/e residual is defined as the rung residual of pdg_muon / pdg_electron at rung 11. Positivity of that residual is the statement that the observed ratio exceeds φ¹¹.
Constants live in RS-native comparison units only insofar as ratios cancel the overall yardstick; the absolute MeV scale here is the standard PDG anchor, not an RS-derived mass.
proof idea
No proof. The declaration is a one-line real definition binding the symbol to the literal 0.510999.
why it matters
Supplies the electron mass used by leptonGen12Residual and the positivity theorem leptonGen12Residual_pos, which asserts that the μ/e residual is positive because the observed ratio exceeds φ¹¹. Those residuals feed the refined-family and sign-class machinery that aims to close Item 8 (unified sub-leading mass formula) for leptons before the all-sector generalization.
In the broader RS picture, charged-lepton masses sit on the φ-ladder with rung offsets; this constant is pure external data, not a derived mass formula. It does not touch T5–T8 forcing, RCL, or the α band; it only anchors empirical ratios against which ladder predictions are tested.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.