pdg_down
plain-language theorem explainer
Fixes the PDG reference mass of the down quark at 4.67 MeV as a real constant. Downstream residual and RG-transport definitions cite it as the light-quark anchor for the down sector. The body is a bare numeric assignment with no proof obligations.
Claim. The Particle Data Group reference mass of the down quark is the real number $m_d^{\mathrm{PDG}} = 4.67$ (MeV).
background
Item 8 Closure Target builds a minimal theorem layer for the open quark sub-leading mass correction. The module compares predicted rung residuals and RG-transported masses against fixed PDG anchors so that the refined sign-split family can be solved uniquely for coefficients $(c,\eta)$.
pdg_down is one of those anchors: the conventional PDG down-quark mass (in MeV) used as a pure numeric input. Sibling constants play the same role for other flavors. No Recognition-Science derivation is claimed here; the value is an external experimental reference against which the $\phi$-ladder and running-coupling transport are checked.
Downstream, the ratio of strange to down PDG masses feeds a generation-1–2 residual, and the down mass itself is the starting point for transport through the piecewise $\alpha_s$ running to the RS anchor scale.
proof idea
No proof. The declaration is a def equal to the literal real 4.67. There are no tactics, lemmas, or hypotheses.
why it matters
Supplies the experimental down-quark mass that two Item-8 targets need. downGen12Residual forms the rung residual of the PDG strange/down ratio at step 6, testing the structural rigidity of the ratio family against data. downMassAtAnchor RG-transports this mass through the piecewise strong coupling from the 2 GeV quark reference scale to the RS anchor, with four active thresholds.
In the broader Recognition picture, quark masses sit on the $\phi$-ladder (yardstick times $\phi$ to a rung offset). Item 8 is the remaining sub-leading correction that must close before the all-sector mass formula is fully falsifiable. This constant does not prove that closure; it only pins the PDG side of the comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.