pdg_up
plain-language theorem explainer
Fixes the PDG reference mass of the up quark at 2.16 (MeV-scale units used throughout the module). Downstream residual and RG-transport definitions cite this constant as the light-generation anchor for the up sector. The body is a bare real literal; no proof content.
Claim. The Particle Data Group reference mass for the up quark is fixed at $m_u^{\mathrm{PDG}} = 2.16$ in the module's mass units.
background
Item 8 Closure Target builds a minimal theorem layer for quark sub-leading mass corrections so the all-sector generalization becomes falsifiable. Mass inputs enter as PDG literals; residuals and RG transport then compare those data to Recognition Science ladder predictions.
The up-sector residual is formed from the charm-to-up mass ratio against rung 13, and light/heavy quark masses are transported to the RS anchor scale $\mu^*$ via piecewise $\alpha_s$ running. Both constructions need a fixed numerical $m_u$.
Sibling literals (pdg_charm, lepton and down-quark anchors) play the same role in other sectors. Units are the conventional MeV-scale PDG values used by the residual and transport helpers in this file.
proof idea
Definitional constant: the real literal 2.16 is assigned with no lemmas, tactics, or computation. Downstream noncomputable defs read the value directly.
why it matters
Supplies the light-generation up-quark mass for Item 8 residual and anchor-mass pipelines. upGen12Residual builds the gen-1–2 residual as rungResidual (pdg_charm / pdg_up) 13. upMassAtAnchor transports this mass through the two-GeV reference scale to the RS anchor with four active flavors.
Those quantities feed the refined-family solvability and uniqueness results that close the sub-leading correction item (existence and uniqueness of coefficients $(c,\eta)$ per sign sector). Without a pinned PDG up mass, the up-sector residual pair and transported anchor mass are undefined, so the falsifiable comparison to the phi-ladder mass formula cannot be stated numerically.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.