m_s_exp
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 in Recognition Science
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.
scope and limits
- Does not derive the mass from Recognition Science equations.
- Does not carry uncertainty bounds or renormalization details.
- Does not apply to up-type quarks or other sectors.
- Does not update when PDG values change.
formal statement (Lean)
49def m_s_exp : ℝ := 93.5