Goal: the one-loop running dichotomy in the energy scale

Proved

CouplingConstantRG.running_coupling_mu_dichotomy

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

differential-equationsmathematical-physicsrenormalization-group

The goal of the mission: the sign of the one-loop coefficient decides, completely, how a coupling runs above a reference energy.

Fix a reference energy $\mu_0 > 0$ and a positive coupling value $\alpha_0$ measured there, and consider the one-loop equation in the energy scale,

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

Asymptotically free branch ( $b < 0$ ). Every coupling $\alpha$ with $\alpha(\mu_0) = \alpha_0$ satisfying the equation at all energies $\mu \ge \mu_0$ is given in closed form by

\alpha(\mu) \;=\; \frac{\alpha_0}{1 - b\,\alpha_0 \ln(\mu/\mu_0)}, \qquad \mu \ge \mu_0,

and tends to $0$ as $\mu \to \infty$ . This is asymptotic freedom, with the solution unique rather than merely exhibited.

Landau-pole branch ( $b > 0$ ). No coupling with $\alpha(\mu_0) = \alpha_0$ satisfies the equation on the entire closed interval $[\mu_0,\ \mu_0 e^{1/(b\alpha_0)}]$ , whose upper endpoint is the pole scale the equation itself predicts.

The two branches are the mathematical content of the source's QED and QCD sections, in the variable in which the source defines the beta function. The case $b = 0$ is outside the statement; it is covered by the scale-invariance milestone.

Preamble

import Mathlib
import Definitions.Def_CouplingConstantRGDefs

Formal statement

namespace CouplingConstantRG

theorem running_coupling_mu_dichotomy (b μ₀ α₀ : ℝ) (hμ₀ : 0 < μ₀) (hα₀ : 0 < α₀) :
    (b < 0 → ∀ α : ℝ → ℝ, α μ₀ = α₀ → IsMuRunning b α (Set.Ici μ₀) →
        (∀ μ, μ₀ ≤ μ → α μ = α₀ / (1 - b * α₀ * Real.log (μ / μ₀))) ∧
          Filter.Tendsto α Filter.atTop (nhds 0)) ∧
      (0 < b → ¬ ∃ α : ℝ → ℝ, α μ₀ = α₀ ∧
        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 $\mu_0 > 0$ and $\alpha_0 > 0$ . The claim is a conjunction of two conditional statements about the same $b$ .

First conjunct (hypothesis $b < 0$ ). For every function $\alpha : \mathbb{R} \to \mathbb{R}$ such that $\alpha(\mu_0) = \alpha_0$ and $\alpha$ is one-loop running with coefficient $b$ on the closed half-line $[\mu_0, \infty)$ — i.e. at every $\mu \ge \mu_0$ , $\alpha$ is differentiable with $\alpha'(\mu) = b\,\alpha(\mu)^2/\mu$ — both of the following hold:

for every real $\mu$ with $\mu \ge \mu_0$ ,

\alpha(\mu) \;=\; \frac{\alpha_0}{1 - b\,\alpha_0 \ln(\mu/\mu_0)} ;

$\alpha(\mu) \to 0$ as $\mu \to +\infty$ (convergence of the function along the filter of arbitrarily large real arguments; it constrains $\alpha$ only through its values at large $\mu$ ).

In item 1 the division is the total one: were the denominator zero at some $\mu$ , the right-hand side would be read as $0$ . With $b<0$ , $\alpha_0>0$ and $\mu \ge \mu_0$ the denominator is $1 + |b|\alpha_0\ln(\mu/\mu_0) \ge 1$ , so that degenerate reading does not arise here.

Second conjunct (hypothesis $0 < b$ ). There is no function $\alpha : \mathbb{R} \to \mathbb{R}$ with $\alpha(\mu_0) = \alpha_0$ that is one-loop running with coefficient $b$ on the closed interval $[\mu_0,\ \mu_0 e^{1/(b\alpha_0)}]$ .

Both conjuncts are conditional on the sign of $b$ , so for $b = 0$ the statement asserts nothing; the first conjunct is also vacuous if no function satisfies its hypotheses, and the second is an existence denial over all real functions, with no regularity assumed beyond the differentiability it denies.

View graph