Only variations of dimensionless constants can be measured

Proved

VaryingConstants.only_dimensionless_variations_measurable

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 a dimension matrix and let $f:\mathbb R^n\to\mathbb R$ be a unit-invariant observable: $f(s\cdot x)=f(x)$ for all positive $x$ and all positive changes of units $s$ . If $x,y\in\mathbb R^n_{>0}$ satisfy

\prod_i x_i^{a_i}=\prod_i y_i^{a_i}\qquad\text{for every } a\in\mathcal Z_D,

then

f(x)=f(y).

This is the formal content of Uzan's remark that only the variation of dimensionless constants can be measured: a change of the dimensional constants that leaves every dimensionless combination fixed is invisible to every measurement outcome.

Preamble

import Mathlib
import Definitions.Def_VaryingConstants_units

Formal statement

namespace VaryingConstants

theorem only_dimensionless_variations_measurable {n d : ℕ} (D : Matrix (Fin n) (Fin d) ℝ)
    (f : (Fin n → ℝ) → ℝ) (hf : IsUnitInvariant D f)
    (x y : Fin n → ℝ) (hx : IsPositive x) (hy : IsPositive y)
    (hxy : ∀ a ∈ dimensionlessExponents D, powerMonomial a x = powerMonomial a y) :
    f x = f y := 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.2 "Constants and metrology", p. 14: "This implies that only the variation of dimensionless constants can be measured".

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$ , every real $n\times d$ matrix $D$ , and every function $f:\mathbb R^n\to\mathbb R$ such that $f(z')=f(z)$ whenever $z\in\mathbb R^n$ has all $z_i>0$ , $s\in\mathbb R^d$ has all $s_j>0$ , and $z'_i=z_i\prod_j s_j^{D_{ij}}$ (no regularity of $f$ is assumed): for all $x,y\in\mathbb R^n$ with all entries positive such that $\prod_i x_i^{a_i}=\prod_i y_i^{a_i}$ for every $a\in\mathbb R^n$ with $\sum_ia_iD_{ij}=0$ for all $j$ , we have $f(x)=f(y)$ .

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