Prove2Me

Number of independent dimensionless combinations is n−rank⁡Dn-\operatorname{rank}D

Proved
VaryingConstants.finrank_dimensionlessExponents

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

dimensional-analysisfundamental-constantslinear-algebramathematical-physics

Let D∈Rn×dD\in\mathbb R^{n\times d} be the dimension matrix of nn constants with respect to dd base units. The space of dimensionless exponent vectors

ZD={a∈Rn: ∑i=1naiDij=0  for all j}\mathcal Z_D=\Big\{a\in\mathbb R^n:\ \sum_{i=1}^n a_iD_{ij}=0\ \text{ for all } j\Big\}

has dimension

dim⁡RZD  =  n−rank⁡D.\dim_{\mathbb R}\mathcal Z_D \;=\; n-\operatorname{rank}D .

This is the dimension count of the Buckingham π\pi theorem: from nn constants whose dimensions span an rr-dimensional space one can form exactly n−rn-r independent dimensionless combinations (for c,G,ℏc,G,\hbar plus further constants in mechanical units, r=3r=3).

Preamble
import Mathlib
import Definitions.Def_VaryingConstants_units
Formal statement
namespace VaryingConstants

theorem finrank_dimensionlessExponents {n d : ℕ} (D : Matrix (Fin n) (Fin d) ℝ) :
    Module.finrank ℝ (dimensionlessExponents D) = n - D.rank := 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, pp. 15–17 ("Natural units", "Fundamental parameters"): with three independent constants as units, all other constants become dimensionless; standard dimension count of the Buckingham π theorem (E. Buckingham, Phys. Rev. 4 (1914) 345, https://doi.org/10.1103/PhysRev.4.345).
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,dn,d and every real n×dn\times d matrix DD: the real vector space of all a∈Rna\in\mathbb R^n with ∑iaiDij=0\sum_i a_iD_{ij}=0 for every jj has (finite) dimension equal to n−rank⁡(D)n-\operatorname{rank}(D), where rank⁡\operatorname{rank} is the rank of DD over R\mathbb R and the subtraction is natural-number subtraction (it never truncates here since rank⁡D≤n\operatorname{rank}D\le n, but the statement itself uses truncated subtraction).

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