Positive beta function: the coupling increases with energy

Proved

CouplingConstantRG.betaFunctionMu_pos_strictMonoOn

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

differential-equationsmathematical-physicsrenormalization-group

"If a beta function is positive, the corresponding coupling increases with increasing energy." This milestone is that sentence, stated for an arbitrary coupling.

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

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

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

Together with the companion statement for a negative beta function, this is the qualitative dictionary the source uses to pass from the sign of $\beta$ to the direction in which a coupling runs — the step that turns the perturbative computation of a sign into the physical statements about QED and QCD.

Preamble

import Mathlib
import Definitions.Def_CouplingConstantRGDefs

Formal statement

namespace CouplingConstantRG

theorem betaFunctionMu_pos_strictMonoOn (g : ℝ → ℝ)
    (hg : ∀ μ, 0 < μ → DifferentiableAt ℝ g μ)
    (hβ : ∀ μ, 0 < μ → 0 < betaFunctionMu g μ) :
    StrictMonoOn 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 greater than $0$ .

The conclusion is that $g$ is strictly increasing on the open half-line $(0,\infty)$ : for all $\mu_1, \mu_2$ in that half-line with $\mu_1 < \mu_2$ , one has $g(\mu_1) < g(\mu_2)$ .

Since the hypotheses only constrain $\mu > 0$ , the conclusion compares values of $g$ only at strictly positive arguments; $g$ on $(-\infty, 0]$ is unconstrained. Because $\mu > 0$ , hypothesis 2 is equivalent to $g'(\mu) > 0$ for all $\mu > 0$ . The inequality in the conclusion is strict, and the ordering of the arguments is strict as well, so nothing is asserted when $\mu_1 = \mu_2$ .

View graph