m_b_PDG_GeV
plain-language theorem explainer
The declaration fixes the PDG central value for the bottom-quark MS-bar mass at its own scale as 4.18 GeV. Recognition Science modelers and QCD phenomenologists cite it when testing the phi-ladder mass formula at rung 21 against experiment. The definition is a direct numerical binding with no further computation or hypothesis.
Claim. The central value of the bottom-quark mass in the MS-bar scheme evaluated at the scale of the mass itself is defined to be $4.18$ GeV.
background
The module BottomMSBarScoreCard assembles a comparison between the Recognition Science mass prediction for the bottom quark and the PDG 2024 experimental input. The bottom quark is assigned rung 21 on the phi-ladder as a down-type fermion of the third generation. The supplied definition supplies the numerical anchor used by all subsequent statements in the file.
proof idea
The declaration is a direct definition that binds the literal real number 4.18 to the identifier.
why it matters
It supplies the experimental central value required by BottomMSBarCert, which checks that the RS prediction at rung 21 lies inside the PDG band. The definition therefore closes the comparison between the eight-tick octave mass formula and the measured bottom mass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.