Landau pole: no one-loop solution reaches the pole scale when $b>0$

Proved

CouplingConstantRG.landau_pole_mu

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

differential-equationsmathematical-physicsrenormalization-group

"The perturbative beta function tells us that the coupling continues to increase, and QED becomes strongly coupled at high energy. In fact the coupling apparently becomes infinite at some finite energy. This phenomenon ... is called the Landau pole."

Let $b > 0$ be a one-loop coefficient of the QED sign, $\mu_0 > 0$ a reference energy and $\alpha_0 > 0$ the coupling there. Then there is no function $\alpha$ with $\alpha(\mu_0) = \alpha_0$ satisfying

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

at every energy of the closed interval

\Big[\mu_0,\; \mu_0\,e^{1/(b\alpha_0)}\Big].

The upper endpoint is the pole scale predicted by the one-loop equation itself, namely the energy at which the inverse coupling $1/\alpha_0 - b\ln(\mu/\mu_0)$ reaches zero. Stating the pole as non-existence of a solution, rather than as a divergence of one chosen formula, is what makes it an obstruction: no candidate running coupling of any kind survives to that energy.

Preamble

import Mathlib
import Definitions.Def_CouplingConstantRGDefs

Formal statement

namespace CouplingConstantRG

theorem landau_pole_mu (b μ₀ α₀ : ℝ) (hb : 0 < b) (hμ₀ : 0 < μ₀) (hα₀ : 0 < α₀) :
    ¬ ∃ α : ℝ → ℝ, α μ₀ = α₀ ∧
      IsMuRunning b α (Set.Icc μ₀ (μ₀ * Real.exp (1 / (b * α₀)))) := 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, \alpha_0$ with $b > 0$ , $\mu_0 > 0$ , $\alpha_0 > 0$ , and set

T \;=\; \mu_0\,e^{1/(b\alpha_0)} ,

a real number strictly greater than $\mu_0$ (the exponent $1/(b\alpha_0)$ is positive).

The claim is a negation: there is no function $\alpha : \mathbb{R} \to \mathbb{R}$ such that both

$\alpha(\mu_0) = \alpha_0$ , and
$\alpha$ is one-loop running with coefficient $b$ on the closed interval $[\mu_0, T]$ — that is, at every $\mu$ in that interval $\alpha$ is differentiable (two-sided) with $\alpha'(\mu) = b\,\alpha(\mu)^2/\mu$ .

Nothing is asserted about solutions on smaller intervals $[\mu_0, T']$ with $T' < T$ , nor about functions failing the initial condition, nor about $b \le 0$ or $\alpha_0 \le 0$ . The quantification is over arbitrary real-valued functions on the whole line: no continuity, positivity or measurability is presupposed beyond the differentiability demanded on $[\mu_0,T]$ , and a candidate is free to behave arbitrarily outside a neighbourhood of that interval.

View graph

Landau pole: no one-loop solution reaches the pole scale when b>0b>0b>0

Landau pole: no one-loop solution reaches the pole scale when $b>0$