pdg_top
plain-language theorem explainer
Fixes the PDG top-quark pole mass at 172690 MeV as a real constant for Item 8 residual arithmetic. Downstream residual and RG-transport defs cite it as the gen-3 up-sector anchor. The body is a bare numeric assignment with no proof content.
Claim. The Particle Data Group top-quark mass used in this module is the real number $172690$ (MeV).
background
Item 8 Closure Target builds a minimal theorem layer for quark sub-leading mass corrections so the all-sector generalization becomes falsifiable. Residuals compare PDG mass ratios on the $\varphi$-ladder against predicted rung steps; the top enters the up-sector gen-2–3 ratio and the RG transport to the RS anchor scale.
Sibling constants (pdg_charm, etc.) play the same role for other flavors. upGen23Residual is rungResidual (pdg_top / pdg_charm) 11. topMassAtAnchor feeds pdg_top into Physics.RG.transport_mass_through with the piecewise $\alpha_s$ running from the top threshold to the RS anchor.
No Recognition-native derivation is claimed here: the value is an external experimental input in MeV, held fixed so residual identities and uniqueness proofs can treat data as concrete reals.
proof idea
Definitional constant: the right-hand side is the literal real 172690. No tactics, lemmas, or computation.
why it matters
Supplies the gen-3 up-quark mass anchor for Item 8. upGen23Residual builds the top/charm rung residual from it; topMassAtAnchor RG-transports it to the RS anchor under the LO scaffold so shell residuals can be compared to the refined family.
Within the module’s proved layer (consistency of the sign-split ratio family, closed-form $\eta$, solvability and uniqueness of refined-family coefficients), this constant is pure data plumbing. It does not touch T5–T8 forcing, RCL, or the mass yardstick formula beyond providing the experimental numerator those residual checks need.
Closing Item 8 means matching such PDG-anchored residuals with unique $(c,\eta)$; without a fixed top mass the gen-23 up residual is undefined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.