strangeMassAtAnchor
plain-language theorem explainer
Defines the strange-quark MS-bar mass transported from the PDG 2 GeV reference to the RS anchor μ* ≈ 182.2 GeV. Downstream residual definitions for the down-sector gen12 and gen23 ratios cite it as the middle rung. The body is a direct call to multi-segment RG mass transport with piecewise α_s, bottom/top thresholds, and n_f = 4 at start.
Claim. Let $m_s^{\mathrm{PDG}} = 93.4\,\mathrm{MeV}$ at $\mu_{\mathrm{ref}} = 2\,\mathrm{GeV}$. The strange mass at the RS anchor is the multi-segment RG transport of this value to $\mu_\star = 182.201\,\mathrm{GeV}$ under the piecewise one-loop $\alpha_s$, crossing the bottom and top thresholds, with initial active-flavor count $n_f = 4$.
background
Item 8 Closure Target builds the smallest precise framework that would close the open quark sub-leading correction and make the all-sector generalization falsifiable. Light quarks are quoted in the MS-bar scheme at a shared 2 GeV reference; residuals at the RS anchor require transporting those masses upward through heavy-flavor thresholds.
The RS anchor scale is $\mu_\star = 182.201$ GeV, the stationarity point of the RG flow used throughout the monolith. Multi-segment mass transport runs a reference mass from $\mu_{\mathrm{start}}$ to $\mu_{\mathrm{end}}$ through a list of flavor thresholds, switching $n_f$ at each crossing. Piecewise one-loop $\alpha_s$ is stitched across top, bottom, and charm thresholds.
Here the PDG strange input is $93.4$ (MeV convention of the module), the start scale is 2 GeV, the end scale is $\mu_\star$, the threshold list is bottom then top, and the initial flavor count is 4 (above charm, below bottom).
proof idea
Not a proof: a noncomputable abbreviation. It instantiates transport_mass_through on pdg_strange, the piecewise $\alpha_s$ evaluator, start scale 2 GeV, end scale rs_anchor_scale, threshold list thresholdsFromTwoGeV (bottom, top), and $n_f^{\mathrm{init}} = 4$. Empty-list base case would call single-segment running_mass; with two thresholds the recursive branch switches $n_f$ at each crossing.
why it matters
Supplies the middle rung of the down-type ladder at the anchor. anchorDownGen12Residual is the rung residual of (strange/down) against step 6; anchorDownGen23Residual is the residual of (bottom/strange) against step 8. Those residuals feed the refined-family solvability and uniqueness apparatus that aims to close Item 8 (quark sub-leading corrections) and make the all-sector generalization falsifiable.
In the broader RS picture, masses sit on the $\varphi$-ladder (yardstick times $\varphi$ to a rung offset). Anchor-scale transport removes scheme/scale mismatch before comparing PDG ratios to ladder predictions. Without a common $\mu_\star$ mass for strange, the gen12 and gen23 down residuals are undefined and the $\exists!$ sector-closure theorems have no numerical target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.