pdg_charm
plain-language theorem explainer
Fixes the PDG charm-quark mass anchor at 1270 MeV as a real constant. Downstream residual and RG-transport definitions cite it when building up-sector gen-12/23 residuals and the charm mass at the RS anchor scale. The body is a literal numeric assignment with no proof obligations.
Claim. The Particle Data Group charm-quark mass used as the numerical anchor is the real number $1270$ (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 against PDG mass ratios and asks whether a refined coefficient family can match the data uniquely.
PDG sector masses enter as fixed real anchors. The charm value is the middle rung of the up-type chain: it appears in the ratio charm/up for the gen-12 residual and top/charm for the gen-23 residual, and as the starting mass for RG transport down to the RS anchor scale.
No Recognition-native derivation is claimed here; the number is an external experimental input against which the phi-ladder residual machinery is tested.
proof idea
Pure definition: the real constant is set to the literal 1270. No lemmas, tactics, or algebraic reduction.
why it matters
Feeds three local consumers: charmMassAtAnchor (RG transport of this mass through the piecewise alpha_S schedule to the RS anchor), upGen12Residual (rung residual of pdg_charm/pdg_up at step 13), and upGen23Residual (rung residual of pdg_top/pdg_charm at step 11). Those residuals are the data side of the refined-family solvability and uniqueness theorems that close Item 8 for the up sector. In the broader RS mass picture, yardstick times phi^(rung-8+gap(Z)) supplies the leading ladder; this constant is the experimental counterpart used to measure sub-leading residuals, not a derived RS mass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.