M_Z_GeV
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.