m_b_at_MZ_GeV
plain-language theorem explainer
The declaration supplies the RS-anchored reference value for the bottom quark MS-bar mass at the Z-boson scale, fixed at 2.85 GeV. Heavy-quark running calculations in the Recognition Science framework cite this constant as the input for two-loop QCD evolution from M_Z down to the bottom scale. It is introduced as a direct numeric definition with no lemmas or proof obligations.
Claim. The bottom-quark MS-bar mass at the Z-boson scale equals 2.85 GeV.
background
This definition sits inside the Bottom Quark MS-bar Mass Scorecard module. The module records the PDG 2024 value m_b(m_b) = 4.18 ± 0.03 GeV in the MS-bar scheme and assigns the RS sector rung b = 21 to the down-type third generation. The constant functions as the fixed starting point for mass running under the two-loop anomalous dimension.
proof idea
The declaration is a one-line definition that directly assigns the real number 2.85. No tactics, lemmas, or reductions are applied.
why it matters
The value anchors the bottom-quark scorecard and is referenced by the positivity statement m_b_at_MZ_pos together with the running prediction m_b_predicted. It supplies the numerical input at rung b = 21 for the RS mass formula and two-loop evolution, linking the phi-ladder to observable heavy-quark masses. The module reports zero sorry statements and zero axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.