API: Make Dimension's base-dimension set parametric

[NicolasRouquette]

Details

The details of this issue are not yet completed. The issue is here to track the progress of the API specified by the title. Parts of this API may already be included within the project. There are a number of things we need to specify, help in specifying these points is appreciated.

Key data structure

Physlib.Units.Dimension models a physical dimension as a fixed record of five rational exponents over a hardwired basis — length, time, mass, charge, temperature:

-- Physlib/Units/Dimension.lean  (rev b0070e4, inputRev v4.31.0)
/-- The foundational dimensions.
  Defined in the order ⟨length, time, mass, charge, temperature⟩ -/
structure Dimension where
  length : ℚ
  time : ℚ
  mass : ℚ
  charge : ℚ
  temperature : ℚ

The exponent type is already ℚ (there is an instance : Pow Dimension ℚ), which is great. What is baked in is the basis itself — its rank (5) and the identity/choice of its generators. That single choice is more opinionated than it looks, and it blocks several standard quantity systems. This is a feature request / design discussion, not a bug: could Dimension be made parametric in its generating set, with the current SI-style basis recovered as one instance?

Why the fixed basis is limiting

Judged against the ISQ's seven base quantities (ISO/IEC 80000-1) and the SI base units (VIM, 4th ed. 2nd Committee Draft, §1.19), the hardwired basis is not a neutral default: it already embeds specific metrological commitments, and it cannot express others that are entirely standard:

1. Charge vs. electric current. The SI/ISQ electromagnetic base quantity is electric current (the ampere); Dimension instead uses charge. The two are inter-derivable (I = Q/T), so which one is "base" is exactly a choice of generator — and it's fixed here.

2. No amount-of-substance or luminous-intensity axis. The ISQ has seven base quantities; Dimension has five, omitting amount of substance (mole, N) and luminous intensity (candela, J). Downstream users who want the full ISQ basis, or who want to argue those two shouldn't be independent, currently have no way to select either stance — the answer is fixed by the record.

3. Non-SI systems are inexpressible.

   • Gaussian–CGS uses only three generators (length, mass, time) and derives electric charge as M^(1/2)·L^(3/2)·T^(-1). Rational exponents already make that vector representable, but the five-field record keeps charge as an independent fourth axis, so it cannot impose the Gaussian identification (charge is not independent there).
   • Natural units set c = ħ = 1, collapsing generators (e.g. length becomes inverse mass) — an identification the fixed basis cannot make.

4. The angle-dimension proposals. A decade of Metrologia papers argues for promoting angle to a base dimension of its own — with solid angle as its square (dimension A², so sr = rad²) — so the algebra itself rules out spurious factors of 2π:

   • Quincey, The range of options for handling plane angle and solid angle within a system of units, Metrologia 53 (2016) 840, doi:10.1088/0026-1394/53/2/840
   • Mills, On the units radian and cycle for the quantity plane angle, Metrologia 53 (2016) 991, doi:10.1088/0026-1394/53/3/991
   • Quincey, Mohr & Phillips, Angles are inherently neither length ratios nor dimensionless, Metrologia 56 (2019) 043001, doi:10.1088/1681-7575/ab27d7
   • Kalinin, On the status of plane and solid angles in the International System of Units (SI), Metrologia 56 (2019) 065009, doi:10.1088/1681-7575/ab3fbf
   • Leonard, Proposal for the dimensionally consistent treatment of angle and solid angle by the SI, Metrologia 58 (2021) 052001, doi:10.1088/1681-7575/abe0fc
   • Mohr, Shirley, Phillips & Trott, On the dimension of angles and their units, Metrologia 59 (2022) 053001, doi:10.1088/1681-7575/ac7bc2

   None of this is expressible without changing Dimension's basis: adding an angle generator (and giving solid angle the exponent 2 over it) is precisely a change of generating set.

Need

Abstract the basis behind a (finite) index type, so a dimension is a ℚ-valued vector over a chosen generator set, and recover the present type as one instantiation. Roughly:

/-- A dimension over a chosen finite set `B` of base dimensions. -/
abbrev Dimension (B : Type) [Fintype B] [DecidableEq B] := B → ℚ   -- or  B →₀ ℚ

with the group/module structure obtained essentially for free from Mathlib (Pi/Finsupp already give CommGroup/ℚ-module instances), and PhysLib's current basis recovered as Dimension PhyslibBase for a concrete PhyslibBase enum (named neutrally — as point 1 above notes, that basis is charge-based, so it is not the SI/ISQ set). Gaussian, NaturalUnits, a true ISQBase, or an angle-augmented basis become other instances rather than forks of the file.

This is not an exotic framing: the metrology literature already describes a unit system as exactly a set of independent, dimensionally orthogonal base units modified by conventions (Quincey & Brown, A clearer approach for defining unit systems, Metrologia 54 (2017) 454, doi:10.1088/1681-7575/aa7160) — i.e. a choice of B together with the derived identities (c = ħ = 1, charge as M^(1/2)L^(3/2)T^(-1), …) that a convention imposes. Making Dimension parametric in B is the type-level form of that same picture.

