m_e_exp_sigma
plain-language theorem explainer
Literal PDG-style one-sigma uncertainty on the electron rest mass, stored as a real constant 1.6e-10. Mass-comparison and residual checks in the quarantined verification layer cite it next to the electron central value. The body is a bare numeric assignment, not a derived claim.
Claim. The experimental one-standard-deviation uncertainty on the electron rest mass is fixed as the real constant $1.6 \times 10^{-10}$ (MeV scale, matching the sibling electron central-value entry).
background
Module Verification.MassComparison holds a machine-checked side-by-side of Recognition Science mass predictions against PDG 2024 numbers. It is explicitly quarantined from the certified surface: experimental inputs are not RS-derived, and the predictions ride the anchor / φ-ladder rung system.
RS species masses take the form $m = \mathrm{yardstick}(\mathrm{sector}) \times \varphi^{r_0 + r_{\mathrm{species}}}$, with coherence energy $E_{\mathrm{coh}} = \varphi^{-5}$ and sector integers from cube geometry. This declaration is not that formula. It is the experimental error bar paired with the electron central value among the lepton/quark m_*_exp / m_*_exp_sigma siblings.
Name collisions on mass in the SevenGaps ledger stack (column mass, class mass, Gibbs weight) are unrelated; they do not feed this constant.
proof idea
Definitional constant: the real is assigned the decimal literal 0.00000000016. No lemma, no tactic, no reduction. Downstream code treats it as the electron experimental σ in the same units as m_e_exp.
why it matters
Supplies the electron experimental uncertainty for residual and σ-band comparisons in the PDG 2024 verification layer. Without it, predicted-vs-measured electron checks cannot report a dimensionless pull. It does not touch the forcing chain (T0–T8), RCL, or the φ-ladder derivation of masses; it only anchors the external datum. No downstream theorems currently depend on it in the graph, so it is infrastructure for comparison reports rather than a step in a proved mass theorem. The module’s quarantine status remains: importing this number never certifies an RS prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.