mass_strange_exp
plain-language theorem explainer
The declaration supplies the PDG experimental value for the strange quark mass as the real constant 93.4. Model builders comparing quarter-ladder geometric predictions against measured quark masses cite this numeric target. It is introduced by direct assignment of the datum with no computation or derivation.
Claim. The experimental strange quark mass is defined as $93.4$ (in the model's mass units).
background
The module formalizes quark masses via the Quarter-Ladder Hypothesis: quarks share the structural base mass of leptons (Sector Gauge B=-22, R0=62) but sit at quarter-integer rungs on the phi-ladder. Ideal positions include strange at R = -10.00 = -40/4, with the listed discrepancy attributed to non-perturbative QCD effects not yet folded into the bare geometric derivation. The definition mirrors the identical constant from the RRF.Physics.QuarkMasses sibling module.
proof idea
Direct definition that assigns the constant 93.4 with no lemmas or tactics applied.
why it matters
It anchors the strange-quark target in the quarter-ladder comparison chain (top to bottom to charm to strange steps of 7.75, 2.50, 5.50 rungs). The value feeds downstream mass-match assessments inside the same module and connects to the broader phi-ladder mass formula. The module explicitly flags that light-quark discrepancies remain outside the current bare derivation and await reconciliation with the core parameter-free mass layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.