rs_alpha_s_perturbative
plain-language theorem explainer
The declaration proves that the RS strong coupling at the anchor scale satisfies 0 < α_s(μ*) < 1. QCD phenomenologists working on perturbative running would cite this to confirm the coupling remains in the perturbative regime at μ* = 182.201 GeV. The proof is a one-line term wrapper that splits the conjunction and normalizes the numerical definition of the anchor value.
Claim. $0 < α_s(μ^*) < 1$, where μ* is the RS anchor scale at which the strong coupling equals 0.1181.
background
The module derives renormalization group flows from the RS φ-ladder. The anchor scale μ* = 182.201 GeV is a stationarity point of the RG flow, and the β-function is obtained from the ladder derivative β(g) = (1/ln φ) dg/dr. The upstream rs_alpha_s_anchor supplies the concrete value 0.1181, while PrimitiveDistinction.from extracts the four structural conditions plus three definitional facts from seven independent axioms.
proof idea
The proof is a one-line term-mode wrapper. It applies the constructor tactic to split the conjunction into two goals and then invokes norm_num on the definition of rs_alpha_s_anchor to discharge both inequalities by direct numerical evaluation.
why it matters
This result confirms perturbativity of α_s at the RS anchor, a prerequisite for the one-loop running formula and the asymptotic freedom criterion β_QCD < 0 for n_f ≤ 16. It supports the module's key results on the running coupling formula and α_s(M_Z) ≈ 0.1185. The declaration closes the perturbative regime check before ladder-based evolution to other scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.