$\mu\,\partial g/\partial\mu = \partial g/\partial \ln\mu$

Proved

CouplingConstantRG.betaFunctionMu_eq_deriv_log

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

differential-equationsmathematical-physicsrenormalization-group

The source defines the beta function by

\beta(g) \;=\; \mu\,\frac{\partial g}{\partial \mu} \;=\; \frac{\partial g}{\partial \ln \mu},

asserting in one line that two different derivatives agree. This milestone is that identity.

Let $g$ be a coupling regarded as a function of the energy scale, let $\mu > 0$ be a scale at which $g$ is differentiable, and let $\tilde g(t) = g(e^{t})$ be the same coupling regarded as a function of $t = \ln \mu$ . Then

\mu\,\frac{d g}{d \mu}(\mu) \;=\; \frac{d \tilde g}{d t}(\ln \mu).

The identity is what lets the two conventional forms of the renormalization-group equation — in the scale and in its logarithm — be used interchangeably, and it is the bridge between the statements of this mission and formalizations written in the logarithmic variable.

Preamble

import Mathlib
import Definitions.Def_CouplingConstantRGDefs

Formal statement

namespace CouplingConstantRG

theorem betaFunctionMu_eq_deriv_log (g : ℝ → ℝ) (μ : ℝ) (hμ : 0 < μ)
    (hg : DifferentiableAt ℝ g μ) :
    betaFunctionMu g μ = deriv (fun t : ℝ => g (Real.exp t)) (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.

For a function $g : \mathbb{R} \to \mathbb{R}$ and a real number $\mu$ , assume:

$\mu > 0$ ;
$g$ is differentiable at the point $\mu$ (in the real sense, two-sided).

Under these assumptions the claim is the equality of two real numbers:

\mu \cdot g'(\mu) \;=\; h'(\ln \mu), \qquad\text{where } h(t) = g(e^{t}).

On the left, $g'(\mu)$ is the derivative of $g$ at $\mu$ . On the right, $h$ is the composite of the real exponential with $g$ , $h'$ is its derivative, evaluated at the natural logarithm of $\mu$ ; since $\mu > 0$ , this logarithm is the ordinary one (the convention that assigns the value $0$ to the logarithm at non-positive arguments is not in play).

No hypotheses beyond positivity of $\mu$ and differentiability of $g$ at $\mu$ are imposed: $g$ is an arbitrary real function, not assumed continuous, monotone, positive, or differentiable anywhere else.

View graph

μ ∂g/∂μ=∂g/∂ln⁡μ\mu\,\partial g/\partial\mu = \partial g/\partial \ln\muμ∂g/∂μ=∂g/∂lnμ

$\mu\,\partial g/\partial\mu = \partial g/\partial \ln\mu$