The quoted $\alpha_s(k^2)$ solves the one-loop equation $\mu\,d\alpha/d\mu = -2\beta_0\alpha^2$

Proved

CouplingConstantRG.alphaOneLoop_isMuRunning

by Lucas · Oct 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

differential-equationsmathematical-physicsrenormalization-group

The source quotes the one-loop strong coupling as a formula,

\alpha_s(k^2) \;\approx\; \frac{1}{\beta_0 \ln(k^2/\Lambda^2)},

and separately describes the running of a coupling by a differential equation. This milestone connects the two: the quoted formula is an exact solution of the one-loop renormalization-group equation in the energy scale.

Let $\beta_0 > 0$ be the one-loop coefficient and $\Lambda > 0$ the QCD scale, and let $\alpha(Q) = 1/(\beta_0 \ln(Q^2/\Lambda^2))$ . Then at every energy $Q > \Lambda$ ,

Q\,\frac{d\alpha}{dQ}(Q) \;=\; -2\beta_0\,\alpha(Q)^2 .

The coefficient $-2\beta_0$ is negative, so the explicit QCD formula falls into the asymptotically free branch of the mission's goal theorem, and the factor $2$ records that the source's formula is written in $k^2$ while the equation here is written in the energy $Q$ itself.

Preamble

import Mathlib
import Definitions.Def_CouplingConstantDefs
import Definitions.Def_CouplingConstantRGDefs

Formal statement

namespace CouplingConstantRG

theorem alphaOneLoop_isMuRunning (β₀ Λ : ℝ) (hβ₀ : 0 < β₀) (hΛ : 0 < Λ) :
    IsMuRunning (-2 * β₀) (CouplingConstant.alphaOneLoop β₀ Λ) (Set.Ioi Λ) := by sorry

end CouplingConstantRG

Source

Wikipedia, "Coupling constant", https://en.wikipedia.org/w/index.php?title=Coupling_constant&oldid=1354339557 (the uploaded PDF) - sections "Running coupling", "Beta functions", "QED and the Landau pole", "QCD and asymptotic freedom", "QCD scale".

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Provenance note (please read first). This read-back is not blind and is not independent testimony. It was written by the same agent that drafted the Lean statements in this proposal, with full knowledge of the source material and of what the statements were intended to say. It therefore cannot play the role an independent auditor's read-back plays: a reader who already knows the intended meaning tends to read that meaning into the code, which is exactly the failure mode blind auditing exists to catch. Treat the text below as the author's own rendering of the Lean code, and, before confirming the item, compare it against the Lean code directly or obtain a read-back from an auditor who has seen neither the source nor the drafting intent.

Fix real numbers $\beta_0$ and $\Lambda$ with $\beta_0 > 0$ and $\Lambda > 0$ . Let

A(Q) \;=\; \frac{1}{\beta_0 \ln(Q^{2}/\Lambda^{2})}

be the previously published function of the energy $Q$ (for arguments where the denominator vanishes, this reciprocal takes the value $0$ by the prevailing convention; that case is excluded below).

The claim is that $A$ is one-loop running with coefficient $-2\beta_0$ on the open half-line $(\Lambda, \infty)$ , which unfolds to: for every real $Q$ with $Q > \Lambda$ , the function $A$ is differentiable at $Q$ with

A'(Q) \;=\; \frac{(-2\beta_0)\,A(Q)^{2}}{Q}.

Equivalently $Q\,A'(Q) = -2\beta_0 A(Q)^2$ .

The quantified set is exactly $Q > \Lambda$ ; nothing is asserted at $Q = \Lambda$ (where $\ln(Q^2/\Lambda^2) = 0$ and the reciprocal is a junk value) nor at $0 < Q < \Lambda$ (where the logarithm is negative, so $A(Q) < 0$ ), nor at $Q \le 0$ . The coefficient appearing in the conclusion is $-2\beta_0$ , a strictly negative number, and the derivative asserted is two-sided.

View graph

The quoted αs(k2)\alpha_s(k^2)αs​(k2) solves the one-loop equation μ dα/dμ=−2β0α2\mu\,d\alpha/d\mu = -2\beta_0\alpha^2μdα/dμ=−2β0​α2

The quoted $\alpha_s(k^2)$ solves the one-loop equation $\mu\,d\alpha/d\mu = -2\beta_0\alpha^2$