alpha_s_MZ_pos
plain-language theorem explainer
The theorem establishes that the strong coupling constant at the Z-boson mass scale is strictly positive under the Recognition Science geometric construction. QCD modelers working with one-loop running would cite the result when confirming the sign needed for asymptotic freedom. The proof is a one-line wrapper that unfolds the definitions of alpha_s_MZ and alpha_s_geom then applies norm_num to the resulting real number.
Claim. $0 < α_s(M_Z)$, where $α_s(M_Z)$ is the strong coupling at the Z-boson mass obtained from the geometric construction that evaluates to 2/17.
background
The module derives the running of α_s from Recognition Science by fixing its value at the Z scale and applying the one-loop beta function. It states α_s = 2/17 at M_Z with b₀ = (11N_c - 2N_f)/(12π) > 0 for N_f < 17, ensuring asymptotic freedom when N_c = 3. The definition alpha_s_MZ is set equal to alpha_s_geom, and upstream structural results confirm the underlying geometric and ledger constructions remain collision-free and algebraically closed.
proof idea
The proof is a one-line wrapper that unfolds alpha_s_MZ and alpha_s_geom, then invokes norm_num to verify the resulting real number satisfies the strict inequality.
why it matters
This positivity result is required for the beta function to produce the correct sign of the running in the RS model of the strong force. It supports the module's claim that α_s(M_Z) lies between 0.11 and 0.12 and feeds the extrapolation to nuclear scales. The theorem aligns with the framework's derivation of constants and the eight-tick octave while closing a verification step in the QCD RGE chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.