Vanishing beta function implies a scale-invariant coupling

Proved

CouplingConstantRG.betaFunctionMu_eq_zero_scale_invariant

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

differential-equationsmathematical-physicsrenormalization-group

"If the beta functions of a quantum field theory vanish, then the theory is scale-invariant." This milestone is that sentence for a single coupling.

Let $g$ be a coupling that is differentiable at every positive energy scale and whose beta function vanishes there,

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

Then $g$ takes the same value at any two positive scales: $g(\mu_1) = g(\mu_2)$ for all $\mu_1, \mu_2 > 0$ .

The statement is about an arbitrary coupling, not only a one-loop one, so it isolates exactly the implication the source states: no running at any scale means no scale dependence at all. Nothing is asserted about $\mu \le 0$ , which is not a physical energy scale.

Preamble

import Mathlib
import Definitions.Def_CouplingConstantRGDefs

Formal statement

namespace CouplingConstantRG

theorem betaFunctionMu_eq_zero_scale_invariant (g : ℝ → ℝ)
    (hg : ∀ μ, 0 < μ → DifferentiableAt ℝ g μ)
    (hβ : ∀ μ, 0 < μ → betaFunctionMu g μ = 0) :
    ∀ μ₁ μ₂ : ℝ, 0 < μ₁ → 0 < μ₂ → g μ₁ = g μ₂ := 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}$ be a function. Assume:

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

The conclusion is: for all real $\mu_1, \mu_2$ with $\mu_1 > 0$ and $\mu_2 > 0$ , $g(\mu_1) = g(\mu_2)$ .

Three points about the scope. The hypotheses and the conclusion concern only strictly positive arguments: $g$ may be arbitrary, and arbitrarily non-differentiable, on $(-\infty, 0]$ , and no claim is made about its values there. Since $\mu > 0$ in hypothesis 2, the equation $\mu \cdot g'(\mu) = 0$ is equivalent to $g'(\mu) = 0$ . The conclusion is the statement that $g$ is constant on the open half-line $(0,\infty)$ , phrased as equality of values at any two such points; it does not name the common value.

View graph