mass_electron_PDG
plain-language theorem explainer
PDG electron rest mass fixed at 0.51099895069 MeV, the central experimental value used for RS-versus-data checks. Authors of the quarantined PDG comparison module cite it when scoring lepton mass predictions. It is a bare real literal with no proof body.
Claim. The Particle Data Group electron rest mass is the real constant $0.51099895069$ MeV (central value; uncertainty $16$ in the last digits is recorded separately).
background
The module Machine-Verified PDG Comparison holds experimental anchors from PDG 2024 and CODATA 2022 so that Recognition Science numerical predictions can be compared side-by-side with data. It is explicitly quarantined from the certified surface: experimental imports are not derived from RS, and the comparisons are informational only.
Sibling constants record the matching PDG central values and sigmas for the muon and tau, plus CODATA $\alpha^{-1}$ and the RS $\alpha^{-1}$ interval $(137.030, 137.039)$. The electron mass here is the MeV-scale yardstick against which the RS phi-ladder mass formula for the electron is scored.
No upstream Lean theorems are required; the value is taken from the PDG review (Navas et al., Phys. Rev. D 110, 030001, 2024).
proof idea
Pure definition: a real literal assignment with empty proof body. No lemmas, tactics, or algebraic reduction.
why it matters
Supplies the experimental electron mass anchor inside the quarantined verification layer. Downstream comparison scripts (not yet wired as used_by edges on this declaration) can subtract RS electron-mass predictions from this constant and test residual size against the recorded PDG sigma. It does not enter the forcing chain T0–T8, the Recognition Composition Law, or the certified alpha band; those remain independent of PDG numbers. Its role is purely metrological: keep the experimental reference frozen and machine-readable so interval containment claims stay reproducible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.