The one-loop flow in closed form: the inverse-coupling relation

Proved

CouplingConstantRG.isMuRunning_inv_relation

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

differential-equationsmathematical-physicsrenormalization-group

This is the integrated form of the one-loop equation, and the technical heart of the mission: it holds for either sign of the one-loop coefficient and yields both branches of the goal theorem.

Let $b$ be a one-loop coefficient, $\mu_0 > 0$ a reference energy, $T \ge \mu_0$ an upper energy, and let $\alpha$ be a coupling with $\alpha(\mu_0) = \alpha_0 > 0$ satisfying the one-loop equation

\mu\,\frac{d\alpha}{d\mu}(\mu) \;=\; b\,\alpha(\mu)^2

at every $\mu \in [\mu_0, T]$ . Then for every such $\mu$ ,

\alpha(\mu)\,\Big(1 - b\,\alpha_0 \ln(\mu/\mu_0)\Big) \;=\; \alpha_0 .

Written as $1/\alpha(\mu) = 1/\alpha_0 - b \ln(\mu/\mu_0)$ where $\alpha$ does not vanish, this is the familiar statement that the inverse coupling runs linearly in the logarithm of the energy. The multiplicative form above is used because it remains meaningful without first knowing that $\alpha$ stays nonzero. For $b > 0$ the bracket reaches $0$ at $\mu = \mu_0 e^{1/(b\alpha_0)}$ , which is where the Landau pole milestone takes over; for $b < 0$ the bracket grows without bound, which is asymptotic freedom.

Preamble

import Mathlib
import Definitions.Def_CouplingConstantRGDefs

Formal statement

namespace CouplingConstantRG

theorem isMuRunning_inv_relation (b μ₀ T α₀ : ℝ) (α : ℝ → ℝ) (hμ₀ : 0 < μ₀)
    (hT : μ₀ ≤ T) (hα₀ : 0 < α₀) (h₀ : α μ₀ = α₀)
    (hα : IsMuRunning b α (Set.Icc μ₀ T)) :
    ∀ μ ∈ Set.Icc μ₀ T, α μ * (1 - b * α₀ * Real.log (μ / μ₀)) = α₀ := 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 $b, \mu_0, T, \alpha_0$ and a function $\alpha : \mathbb{R} \to \mathbb{R}$ . Assume:

$\mu_0 > 0$ ;
$\mu_0 \le T$ (so the closed interval $[\mu_0, T]$ is nonempty; it is a single point when $T = \mu_0$ );
$\alpha_0 > 0$ ;
$\alpha(\mu_0) = \alpha_0$ ;
$\alpha$ is one-loop running with coefficient $b$ on $[\mu_0, T]$ , i.e. for every $\mu \in [\mu_0,T]$ the function $\alpha$ is differentiable at $\mu$ with $\alpha'(\mu) = b\,\alpha(\mu)^2/\mu$ (two-sided derivative, so the condition at the two endpoints also constrains $\alpha$ just outside the interval).

The conclusion is: for every $\mu \in [\mu_0, T]$ ,

\alpha(\mu)\cdot\Big(1 - b\,\alpha_0\,\ln(\mu/\mu_0)\Big) \;=\; \alpha_0 .

The identity is stated in product form, so it carries no implicit assumption that $\alpha(\mu) \ne 0$ or that the bracket is nonzero; at a scale where the bracket vanished, the identity would force $\alpha_0 = 0$ , contradicting hypothesis 3. The sign of $b$ is unrestricted: $b$ may be negative, zero (in which case the claim reduces to $\alpha(\mu) = \alpha_0$ on the interval) or positive. Nothing is claimed for $\mu$ outside $[\mu_0,T]$ , and $\mu/\mu_0$ is a ratio of positive numbers throughout, so the logarithm is the ordinary one and is $\ge 0$ on the interval.

View graph