theorem proved term proof

`rs_alpha_s_perturbative`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 100theorem rs_alpha_s_perturbative :
 101    0 < rs_alpha_s_anchor ∧ rs_alpha_s_anchor < 1 := by

Term-mode proof.

 102  constructor <;> norm_num [rs_alpha_s_anchor]
 103
 104/-- **RS α_s(M_Z)**: Running from μ* = 182.201 GeV to M_Z = 91.2 GeV. -/

Lean names referenced from this declaration's body.