Equal dimensionless combinations $\iff$ related by a change of units

Proved

VaryingConstants.same_dimensionless_iff_unit_change

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 $x,y\in\mathbb R^n_{>0}$ be two positive configurations of the constants. Then

\Big(\forall a\in\mathcal Z_D:\ \prod_i x_i^{a_i}=\prod_i y_i^{a_i}\Big) \iff \exists\, s\in\mathbb R^d_{>0}:\ y_i=x_i\prod_j s_j^{D_{ij}}\ \ \forall i .

The direction $(\Rightarrow)$ is Uzan's statement that a variation of the constants that leaves all dimensionless numbers unchanged is just a redefinition of units; $(\Leftarrow)$ says that a redefinition of units leaves all dimensionless numbers unchanged.

Preamble

import Mathlib
import Definitions.Def_VaryingConstants_units

Formal statement

namespace VaryingConstants

theorem same_dimensionless_iff_unit_change {n d : ℕ} (D : Matrix (Fin n) (Fin d) ℝ)
    (x y : Fin n → ℝ) (hx : IsPositive x) (hy : IsPositive y) :
    (∀ a ∈ dimensionlessExponents D, powerMonomial a x = powerMonomial a y) ↔
      ∃ s : Fin d → ℝ, IsPositive s ∧ y = unitRescale D s 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 "Fundamental parameters", p. 17: "any variation of constants that will leave these numbers unaffected is actually just a redefinition of units."

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 all $x,y\in\mathbb R^n$ with all $x_i>0$ and all $y_i>0$ , the following are equivalent:

(A) for every $a\in\mathbb R^n$ with $\sum_i a_iD_{ij}=0$ for all $j$ , $\prod_i x_i^{a_i}=\prod_i y_i^{a_i}$ (real powers);

(B) there is $s\in\mathbb R^d$ with all $s_j>0$ such that $y_i=x_i\prod_j s_j^{D_{ij}}$ for every $i$ .

Edge cases: if $D=0$ (or $d=0$ ), every $a$ qualifies in (A) and the rescaling in (B) is the identity, so both sides say $x=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

Equal dimensionless combinations ⟺ \iff⟺ related by a change of units

Equal dimensionless combinations $\iff$ related by a change of units