I recognize this is an API change with real cost. The five-base choice is hardwired twice — in Dimension and, in parallel, in UnitChoices / UnitChoices.dimScale (which folds over the same five named fields) — so parametrizing Dimension alone is not enough; the unit-side twin has to move with it. The good news is that the surface is contained: the Dimension type and the HasDim / CarriesDimension carrier layer live almost entirely within Physlib/Units/ (~12 files), not scattered through the physics library. A migration-friendly path could be to introduce the parametric core alongside the current one — or make Dimension a thin structure wrapping Dimension PhyslibBase, keeping the named projections and @[simp] lemmas — so existing Units/ code compiles unchanged while a new development can pick a different basis. I'm happy to help prototype if there's interest.

Open questions for maintainers:

• One basis, or many? HasDim M gives a single Dimension, so a development effectively shares one basis. Is the intended model a single default basis (PhyslibBase) for the library, with parametricity available to separate developments — or per-type / mixed bases (which then need change-of-basis maps to interoperate)?
• Replace or extend? Should the parametric type replace Dimension, or sit beside it (say, Dimension') behind a deprecation window?
• B → ℚ or B →₀ ℚ? A total function over a Fintype B (simplest; matches the current fixed-rank record) or finitely-supported functions (allowing an open-ended basis)?
• Conventions. Systems like natural units impose identities among generators (c = ħ = 1). Are these best modelled by choosing a smaller B and deriving the rest, or by an explicit relation/quotient layer on top of a fixed B?

Prototype

A self-contained sketch (compiles as-is against a current Mathlib) — the commutative-group structure really does come for free, and a different basis with rational exponents just works:

import Mathlib

/-- A dimension over a chosen generating set `B`: a `ℚ`-valued exponent vector,
written multiplicatively so that composing dimensions adds exponents. -/
abbrev Dimension (B : Type) := Multiplicative (B → ℚ)

namespace Dimension
variable {B : Type}

-- The commutative-group structure (`*`, `1`, `⁻¹`, `/`) is inherited for free:
example : CommGroup (Dimension B) := inferInstance

/-- Rational powers: scale the exponent vector (the `ℚ`-module action on `B → ℚ`). -/
instance : Pow (Dimension B) ℚ :=
  ⟨fun d q => Multiplicative.ofAdd (q • Multiplicative.toAdd d)⟩

/-- Base dimension `b`: exponent `1` at `b`, `0` elsewhere. -/
def base [DecidableEq B] (b : B) : Dimension B := Multiplicative.ofAdd (Pi.single b 1)

end Dimension

/-- The current five-generator (charge-based) basis — the drop-in default. -/
inductive PhyslibBase | length | time | mass | charge | temperature
  deriving DecidableEq
abbrev PhyslibDimension := Dimension PhyslibBase

/-- A different generating set: Gaussian–CGS has three generators, charge derived. -/
inductive GaussianBase | length | mass | time
  deriving DecidableEq

open GaussianBase in
/-- Gaussian charge `M^(1/2)·L^(3/2)·T^(-1)` — half-integer exponents, fine over `ℚ`. -/
def gaussianCharge : Dimension GaussianBase :=
  Dimension.base mass ^ (1/2 : ℚ) * Dimension.base length ^ (3/2 : ℚ)
    * Dimension.base time ^ (-1 : ℚ)

Multiplicative (B → ℚ) reuses Mathlib's Pi group/module instances, so only the ℚ-power (a one-liner over the module action) and the base-vector constructor need writing; back-compat can then wrap Dimension PhyslibBase in a structure carrying the named projections.

Requirements

A tickbox list of the requirements of the API. This should include things which have already been done as well as things still to be worked on. Details on writing good system requirements can be found here.

Already satisfied by the current Dimension (to be preserved by the generic API):

• Dimension exponents shall be represented over ℚ, so fractional powers are representable (e.g. the Gaussian charge = M^(1/2)·L^(3/2)·T^(-1)). (structure Dimension over ℚ; instance : Pow Dimension ℚ)
• Dimensions shall form a commutative group under multiplication — composition adds exponents, inversion negates them, and 1 is the dimensionless element. (instance : CommGroup Dimension)
• Dimensional equality shall be extensional. (@[ext] lemma Dimension.ext)

Core — parametrize the generating set:

• Dimension shall be parametric in a finite index type B enumerating the base dimensions (the generating set), so that the rank and identity of the basis are inputs, not fixed — e.g. Dimension (B : Type) [Fintype B] [DecidableEq B].
• For every finite B, the commutative-group and ℚ-power structure on Dimension B shall be derived generically (e.g. from Pi/Finsupp), not restated per basis.
• Dimension B shall have decidable equality whenever B has DecidableEq and Fintype.
• For each b : B, the API shall provide the corresponding unit base vector (the generic analog of L𝓭, T𝓭, …): exponent 1 at b, 0 elsewhere.
• The unit side of the bridge shall be parametrized in the same basis B: UnitChoices (currently five named unit fields) shall become a unit choice per b : B, and dimScale : UnitChoices B → UnitChoices B → Dimension B →* ℝ≥0 shall fold over B generically — so HasDim / CarriesDimension / HasDimension carry the basis consistently. (Parametrizing Dimension alone is insufficient; the same five bases are hardwired again in UnitChoices.)

Backward compatibility:

• PhysLib's current basis shall be recoverable as a specific instantiation Dimension PhyslibBase over a concrete enumeration PhyslibBase = {length, time, mass, charge, temperature} (charge-based; a faithful SI/ISQ basis is a separate instance — see Coverage).
• For that SI instantiation, the existing named projections (.length, .time, .mass, .charge, .temperature) and their @[simp] lemmas shall remain available, so current downstream code compiles unchanged (e.g. via a thin structure wrapper or abbreviations over the parametric core).

Coverage — the motivating quantity systems (each a verifiable instantiation):

• The full ISQ seven-base-quantity system shall be expressible — adding amount of substance and luminous intensity, and taking electric current in place of charge, per ISO/IEC 80000-1.
• Gaussian–CGS shall be expressible: three generators L, M, T, with charge a derived ℚ-vector M^(1/2)·L^(3/2)·T^(-1) rather than an independent axis.
• A natural-unit system (c = ħ = 1, reduced generating set) shall be expressible.
• An angle-augmented basis shall be expressible: an added angle generator A, with solid angle the derived square A² (sr = rad²).

Optional / stretch:

• The API should provide a change-of-basis map for an embedding of bases B ↪ B' (e.g. PhyslibBase ↪ an angle-augmented basis), so a dimension in one system can be re-expressed in an extending one. (non-blocking; supports migration and cross-system comparison)
• The design, the SI recovery, and at least one worked non-SI instantiation shall be documented (as an example or test).

References

• P. Quincey, The range of options for handling plane angle and solid angle within a system of units, Metrologia 53 (2016) 840. doi:10.1088/0026-1394/53/2/840
• I. Mills, On the units radian and cycle for the quantity plane angle, Metrologia 53 (2016) 991. doi:10.1088/0026-1394/53/3/991
• P. Quincey, R. J. C. Brown, A clearer approach for defining unit systems, Metrologia 54 (2017) 454. doi:10.1088/1681-7575/aa7160
• P. Quincey, P. J. Mohr, W. D. Phillips, Angles are inherently neither length ratios nor dimensionless, Metrologia 56 (2019) 043001. doi:10.1088/1681-7575/ab27d7
• M. I. Kalinin, On the status of plane and solid angles in the International System of Units (SI), Metrologia 56 (2019) 065009. doi:10.1088/1681-7575/ab3fbf
• B. P. Leonard, Proposal for the dimensionally consistent treatment of angle and solid angle by the International System of Units (SI), Metrologia 58 (2021) 052001. doi:10.1088/1681-7575/abe0fc
• P. J. Mohr, E. L. Shirley, W. D. Phillips, M. Trott, On the dimension of angles and their units, Metrologia 59 (2022) 053001. doi:10.1088/1681-7575/ac7bc2
• ISO/IEC 80000-1 Quantities and units — General
• VIM, 4th ed. 2nd Committee Draft, July 31, 2023. https://www.bipm.org/documents/20126/115700832/VIM4_2CD_clean/c6d0dfb2-ddbf-059e-1f74-9b025c9c59d8

Corresponding file system

The Dimension type is used only within Physlib/Units/ — 11 files (the one match elsewhere is an unrelated doc-heading, "Dimension 7 plane", in Particles/…/DimSevenPlane.lean) — and the HasDim / CarriesDimension carrier layer appears in 10 of them. So the migration surface is a single subsystem, not the whole library.

Core — the type

• Physlib/Units/Dimension.lean — the Dimension record, its CommGroup / Pow ℚ structure, and the SI base vectors L𝓭, T𝓭, M𝓭, C𝓭, Θ𝓭.

Unit/carrier bridge — the same five bases are hardwired again here

• Physlib/Units/Basic.lean — UnitChoices (one unit field per base dimension; five fields), UnitChoices.dimScale : UnitChoices → UnitChoices → Dimension →* ℝ≥0 (folds over the five named fields), and the carrier layer HasDim / dim / CarriesDimension / HasDimension / Dimensionful.

Dimensioned-quantity machinery and worked instances (built on the above)

• Physlib/Units/UnitDependent.lean, Physlib/Units/Integral.lean, Physlib/Units/FDeriv.lean, Physlib/Units/Examples.lean
• Physlib/Units/WithDim/{Basic, Area, Energy, Momentum, Pressure, Speed}.lean — worked dimensioned types.