Negative beta function: the coupling decreases with energy

Proved

CouplingConstantRG.betaFunctionMu_neg_strictAntiOn

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

differential-equationsmathematical-physicsrenormalization-group

"In non-abelian gauge theories, the beta function can be negative ... and as a result the QCD coupling decreases at high energies." This milestone is the implication behind that "as a result".

Let $g$ be differentiable at every positive energy scale and suppose its beta function is strictly negative there,

\mu\,\frac{d g}{d\mu}(\mu) \;<\; 0 \qquad\text{for all } \mu > 0 .

Then $g$ is strictly decreasing on $(0, \infty)$ : if $0 < \mu_1 < \mu_2$ then $g(\mu_2) < g(\mu_1)$ .

It is the mirror image of the positive-sign statement, and the general form of the behaviour that the explicit one-loop QCD coupling exhibits; it says nothing yet about the rate of the decrease or about a limit at infinity.

Preamble

import Mathlib
import Definitions.Def_CouplingConstantRGDefs

Formal statement

namespace CouplingConstantRG

theorem betaFunctionMu_neg_strictAntiOn (g : ℝ → ℝ)
    (hg : ∀ μ, 0 < μ → DifferentiableAt ℝ g μ)
    (hβ : ∀ μ, 0 < μ → betaFunctionMu g μ < 0) :
    StrictAntiOn g (Set.Ioi 0) := 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.

Let $g : \mathbb{R} \to \mathbb{R}$ . Assume:

$g$ is differentiable at every real $\mu > 0$ ;
for every real $\mu > 0$ , the quantity $\mu \cdot g'(\mu)$ is strictly less than $0$ .

The conclusion is that $g$ is strictly decreasing on $(0,\infty)$ : for all $\mu_1, \mu_2 > 0$ with $\mu_1 < \mu_2$ , one has $g(\mu_2) < g(\mu_1)$ .

As with the companion statement, nothing is claimed for $\mu \le 0$ , hypothesis 2 is equivalent to $g'(\mu) < 0$ on $(0,\infty)$ because $\mu$ is positive there, and the conclusion asserts strict decrease only, with no rate, no limit at infinity, and no sign or bound on the values of $g$ .

View graph