quarkReferenceScale2GeV
plain-language theorem explainer
Fixes the shared PDG reference energy for light MS-bar quarks (u, d, s) at 2 GeV. Anyone transporting PDG light-quark masses to the RS anchor scale cites this constant. The body is a one-line numeric definition, not a derived claim.
Claim. The common PDG reference scale for the light $\overline{\mathrm{MS}}$ quark masses $m_u$, $m_d$, and $m_s$ is fixed at $2\,\mathrm{GeV}$.
background
Item 8 of the Recognition Science verification program concerns sub-leading corrections to the quark mass formula. This module builds the smallest precise framework that would close that item and make the all-sector generalization falsifiable: ratio families, residual signatures, and refined $(c,\eta)$ closures for each charge sector.
PDG quotes light-quark $\overline{\mathrm{MS}}$ masses at a conventional renormalization point of $2,\mathrm{GeV}$. Heavier flavors and the RS mass ladder live at other scales, so comparison requires RG transport. Downstream definitions call Physics.RG.transport_mass_through from this reference through a piecewise $\alpha_s$ and a threshold list up to the RS anchor $\mu^*$.
The constant itself carries no dynamics; it is the shared starting energy for the three light-flavor transport maps used when residual signatures and ratio-family coefficients are evaluated at the anchor.
proof idea
Pure definition: the real constant $2$. No lemmas, tactics, or algebraic reduction. Downstream mass-at-anchor defs plug it in as the source scale argument of the RG transport.
why it matters
Without a single shared source scale, the three light-quark anchor masses would not be comparable under the same transport path. This constant is the common first argument of upMassAtAnchor, downMassAtAnchor, and strangeMassAtAnchor, which feed residual pairs and the refined-family solvability/uniqueness results that target Item 8 closure.
It sits on the verification side of the mass ladder (yardstick $\cdot,\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$), not in the T0–T8 forcing chain. Closing Item 8 needs PDG numbers moved to $\mu^*$ before residual signatures and $\eta$-refined families can be checked against data. The definition is the bookkeeping hinge for that move.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.