m_W_exp_sigma
plain-language theorem explainer
Numeric PDG-style one-sigma uncertainty on the W boson mass, fixed at 13.3 in the module's MeV convention. Used when scoring Recognition Science W-mass ladder predictions against experiment. Pure real constant: no proof, only a literal assignment.
Claim. The experimental one-standard-deviation uncertainty on the $W$ boson mass is the real constant $13.3$ (MeV-scale units matching the module's experimental mass table).
background
Module Verification.MassComparison is a quarantined side table: it compares Recognition Science mass predictions to PDG 2024 values and is kept off the certified surface because it imports external data and the φ-ladder anchor system.
RS 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. Sibling constants (m_e_exp_sigma, m_mu_exp_sigma, quark sigmas, etc.) store the matching experimental central values and uncertainties for each species.
m_W_exp_sigma is the W entry in that uncertainty column. Upstream name collisions on mass and Z in the SevenGaps ledger stack are unrelated ledger-mass and partition-function symbols, not particle masses.
proof idea
Definitional real literal: the body is the constant 13.3 with no lemmas, tactics, or obligations. Classification is def_or_abbrev.
why it matters
Gives the experimental error bar needed to judge whether an RS W-mass prediction (φ-ladder rung plus sector yardstick) lands inside the PDG band. The module's stated role is rigorous prediction-vs-PDG comparison; this constant is the W uncertainty half of that pair.
No downstream Lean users are wired yet (used_by empty), so it is table infrastructure rather than a forcing-chain step. It does not touch T5–T8, RCL, or the certified constant surface; it only supports the quarantined verification layer that cites PDG 2024 (Navas et al.).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.