m_s_exp
plain-language theorem explainer
The declaration supplies the PDG 2024 experimental value 93.5 MeV for the strange quark mass. Quark mass verification routines cite it to benchmark Recognition Science predictions against data. It is a direct constant definition with no computation or derivation.
Claim. $m_s^{exp} = 93.5$ (MeV, PDG 2024 MS-bar at 2 GeV)
background
The module compares Recognition Science quark mass formulas to PDG 2024 values. Down-type quarks use the formula $m = 2^{23} phi^{-10+r}/10^6$ MeV with rung integers r=4 for d, r=15 for s, r=21 for b. The strange quark sits at rung 15 in the down sector. This definition imports the central PDG value 93.5 MeV as a fixed real constant for direct numerical comparison.
proof idea
Direct definition that assigns the literal real number 93.5 with no lemmas or tactics applied.
why it matters
It anchors the experimental side of the quark mass verification for the strange quark at rung 15. The value enters comparisons against the down-sector formula derived from the phi-ladder and the eight-tick octave in the forcing chain. It remains quarantined from the certified RS surface as an imported constant rather than a derived result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.