M_Z_GeV
M_Z_GeV supplies the Z-boson mass 91.1876 GeV as the reference scale for one-loop evolution of the strong coupling in the Recognition Science QCD model. Researchers matching RS predictions to lattice data or low-energy phenomenology would cite this constant when evaluating alpha_s below the electroweak scale. The entry is a direct numerical assignment with no lemmas or reductions applied.
claimThe Z-boson mass is defined as $M_Z = 91.1876$ GeV.
background
The module implements one-loop renormalization group evolution of the strong coupling starting from the Z scale, with the Recognition Science model fixing alpha_s(M_Z) = 2/17 and the beta coefficient b0 = (11 N_c - 2 N_f)/(12 pi) for N_c = 3 to enforce asymptotic freedom when N_f < 17.
proof idea
Direct numerical definition by literal assignment; no lemmas or tactics invoked.
why it matters in Recognition Science
M_Z_GeV anchors the definitions alpha_s_running and the theorems log_at_MZ and low_Q_log_negative. It realizes the module claim that alpha_s equals 2/17 at M_Z, linking the phi-ladder constants to the observed Z mass and enabling the demonstration of asymptotic freedom at lower energies.
scope and limits
- Does not derive the numerical value from the Recognition Science forcing chain.
- Does not incorporate higher-loop beta functions or electroweak corrections.
- Does not specify the active flavor count N_f_Z.
- Does not address non-perturbative regimes below the QCD scale.
formal statement (Lean)
53def M_Z_GeV : ℝ := 91.1876
proof body
Definition body.
54
55/-- Running α_s at scale Q (one-loop). -/