rs_alpha_s_MZ_range
plain-language theorem explainer
The theorem shows that the RS one-loop strong coupling at the Z mass scale lies strictly between 0.11 and 0.14. QCD phenomenologists would cite the bound to confirm that the RS-derived value remains perturbative. The proof unfolds the running formula and anchor definitions, substitutes the six-flavor beta coefficient, and verifies the numerical inequality by a chain of positivity, log-negativity, and linarith steps.
Claim. There exists a real number $x$ such that the RS one-loop strong coupling constant evaluated at the Z-boson mass equals $x$ and $0.11 < x < 0.14$.
background
The module derives renormalization-group running from the RS φ-ladder. The anchor scale μ* = 182.201 GeV is a stationarity point of the flow; the one-loop formula for the strong coupling is alpha_s_running(Q) = alpha_s_MZ / (1 + b0 * alpha_s_MZ * log(Q²/M_Z²) / (2π)), with b0_qcd(n_f) the first beta coefficient. The declaration rs_alpha_s_MZ is obtained by evaluating this formula at the RS anchor and rescaling to M_Z = 91.2 GeV. Upstream results supply the beta-function structure (beta_function_from_ladder_derivative) and the explicit running definition (alpha_s_running from QCDRGE.AlphaRunning).
proof idea
Tactic proof that refines an existential witness to rs_alpha_s_MZ itself. Both branches unfold rs_alpha_s_MZ, alpha_s_running, rs_alpha_s_anchor and rs_anchor_scale, then set b0_qcd 6 = 7 by norm_num. The first branch defines the denominator 1 + (7/(2π))·0.1181·log(91.2/182.201), proves it lies in (0.86,1) via positivity, log-negativity and nlinarith, and concludes 0.1181/denom > 0.11 by linarith. The second branch proves the symmetric upper bound 0.1181/denom < 0.14 by the same numerical estimates.
why it matters
The result closes the perturbative-range claim for the RS value of α_s(M_Z) that appears in the paper proposition alpha_s_at_MZ ≈ 0.1185. It sits inside the asymptotic-freedom block (T6–T7 of the forcing chain) where the φ-ladder derivative forces β_QCD < 0 for n_f ≤ 16. No downstream theorems yet depend on it, so it functions as a numerical sanity check rather than a lemma in a larger derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.