alpha_s_MZ_bounds
plain-language theorem explainer
The theorem establishes that the strong coupling constant at the Z boson mass scale lies strictly between 0.11 and 0.12 in RS-native units. QCD phenomenologists matching the Recognition Science geometric prediction to experimental data at the Z pole would cite this bound when initializing one-loop running. The proof is a one-line term-mode reduction that unfolds the geometric definition of alpha_s and applies numerical normalization to the rational 2/17.
Claim. $0.11 < alpha_s(M_Z) < 0.12$, where $alpha_s(M_Z)$ denotes the strong coupling evaluated at the Z-boson mass from the geometric wallpaper fraction.
background
The module treats the running of the strong coupling from the Recognition Science geometric input. It sets alpha_s equal to 2/17 at the Z-boson mass and invokes the one-loop beta function b0 = (11 N_c - 2 N_f)/(12 pi), which remains positive for N_f less than 17 and thereby encodes asymptotic freedom with N_c fixed at 3. The upstream definition alpha_s_geom supplies the constant 2/17 as the wallpaper fraction, while alpha_s_MZ is the direct alias of that value in real numbers. The anchor integer map Z appears among the dependencies but is not invoked in the bound itself.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definitions of alpha_s_MZ and alpha_s_geom to expose the rational 2/17, splits the conjunction via constructor, and invokes norm_num to confirm both decimal inequalities hold.
why it matters
This bound supplies the concrete numerical anchor for the strong coupling inside the QCD running module and thereby supports the one-loop evolution of alpha_s down to nuclear scales. It closes the geometric input step that follows from the wallpaper fraction in the Recognition Science framework, consistent with the module's claim of full machine verification. No downstream theorems are recorded yet, so the result functions as a verified starting point for any later running calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.