pith. machine review for the scientific record. sign in
def definition def or abbrev high

m_b_predicted

show as:
view Lean formalization →

The definition computes the two-loop QCD-evolved bottom-quark MS-bar mass at its own scale by applying the running formula to the fixed reference value 2.85 GeV at M_Z with five active flavors. High-energy physicists validating Recognition Science mass anchors against PDG data would cite this quantity when checking the rung-21 prediction. It is realized as a direct one-line application of the m_running function to the constant m_b_at_MZ_GeV together with the two input couplings.

claimLet $m_b(M_Z)=2.85$ GeV be the Recognition Science reference value. The predicted MS-bar mass at its own scale is $m_b(m_b)=m_b(M_Z)·R(α_{m_b},α_{M_Z},5)$, where $R$ is the two-loop mass ratio that multiplies the leading-order factor by the exponential correction involving the coefficients $c_0,c_1,b_0,b_1$.

background

The Bottom Quark MS-bar Mass Scorecard module assigns the bottom quark rung 21 on the Recognition Science phi-ladder and records the PDG 2024 central value 4.18 GeV. The upstream constant m_b_at_MZ_GeV supplies the approximate MS-bar anchor 2.85 GeV at the Z-pole scale. The upstream m_running definition implements the full two-loop evolution: it multiplies the initial mass by mass_ratio_two_loop, which itself is the leading-order ratio times an exponential correction involving the coefficients c0, c1, b0, b1 for N_f = 5.

proof idea

The definition is a one-line wrapper that applies the m_running function to the constant m_b_at_MZ_GeV, the input couplings alpha_at_mb and alpha_at_MZ, and the flavor count 5.

why it matters in Recognition Science

This definition supplies the central prediction that enters the BottomMSBarCert structure and the positivity theorem m_b_predicted_pos. It closes the loop between the RS-anchored mass at M_Z and the observable m_b(m_b) by invoking the standard two-loop QCD running formula. Within the Recognition framework it tests whether the rung-21 assignment yields a value inside the PDG band after evolution.

scope and limits

formal statement (Lean)

  36def m_b_predicted (alpha_at_mb alpha_at_MZ : ℝ) : ℝ :=

proof body

Definition body.

  37  m_running m_b_at_MZ_GeV alpha_at_mb alpha_at_MZ 5
  38
  39/-- Closed RS heavy-quark scorecard value after two-loop running. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.