m_H_exp_sigma
plain-language theorem explainer
Experimental one-sigma uncertainty on the Higgs boson mass, fixed at 110 (same units as the companion experimental central value). Used only in the quarantined PDG comparison layer to score RS mass predictions against data. Pure numeric constant; no derivation.
Claim. The experimental standard uncertainty on the Higgs mass is the real constant $110$ (PDG-scale units matching the companion central-value constant).
background
The module Verification.MassComparison is a quarantined comparison layer: it imports PDG 2024 experimental masses and uncertainties and scores them against Recognition Science mass predictions. It is kept off the certified surface because experimental numbers are external inputs, not RS theorems.
RS masses themselves follow $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 part of that ladder; it is the experimental $\sigma$ paired with the Higgs central value for residual or $\chi^2$-style checks.
Sibling constants supply the same role for leptons and light quarks (m_e_exp_sigma, m_mu_exp_sigma, …). Upstream graph edges listed for this def are incidental name collisions, not mathematical dependencies.
proof idea
Definitional abbreviation: the real is set equal to the literal 110. No lemmas, no tactics, no derivation from $\varphi$ or the forcing chain.
why it matters
Gives the PDG-side error bar for Higgs mass in the machine-checked prediction-vs-experiment table. Without it, residuals cannot be normalized. It does not feed the certified RS core (T5–T8, RCL, mass ladder); the module header marks the whole file as quarantined external data. No downstream theorems currently depend on it in the supplied graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.