mass_electron_PDG_sigma
plain-language theorem explainer
Records the PDG one-sigma uncertainty on the electron rest mass as the real constant 1.6e-10 in the module's mass units. Cited by any numerical check that compares an RS electron-mass prediction to experiment with error bars. The body is a bare numeric definition, not a derived claim.
Claim. The Particle Data Group one-standard-deviation uncertainty on the electron mass is the real number $1.6 \times 10^{-10}$ (in the mass units fixed by this verification module).
background
The module Machine-Verified PDG Comparison holds experimental CODATA/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 serve only informational comparison.
Sibling constants fix the electron, muon, and tau PDG central values and their sigmas, together with the CODATA 2022 inverse-fine-structure value and its uncertainty. Mass units are those used by the lepton-generation definitions imported from Physics.LeptonGenerations.Defs; the sigma here is the experimental error bar that would accompany mass_electron_PDG in a residual or pull computation.
No upstream RS theorem is required. The constant is pure data transcription from PDG 2024 (Navas et al.).
proof idea
Definitional constant: the real literal 0.00000000016 is assigned directly. No lemma, tactic, or algebraic reduction is involved.
why it matters
Supplies the experimental error bar needed to turn an RS electron-mass prediction into a dimensionless pull or a containment check against PDG. Sits in the same quarantined verification layer as the alpha-inverse CODATA band (RS interval 137.030–137.039 containing the measured 137.035999177(21)). It does not enter the forcing chain T0–T8, the Recognition Composition Law, or the phi-ladder mass formula; it only anchors external comparison. Downstream use is currently empty in the graph, so the constant is infrastructure for future residual lemmas rather than a link in the certified proof spine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.