Natural units exist and are unique for dimensionally independent constants

Proved

VaryingConstants.natural_units_exists_unique

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 choose $d$ constants $e_1,\dots,e_d$ whose dimensions are independent, i.e. the $d\times d$ submatrix $D_e=(D_{e_j,k})_{j,k}$ satisfies $\det D_e\neq0$ . Then for every positive configuration $x\in\mathbb R^n_{>0}$ there exists a unique $s\in\mathbb R^d$ with $s_k>0$ for all $k$ and

x_{e_j}\prod_{k=1}^d s_k^{D_{e_j,k}} \;=\;1\qquad (j=1,\dots,d).

In words: $d$ dimensionally independent constants define a unique system of natural units in which each of them has numerical value $1$ (Stoney units from $G,e,c$ ; Planck units from $c,G,\hbar$ ; Bohr units from $e,m_e,h$ ).

Formalization Note The chosen constants are a map $e:\mathrm{Fin}\,d\to\mathrm{Fin}\,n$ ; injectivity is implied by $\det D_e\neq0$ .

Preamble

import Mathlib
import Definitions.Def_VaryingConstants_units

Formal statement

namespace VaryingConstants

theorem natural_units_exists_unique {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) :
    ∃! s : Fin d → ℝ, IsNaturalUnitsFor D e x s := 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 "Natural units", pp. 15–16: "these three basic units can be defined in terms of 3 independent constants"; Stoney units

(G,e,c)

and Planck units

(c,G,\hbar)

for which "the numerical value of

G

e

and

c

is 1".

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 map $e:\{0,\dots,d-1\}\to\{0,\dots,n-1\}$ such that the $d\times d$ matrix with $(j,k)$ entry $D_{e(j),k}$ has nonzero determinant, and every $x\in\mathbb R^n$ with all $x_i>0$ : there exists exactly one $s\in\mathbb R^d$ such that (i) $s_k>0$ for all $k$ and (ii) for every $j$ , $x_{e(j)}\prod_k s_k^{D_{e(j),k}}=1$ (real powers). Uniqueness is among all real vectors satisfying (i) and (ii). For $d=0$ the determinant of the empty matrix is $1$ , and the unique $s$ is the empty vector.

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