mass_strange_exp
plain-language theorem explainer
mass_strange_exp supplies the experimental mass of the strange quark as the constant 93.4 in Recognition Science units. A researcher comparing quarter-ladder geometric predictions to data would cite this value when assessing the R = -10 rung. The declaration is a direct numerical assignment with no computation.
Claim. $m_s^{exp} = 93.4$ (in MeV, the measured strange-quark mass used for comparison with the quarter-ladder rung $R = -10$).
background
The module formalizes T12 quark masses under the Quarter-Ladder Hypothesis: quarks share the lepton structural base mass but sit at quarter-integer rungs on the phi-ladder. The strange quark is assigned the ideal topological position $R = -10.00 = -40/4$, with light-quark discrepancies ascribed to non-perturbative QCD effects not yet modeled. This definition supplies the measured benchmark against which the phi-ladder mass formula (yardstick times phi to the power of rung offset) is compared.
proof idea
Direct definition that assigns the literal real number 93.4 to the identifier.
why it matters
The constant anchors the strange-quark entry in the T12 spectrum, enabling direct numerical checks of the quarter-ladder hypothesis against experiment. It sits downstream of the general mass formula on the phi-ladder and upstream of the full set of quark-mass residuals (res_strange etc.). The placement ties to the eight-tick octave and D = 3 spatial dimensions through the underlying J-cost and rung arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.