m_W_exp
plain-language theorem explainer
Records the PDG 2024 central value of the W boson mass as 80369.2 MeV. Cited by anyone comparing Recognition Science electroweak mass predictions against experiment. It is a bare real constant, not a derived claim.
Claim. The experimental W boson mass central value is fixed as $m_W^{\mathrm{exp}} = 80369.2\,\mathrm{MeV}$ (equivalently $80.3692\,\mathrm{GeV}$).
background
The MassComparison module holds PDG 2024 experimental anchors side-by-side with Recognition Science mass predictions. It is quarantined from the certified surface because experimental numbers are external inputs, not RS-derived, and because the predictions themselves sit on the $\varphi$-ladder anchor system.
RS masses take the form $m(\mathrm{species}) = \mathrm{yardstick}(\mathrm{sector})\times\varphi^{r_0+r_{\mathrm{species}}}$, with yardstick built from coherence energy $E_{\mathrm{coh}}=\varphi^{-5}$ and sector integers from cube geometry. Experimental constants such as this W mass supply the comparison targets for those predictions.
The value matches the PDG 2024 entry quoted in the module header (Navas et al., Phys. Rev. D 110, 030001).
proof idea
No proof. The declaration is a one-line real constant equal to 80369.2, encoding the PDG central value in MeV. The companion uncertainty 13.3 MeV appears only in the doc-comment, not in the term.
why it matters
Gives the electroweak sector a fixed experimental reference so predicted W masses on the $\varphi$-ladder can be checked numerically against PDG 2024. Lives in the verification layer rather than the forcing chain (T0–T8); it does not derive $m_W$ from J-cost, RCL, or eight-tick structure. Downstream comparison lemmas and residual tables read this constant as the experimental baseline for the W boson.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.