alpha_s_MZ
alpha_s_MZ fixes the strong coupling at the Z boson mass scale to the RS geometric value 2/17. QCD researchers cite it when matching the predicted alpha_s(M_Z) to experimental measurements in the 0.11-0.12 interval. The definition is a direct alias to the upstream wallpaper fraction with no further reduction.
claim$α_s(M_Z) := 2/17$
background
The module treats the running of the strong coupling from the Recognition Science geometric input. It adopts the one-loop beta function b₀ = (11N_c - 2N_f)/(12π) with N_c = 3, which remains positive for N_f < 17 and encodes asymptotic freedom. The base value is supplied by the upstream definition alpha_s_geom, documented as the wallpaper fraction 2/17 and the predicted strong coupling.
proof idea
One-line definition that directly aliases the geometric constant alpha_s_geom.
why it matters in Recognition Science
This definition supplies the RS input α_s(M_Z) = 2/17 that downstream results confirm lies inside the experimental band 0.11 < α_s(M_Z) < 0.12 and is positive. It anchors the one-loop running formula alpha_s_running for evolution to nuclear scales. The placement matches the module claim that α_s equals 2/17 at M_Z, consistent with the strong-force geometry and the condition N_f < 17 for asymptotic freedom.
scope and limits
- Does not derive the 2/17 fraction from the forcing chain or J-uniqueness.
- Does not incorporate two-loop or higher beta-function corrections.
- Does not fix the active flavor count N_f at the Z scale.
- Does not evaluate the coupling at arbitrary momentum scales Q.
Lean usage
theorem alpha_s_MZ_pos : 0 < alpha_s_MZ := by unfold alpha_s_MZ alpha_s_geom; norm_numformal statement (Lean)
44def alpha_s_MZ : ℝ := alpha_s_geom
proof body
Definition body.
45