Buckingham $\pi$ theorem for physical constants (goal)

Proved

VaryingConstants.buckingham_pi

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

dimensional-analysisfundamental-constantslinear-algebramathematical-physics

Let $D\in\mathbb R^{n\times d}$ be the dimension matrix of $n$ constants with respect to $d$ base units, and put $k=n-\operatorname{rank}D$ . Then there exist exponent vectors $a^{(1)},\dots,a^{(k)}\in\mathbb R^n$ such that

each $a^{(l)}$ is dimensionless: $\sum_i a^{(l)}_iD_{ij}=0$ for all $j$ ;
$a^{(1)},\dots,a^{(k)}$ are linearly independent;
for every unit-invariant observable $f:\mathbb R^n\to\mathbb R$ there is a function $F:\mathbb R^k\to\mathbb R$ with

f(x)=F\big(\pi_1(x),\dots,\pi_k(x)\big),\qquad \pi_l(x)=\prod_{i=1}^n x_i^{a^{(l)}_i},

for every positive configuration $x\in\mathbb R^n_{>0}$ .

Every quantity that does not depend on the choice of units is a function of $n-\operatorname{rank}D$ independent dimensionless combinations of the constants. This is the mathematical statement behind Uzan's §2.1: the physically meaningful parameters are the dimensionless numbers (such as $\alpha_{\rm EM}$ or $m_p/m_e$ ), and only their variation is observable.

Formalization Note No regularity of $f$ or $F$ is required; $f$ is only constrained on positive configurations.

Preamble

import Mathlib
import Definitions.Def_VaryingConstants_units

Formal statement

namespace VaryingConstants

theorem buckingham_pi {n d : ℕ} (D : Matrix (Fin n) (Fin d) ℝ) :
    ∃ a : Fin (n - D.rank) → (Fin n → ℝ),
      (∀ l, a l ∈ dimensionlessExponents D) ∧ LinearIndependent ℝ a ∧
      ∀ f : (Fin n → ℝ) → ℝ, IsUnitInvariant D f →
        ∃ F : (Fin (n - D.rank) → ℝ) → ℝ,
          ∀ x : Fin n → ℝ, IsPositive x → f x = F (fun l => powerMonomial (a l) x) := by sorry

end VaryingConstants

Source

J.-P. Uzan, "Varying Constants, Gravitation and Cosmology", Living Rev. Relativity 14 (2011) 2, http://www.livingreviews.org/lrr-2011-2, §2.1.1–2.1.2, pp. 14–17 (dimensionless combinations of constants, natural units, "only the variation of dimensionless constants can be measured"); classical statement: E. Buckingham, Phys. Rev. 4 (1914) 345, https://doi.org/10.1103/PhysRev.4.345.

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back. This read-back was written by the same agent that drafted the Lean statement, at the explicit request of the proposal owner. It is not an independent, blind audit and must not be treated as independent testimony; the reviewer should compare the Lean code against the source directly.

For all natural numbers $n,d$ and every real $n\times d$ matrix $D$ , writing $k=n-\operatorname{rank}(D)$ (natural-number subtraction, rank over $\mathbb R$ ), there exist vectors $a^{(0)},\dots,a^{(k-1)}\in\mathbb R^n$ such that:

for every $l$ and every $j$ , $\sum_i a^{(l)}_iD_{ij}=0$ ;
the family $(a^{(l)})_l$ is linearly independent over $\mathbb R$ ;
for every function $f:\mathbb R^n\to\mathbb R$ satisfying " $f(z')=f(z)$ whenever all $z_i>0$ , all $s_j>0$ and $z'_i=z_i\prod_j s_j^{D_{ij}}$ ", there exists a function $F:\mathbb R^k\to\mathbb R$ such that for every $x\in\mathbb R^n$ with all $x_i>0$ ,

f(x)=F\Big(\big(\textstyle\prod_i x_i^{a^{(l)}_i}\big)_{l=0}^{k-1}\Big)

(real powers). The family $a$ is chosen before $f$ (it is the same for all $f$ ); $F$ may depend on $f$ and is not required to be continuous or measurable. When $k=0$ the family is empty and $F$ is a function of the empty tuple, so the conclusion says $f$ is constant on positive configurations.

Human review

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

View graph

Buckingham π\piπ theorem for physical constants (goal)

Buckingham $\pi$ theorem for physical constants (goal)