The QCD scale $\Lambda$ is determined by the coupling at one energy

Proved

CouplingConstantRG.existsUnique_qcdScale

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

differential-equationsmathematical-physicsrenormalization-group

The source stresses that "the actual value of the coupling constant is only defined at a given energy scale", quotes $\alpha_s(M_Z^2) = 0.1179 \pm 0.0010$ at the $Z$ mass, and treats $\Lambda$ — the QCD scale — as the parameter carrying that information. This milestone is the statement that the two descriptions are equivalent: one measurement fixes $\Lambda$ , and fixes it uniquely.

Let $\beta_0 > 0$ be the one-loop coefficient, $\mu_0 > 0$ a reference energy, and $\alpha_0 > 0$ the value of the strong coupling measured there. Then there is exactly one scale $\Lambda$ with

0 < \Lambda < \mu_0 \qquad\text{and}\qquad \frac{1}{\beta_0 \ln(\mu_0^2/\Lambda^2)} \;=\; \alpha_0 .

This is the dimensional-transmutation step: a dimensionless measured number at a given energy is traded for a dimensionful scale, below the measurement energy, which then determines the coupling at every energy above it.

Preamble

import Mathlib
import Definitions.Def_CouplingConstantDefs
import Definitions.Def_CouplingConstantRGDefs

Formal statement

namespace CouplingConstantRG

theorem existsUnique_qcdScale (β₀ μ₀ α₀ : ℝ) (hβ₀ : 0 < β₀) (hμ₀ : 0 < μ₀)
    (hα₀ : 0 < α₀) :
    ∃! Λ : ℝ, 0 < Λ ∧ Λ < μ₀ ∧ CouplingConstant.alphaOneLoop β₀ Λ μ₀ = α₀ := 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 $\beta_0, \mu_0, \alpha_0$ with $\beta_0 > 0$ , $\mu_0 > 0$ and $\alpha_0 > 0$ .

The claim asserts the existence of exactly one real number $\Lambda$ satisfying the conjunction of three conditions:

$\Lambda > 0$ ;
$\Lambda < \mu_0$ ;
$\dfrac{1}{\beta_0 \ln(\mu_0^{2}/\Lambda^{2})} = \alpha_0$ , where the left-hand side is the previously published one-loop coupling function evaluated at the energy $\mu_0$ with parameters $\beta_0$ and $\Lambda$ .

"Exactly one" is the strong reading: some $\Lambda$ satisfies all three conditions, and any real number satisfying all three equals it. Uniqueness is asserted only within the constrained range $0 < \Lambda < \mu_0$ ; a value of $\Lambda$ outside that range that happened to satisfy condition 3 would not contradict the statement. Note also that condition 3 is an exact equality, not an approximation, and that $\alpha_0$ is assumed strictly positive, which excludes the degenerate target value $0$ (not attainable by a reciprocal in any case).

View graph

The QCD scale Λ\LambdaΛ is determined by the coupling at one energy

The QCD scale $\Lambda$ is determined by the coupling at one energy