m_s_exp
plain-language theorem explainer
Experimental strange-quark mass fixed at 93.4 MeV (MS-bar, 2 GeV) for PDG-2024 comparison. Anyone checking RS phi-ladder mass predictions against data cites this constant. It is a bare real literal with no proof obligation.
Claim. The experimental strange-quark mass used for comparison is the real number $93.4$ (MeV, $\overline{\mathrm{MS}}$ scheme at $2\,\mathrm{GeV}$).
background
The MassComparison module holds PDG 2024 experimental masses side-by-side with Recognition Science predictions. It is quarantined from the certified surface because the numbers are external data, not derived from the forcing chain.
RS masses follow $m = \mathrm{yardstick}(\mathrm{sector})\times\varphi^{r_0+r_{\mathrm{species}}}$, with coherence energy $E_{\mathrm{coh}}=\varphi^{-5}$ and sector yardsticks fixed by cube geometry. Experimental anchors such as this strange-quark value supply the denominator of any residual or sigma comparison.
Sibling constants cover the charged leptons and the light quarks $u,d,s$, each paired with an uncertainty companion.
proof idea
Pure definition: the real literal 93.4 is assigned with no tactics, lemmas, or computation. The accompanying doc-comment records the PDG central value and the 8.6 MeV uncertainty (the latter lives in the sibling sigma definition).
why it matters
Supplies the experimental strange-quark mass that residual and sigma lemmas in this module compare against RS phi-ladder predictions. Without fixed PDG anchors the verification layer cannot quantify agreement for the light-quark sector. The module itself stays outside the certified surface; the constant merely enables that external check. It does not touch T0–T8, RCL, or the derivation of $\varphi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.