pdg_bottom
plain-language theorem explainer
Fixes the PDG bottom-quark mass anchor at 4180 MeV as a real constant. Downstream residual and RG-transport definitions cite it as the experimental input for the down-sector gen-2–3 step and for transporting the bottom mass to the RS anchor scale. The body is a bare numeric definition.
Claim. The Particle Data Group bottom-quark mass used as an experimental anchor is the real number $4180$ (MeV).
background
Item 8 Closure Target builds a minimal theorem layer for the open quark sub-leading mass correction. Residuals compare PDG mass ratios to pure $\varphi$-ladder predictions via rungResidual, and RG transport moves masses between flavor thresholds and the RS anchor scale.
pdg_bottom is the fixed experimental bottom mass (MeV) fed into those constructions. Sibling anchors (pdg_strange, etc.) play the same role for other flavors. No Recognition-derived formula is claimed here: the value is an external PDG input against which the refined residual family is tested.
proof idea
No proof. The declaration is a numeric def equating the symbol to the real literal $4180$.
why it matters
Supplies the experimental bottom mass for two Item-8 closure definitions. downGen23Residual forms the gen-2–3 down residual as rungResidual (pdg_bottom / pdg_strange) 8, the ratio step that the refined family and $\eta$-correction must match. bottomMassAtAnchor RG-transports this mass through alphaSPiecewise from the bottom threshold to the RS anchor (five active flavors), so sub-leading corrections can be compared at a common scale.
In the broader RS mass story, leading masses sit on the $\varphi$-ladder (yardstick $\cdot \varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$); Item 8 is the remaining sub-leading quark correction. Anchoring PDG bottom makes the all-sector residual target numerically concrete and falsifiable once the refined family is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.