downMassAtAnchor
plain-language theorem explainer
Defines the down-quark MS-bar mass at the RS anchor μ* = 182.201 GeV by RG-transporting the PDG value 4.67 MeV from the 2 GeV light-quark reference through bottom and top thresholds. Anyone computing Item-8 anchor residuals for the down sector cites this number. It is a thin wrapper around multi-segment mass transport with piecewise one-loop α_s and n_f starting at 4.
Claim. Let $m_d^{\mathrm{PDG}}=4.67\,\mathrm{MeV}$ be the PDG down mass at $\mu_{\mathrm{ref}}=2\,\mathrm{GeV}$. The down mass at the RS anchor is the multi-segment RG transport of $m_d^{\mathrm{PDG}}$ from $\mu_{\mathrm{ref}}$ to $\mu^*=182.201\,\mathrm{GeV}$, using the piecewise one-loop $\alpha_s(\mu)$ stitched across heavy-quark thresholds, crossing the bottom and top thresholds, with initial active flavor count $n_f=4$.
background
Item 8 of the Recognition Science verification stack concerns the open quark sub-leading mass correction. This module builds the smallest precise theorem framework that would close that item and make the all-sector generalization falsifiable. Residuals are formed at a common high scale so that sector ratios can be compared without mixing reference-scale conventions.
The RS anchor scale is fixed at $\mu^*=182.201,\mathrm{GeV}$, the stationarity point of the RG flow used throughout the monolith. Light MS-bar quarks $(u,d,s)$ are quoted by PDG at $2,\mathrm{GeV}$; upward transport must cross the bottom and top flavor thresholds, switching $n_f$ at each crossing.
transport_mass_through runs a reference mass from $\mu_{\mathrm{start}}$ to $\mu_{\mathrm{end}}$ through a list of flavor thresholds. The coupling is the piecewise one-loop $\alpha_s$ that selects the $n_f=6,5,4,3$ branch according to whether $\mu$ sits above top, bottom, charm, or below charm. Initial $n_f=4$ is appropriate just above the charm threshold at the $2,\mathrm{GeV}$ start.
proof idea
Pure definition: apply multi-segment mass transport to the PDG down mass, the piecewise $\alpha_s$, start scale $2,\mathrm{GeV}$, end scale $\mu^*$, the threshold list $[b,t]$, and $n_f^{\mathrm{init}}=4$. No proof obligations; the body is a single call.
why it matters
Anchor-scale down mass is the denominator input to the down-sector gen-1–2 residual: the residual is formed from the strange-to-down mass ratio at $\mu^*$ against rung step 6. Without a common-scale transport, PDG light-quark numbers at $2,\mathrm{GeV}$ cannot enter the refined-family residual algebra that Item 8 needs for $\exists!$ closure on $(c,\eta)$.
In the broader RS picture, masses sit on the $\varphi$-ladder with yardstick and rung corrections; sub-leading quark corrections are the remaining obstruction to a fully closed mass formula across sectors. This definition is infrastructure, not a forcing-chain step (T0–T8), but it is required before residual signatures and refined-family uniqueness can be checked against PDG data at one scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.