Beta function in the energy scale $\beta(g)=\mu\,\partial g/\partial\mu$ and one-loop running in $\mu$

Definition

CouplingConstantRGDefs

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

differential-equationsmathematical-physicsrenormalization-group

This file fixes the two objects in which the mission is stated, both written in the energy scale $\mu$ itself rather than in $t = \ln\mu$ .

1. The beta function in the energy scale. For a coupling $g : \mathbb{R} \to \mathbb{R}$ regarded as a function of the energy scale, its beta function is

\beta(g)(\mu) \;=\; \mu \cdot \frac{d g}{d\mu}(\mu),

the quantity the source uses to define the running of a coupling. It is a function of $\mu$ , defined for every real $\mu$ and every $g$ ; at a scale where $g$ has no derivative the underlying derivative operator returns $0$ , so statements below restrict to scales where differentiability is assumed.

2. One-loop running in $\mu$ . For a one-loop coefficient $b \in \mathbb{R}$ , a coupling $\alpha$ and a set $S$ of scales, the predicate " $\alpha$ is one-loop running with coefficient $b$ on $S$ " asserts that at every $\mu \in S$ the coupling is differentiable with

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

The sign of $b$ distinguishes the two regimes the source describes: $b < 0$ is the asymptotically free case of QCD, $b > 0$ the case the source attributes to QED.

These two objects are the model on which every statement of the mission rests. The explicit one-loop strong coupling $\alpha(Q) = 1/(\beta_0 \ln(Q^2/\Lambda^2))$ is not redefined here: the mission reuses the published platform definition for it.

Formalization Note The derivative in the one-loop predicate is the two-sided derivative at each point of $S$ , so the predicate also constrains the coupling in a neighbourhood of an endpoint of an interval; the division by $\mu$ is harmless on the sets of positive scales used throughout.

Definition code

import Mathlib

namespace CouplingConstantRG

/-- The beta function of a running coupling `g` in the energy scale `μ`:
`β(g)(μ) = μ * ∂g/∂μ`. -/
noncomputable def betaFunctionMu (g : ℝ → ℝ) (μ : ℝ) : ℝ := μ * deriv g μ

/-- `IsMuRunning b α s` says that on the set of energy scales `s` the coupling `α`
obeys the one-loop renormalization-group equation written in the energy scale `μ`,
`μ * dα/dμ = b * α ^ 2`, i.e. `dα/dμ = b * α ^ 2 / μ`. -/
def IsMuRunning (b : ℝ) (α : ℝ → ℝ) (s : Set ℝ) : Prop :=
  ∀ μ ∈ s, HasDerivAt α (b * α μ ^ 2 / μ) μ

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.

The file declares two objects in the namespace CouplingConstantRG, both taking real arguments.

The first assigns to a function $g : \mathbb{R} \to \mathbb{R}$ and a real number $\mu$ the value

\mu \cdot (\text{derivative of } g \text{ at } \mu).

It is total: it is defined for every real $\mu$ , including $\mu \le 0$ , and for every $g$ , including functions that are not differentiable at $\mu$ — in that case the derivative operator used here yields $0$ by convention, so the value of the expression is $0$ rather than undefined.

The second is a proposition depending on a real number $b$ , a function $\alpha : \mathbb{R} \to \mathbb{R}$ and a set $S \subseteq \mathbb{R}$ . It asserts: for every $\mu \in S$ , the function $\alpha$ has derivative exactly

\frac{b \cdot \alpha(\mu)^2}{\mu}

at the point $\mu$ , in the two-sided sense (the derivative is taken in the full real line, not relative to $S$ ; so if $S$ is a closed interval the condition at an endpoint still speaks about behaviour on both sides of it). Degenerate readings: if $S$ is empty the proposition holds vacuously for every $b$ and $\alpha$ ; if $0 \in S$ the quotient divides by zero, which in this setting evaluates to $0$ , so the condition at $\mu = 0$ reads " $\alpha$ has derivative $0$ at $0$ "; if $b = 0$ the condition says $\alpha$ has derivative $0$ at every point of $S$ . No positivity, continuity, or integrability is assumed of $\alpha$ beyond the stated pointwise differentiability.

Human review

Endorsed by Shuze Chen · Oct 8, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Beta function in the energy scale β(g)=μ ∂g/∂μ\beta(g)=\mu\,\partial g/\partial\muβ(g)=μ∂g/∂μ and one-loop running in μ\muμ

Beta function in the energy scale $\beta(g)=\mu\,\partial g/\partial\mu$ and one-loop running in $\mu$