upMassAtAnchor
plain-language theorem explainer
Defines the up-quark MS-bar mass after one-loop QCD running from the PDG 2 GeV reference to the RS anchor μ* ≈ 182.2 GeV. Anyone building Item-8 anchor residuals or gen-12 mass ratios cites it. The body is a direct call to multi-segment mass transport through the bottom and top thresholds with n_f = 4 initially.
Claim. Let $m_u^{\mathrm{PDG}} = 2.16\,\mathrm{MeV}$ at $\mu_{\mathrm{ref}} = 2\,\mathrm{GeV}$. The up mass at the RS anchor is the multi-segment RG transport of this value to $\mu^* = 182.201\,\mathrm{GeV}$ under the piecewise one-loop $\alpha_s$, crossing the bottom and top flavor thresholds, starting with $n_f = 4$.
background
Item 8 of the Recognition Science verification stack concerns the sub-leading quark mass correction. This module builds the smallest precise framework that would close that item and make the all-sector generalization falsifiable. Light-quark PDG masses are quoted in the MS-bar scheme at 2 GeV; RS mass formulas and residual diagnostics are evaluated at the stationarity anchor $\mu^* = 182.201$ GeV.
Transport uses transport_mass_through: multi-segment running of a mass from $\mu_1$ to $\mu_2$ through a list of flavor thresholds, switching $n_f$ at each crossing. The coupling is the piecewise one-loop $\alpha_s$ stitched across charm, bottom, and top thresholds. From 2 GeV the relevant upward thresholds are bottom then top, so the initial active flavor count is $n_f = 4$.
proof idea
Pure definition: a single application of multi-segment mass transport. Arguments are the PDG up mass 2.16, the piecewise $\alpha_s$, start scale 2 GeV, end scale $\mu^*$, the threshold list [bottom, top], and initial $n_f = 4$. No lemmas or tactics; the value is whatever the RG runner returns.
why it matters
Feeds anchorUpGen12Residual, which forms the rung residual of the charm-to-up mass ratio at the anchor (under the LO scaffold, roughly $(0.02, +0.57)$ in rung units). Those residuals are the data side of the refined-family solvability and uniqueness theorems that close Item 8 for each sign sector. Without a common-scale up mass, gen-12 quark residuals cannot be compared to the $\phi$-ladder mass formula or to the $\eta$-corrected sub-leading ansatz. Sits in the verification layer that makes the open quark correction item falsifiable against PDG inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.