The seven defining constants span the dimensions of the SI
ProvedSI.dim_basisThe dimension map from monomials in the seven defining constants to dimensional products is bijective: every dimension of the SI is a unique integral monomial in the defining constants. This is the formal content of the statement of section 2.2 that the SI is defined by seven constants whose units include both base and derived units, and that any unit of the SI can be written through products or quotients of the defining constants. Equivalently, the dimension-exponent matrix of the constants - read off from the units in which their values are fixed (Hz, m s⁻¹, J s, C, J K⁻¹, mol⁻¹, lm W⁻¹) - is unimodular.
import Mathlib import Definitions.Def_SI_dim import Definitions.Def_SI_units import Definitions.Def_SI_qmodel
/-! # The dimension map of the defining constants is bijective Section 2.2 of the SI Brochure states that any unit of the SI can be written through products or quotients of the seven defining constants. In the additive form of the dimension space, the monomial in the defining constants with exponent vector v has dimension dimOfExpo v, so this completeness claim is exactly the surjectivity of dimOfExpo; injectivity says that the expression is unique. Both follow from the fact that the dimension-exponent matrix of the seven defining constants (section 2.2, Table 1: Δν_Cs in Hz, c in m s⁻¹, h in J s, e in C, k in J K⁻¹, N_A in mol⁻¹, K_cd in lm W⁻¹) is unimodular, which is the arithmetic content of the completeness of the seven defining constants. This milestone is proved on the way to the goal theorem `SI.si_complete`. -/ namespace SI /-- The seven defining constants span the dimension space of the SI over the integers: the dimension map dimOfExpo, from monomials in the defining constants to dimensional products, is bijective. In particular every dimension of the SI is a unique integral monomial in the defining constants (section 2.2). -/ theorem dim_basis : Function.Bijective dimOfExpo := by sorry end SI
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The formal statement asserts that the function dimOfExpo, which maps the exponent vector of a monomial in the seven defining constants to its dimension vector, is bijective. Since dimOfExpo is the linear map given by the integer matrix whose columns are the dimensions of Δν_Cs, c, h, e, k, N_A and K_cd, bijectivity over the integers is exactly the unimodularity of that matrix. The statement renders the intended milestone faithfully: completeness and uniqueness of the expression of SI dimensions through the defining constants. Nothing about numerical values, real numbers, or physical measurement is claimed here.