pdg_strange
plain-language theorem explainer
Fixes the PDG strange-quark mass anchor at 93.4 MeV (RS-native comparison units). Downstream residual and RG-transport defs cite it as the middle rung of the down sector. Pure numeric constant; no proof content.
Claim. The Particle Data Group strange-quark mass used as the Item-8 anchor is the real constant $m_s^{\mathrm{PDG}} = 93.4$ (MeV-scale units consistent with the module's other PDG anchors).
background
Item 8 Closure Target builds a minimal theorem layer for the open quark sub-leading mass correction. Residuals compare PDG mass ratios to pure $\varphi$-ladder predictions via rungResidual, then feed a refined two-coefficient family $(c,\eta)$ that absorbs the structural inconsistency of the plain sign-split family.
The down-type sector uses three PDG anchors (down, strange, bottom). The strange mass sits between them: gen-1–2 residual is built from $m_s/m_d$ at rung step 6, gen-2–3 from $m_b/m_s$ at step 8. A separate RG helper transports this same anchor through $\alpha_s$ running to the RS mass scale.
No Recognition-native derivation is claimed here; the number is an external experimental input against which the $\varphi$-ladder and refined-family predictions are scored.
proof idea
Definitional abbreviation: the real literal 93.4. No tactics, lemmas, or algebraic reduction.
why it matters
Supplies the middle PDG datum for the down-quark residual pair that Item 8 must close. downGen12Residual and downGen23Residual form the observed residual signature whose unique $(c,\eta)$ solution is the sector-closure target; strangeMassAtAnchor carries the same number through RG transport to the RS anchor scale.
In the broader RS mass story, bare masses sit on the $\varphi$-ladder (yardstick $\cdot,\varphi^{r_{-}8+\mathrm{gap}(Z)}$). Item 8 is the sub-leading correction layer that makes all-sector generalization falsifiable once residuals are matched. Without a fixed strange anchor, the down-sector $\exists!$ closure statements have nothing concrete to fit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.