Dimensionless power products are unit invariant

Proved

VaryingConstants.powerMonomial_isUnitInvariant

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 $a\in\mathbb R^n$ be a dimensionless exponent vector, i.e. $\sum_i a_iD_{ij}=0$ for every base unit $j$ . Then the power product $\pi_a(x)=\prod_i x_i^{a_i}$ is unit invariant: for every positive configuration $x\in\mathbb R^n_{>0}$ and every positive change of units $s\in\mathbb R^d_{>0}$ ,

\prod_{i=1}^n\Big(x_i\prod_{j=1}^d s_j^{D_{ij}}\Big)^{a_i} \;=\; \prod_{i=1}^n x_i^{a_i}.

This is the precise sense in which a dimensionless combination of constants (such as $\alpha_{\rm EM}=e^2/4\pi\varepsilon_0\hbar c$ or $m_p/m_e$ ) has a value independent of the system of units.

Preamble

import Mathlib
import Definitions.Def_VaryingConstants_units

Formal statement

namespace VaryingConstants

theorem powerMonomial_isUnitInvariant {n d : ℕ} (D : Matrix (Fin n) (Fin d) ℝ)
    (a : Fin n → ℝ) (ha : a ∈ dimensionlessExponents D) :
    IsUnitInvariant D (powerMonomial a) := 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: the values of dimensionless combinations "do 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$ , and every $a\in\mathbb R^n$ satisfying $\sum_{i} a_iD_{ij}=0$ for every $j\in\{0,\dots,d-1\}$ : for every $x\in\mathbb R^n$ with all $x_i>0$ and every $s\in\mathbb R^d$ with all $s_j>0$ ,

\prod_{i}\Big(x_i\prod_j s_j^{D_{ij}}\Big)^{a_i}=\prod_i x_i^{a_i},

all powers being real powers. Degenerate cases included: $n=0$ (both sides are the empty product $1$ ) and $d=0$ (the inner products are $1$ , every $a$ qualifies, and the statement is trivial).

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