Values in natural units do not depend on the starting system of units

Proved

VaryingConstants.natural_unit_values_independent_of_units

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

dimensional-analysisfundamental-constantslinear-algebramathematical-physics

Let $D\in\mathbb R^{n\times d}$ and let $e_1,\dots,e_d$ be constants with $\det D_e\neq0$ (as in the natural-units milestone). Let $x\in\mathbb R^n_{>0}$ and let $r\in\mathbb R^d_{>0}$ be any change of units, giving the configuration $r\cdot x$ . If $s$ is a system of natural units for $x$ and $s'$ is a system of natural units for $r\cdot x$ , then

s'\cdot(r\cdot x) \;=\; s\cdot x .

So the numerical value of every constant expressed in natural units is the same whatever system of units one started from: in natural units all constants are dimensionless numbers.

Preamble

import Mathlib
import Definitions.Def_VaryingConstants_units

Formal statement

namespace VaryingConstants

theorem natural_unit_values_independent_of_units {n d : ℕ} (D : Matrix (Fin n) (Fin d) ℝ)
    (e : Fin d → Fin n) (he : (D.submatrix e id).det ≠ 0)
    (x : Fin n → ℝ) (hx : IsPositive x) (r : Fin d → ℝ) (hr : IsPositive r)
    (s s' : Fin d → ℝ) (hs : IsNaturalUnitsFor D e x s)
    (hs' : IsNaturalUnitsFor D e (unitRescale D r x) s') :
    unitRescale D s' (unitRescale D r x) = 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: "Once a set of three independent constants has been chosen as natural units, then all other constants are dimensionless quantities. The values of these combinations of constants does not depend on ... the definition of the 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$ , every $e:\{0,\dots,d-1\}\to\{0,\dots,n-1\}$ with $\det(D_{e(j),k})_{j,k}\neq0$ , every $x\in\mathbb R^n$ with all $x_i>0$ , every $r\in\mathbb R^d$ with all $r_k>0$ , and all $s,s'\in\mathbb R^d$ such that (a) all $s_k>0$ and $x_{e(j)}\prod_k s_k^{D_{e(j),k}}=1$ for every $j$ , and (b) all $s'_k>0$ and $y_{e(j)}\prod_k (s'_k)^{D_{e(j),k}}=1$ for every $j$ , where $y_i=x_i\prod_k r_k^{D_{ik}}$ : for every $i$ ,

y_i\prod_k (s'_k)^{D_{ik}} \;=\; x_i\prod_k s_k^{D_{ik}} .

All powers are real powers.

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