m_s_exp_sigma
plain-language theorem explainer
Numeric constant fixing the PDG one-sigma uncertainty on the strange-quark mass at 8.6 MeV. Cited by anyone comparing Recognition Science φ-ladder mass predictions against experiment in this quarantined verification module. The body is a bare real literal; there is no proof obligation.
Claim. The experimental one-standard-deviation uncertainty on the strange-quark mass is fixed at $8.6\,\mathrm{MeV}$ (PDG 2024 scale, consistent with the companion central-value constant in the same module).
background
The module MassComparison is deliberately quarantined from the certified RS surface: it imports external PDG 2024 numbers and the anchor/φ-ladder mass formula, neither of which is derived inside the certified core. The RS prediction shape is $m(\mathrm{species})=\mathrm{yardstick}(\mathrm{sector})\times\varphi^{r_0+r_{\mathrm{species}}}$, with coherence energy $E_{\mathrm{coh}}=\varphi^{-5}$.
Sibling constants supply central values and sigmas for leptons and light quarks ($m_e$, $m_\mu$, $m_\tau$, $m_u$, $m_d$, $m_s$, …). The present definition is the experimental width that pairs with the strange-quark central value. Upstream name collisions on mass from the SevenGaps gravity development are unrelated ledger/column masses and do not constrain this constant.
proof idea
No proof. The declaration is a one-line def equal to the real literal 8.6. It records an external experimental figure rather than deriving a proposition.
why it matters
Supplies the experimental error bar needed to score how tightly the RS strange-quark rung prediction sits against PDG 2024. The module exists precisely to host such side-by-side comparisons while remaining outside the certified surface. No downstream theorems currently depend on it (used_by is empty); it is infrastructure for future residual or σ-band lemmas. It does not touch the forcing chain T0–T8, RCL, or the α band; it only anchors the empirical side of the mass-ladder check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.