m_b_at_MZ_GeV
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value from the phi-ladder or forcing chain.
- Does not propagate experimental uncertainties from PDG data.
- Does not specify the precise renormalization scale beyond M_Z.
- Does not perform the two-loop running itself.
formal statement (Lean)
31def m_b_at_MZ_GeV : ℝ := 2.85
proof body
Definition body.
32