1. Physlib
  2. Units
  3. ISQDimensionBase
Imports
/- Copyright (c) 2026 Nicolas Rouquette. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Nicolas Rouquette -/ module public import Physlib.Units.Dimension

The ISQ base quantities

The International System of Quantities (ISQ), specified in ISO/IEC 80000-1 and described in the International Vocabulary of Metrology (VIM, 3rd edition, JCGM 200:2012), fixes seven mutually independent base quantities: length, mass, time, electric current, thermodynamic temperature, amount of substance, and luminous intensity.

ISQDimensionBase is that seven-element basis, realised as an instantiation Dimension ISQDimensionBase of the parametric dimensional algebra. It differs from PhysLib's default LTMCTDimensionBase in two ways:

    the electromagnetic base quantity is electric current, so electric charge is a derived dimension (Q = I · T, ISQDimensionBase.charge); and

    amount of substance and luminous intensity are additional independent base quantities.

References

    ISO/IEC 80000-1:2009, Quantities and units — Part 1: General.

    JCGM 200:2012, International vocabulary of metrology — Basic and general concepts and associated terms (VIM, 3rd edition).

@[expose] public section

The seven ISQ base quantities (ISO/IEC 80000-1; VIM 3rd edition). Unlike LTMCTDimensionBase, electric current is the electromagnetic base quantity (so charge is derived), and amount of substance and luminous intensity are further base quantities.

The length base quantity.

The mass base quantity.

The time base quantity.

The electric-current base quantity.

The thermodynamic-temperature base quantity.

The amount-of-substance base quantity.

The luminous-intensity base quantity.

inductive ISQDimensionBase where | length | mass | time | current | temperature | amount | luminousIntensity deriving DecidableEq, Fintype

The ISQ has seven base quantities.

lemma card_eq_seven : Fintype.card ISQDimensionBase = 7 := ⊢ Fintype.card ISQDimensionBase = 7 All goals completed! 🐙

Electric charge is a derived dimension in the ISQ: Q = I · T.

def charge : Dimension ISQDimensionBase := single .current * single .time

The derived charge dimension has electric-current exponent 1.

lemma charge_exponent_current : charge.exponent .current = 1 := ⊢ charge.exponent current = 1 All goals completed! 🐙

The derived charge dimension has time exponent 1.

lemma charge_exponent_time : charge.exponent .time = 1 := ⊢ charge.exponent time = 1 All goals completed! 🐙

The derived charge dimension has mass exponent 0.

lemma charge_exponent_mass : charge.exponent .mass = 0 := ⊢ charge.exponent mass = 0 All goals completed! 🐙

Amount of substance is an independent base dimension (absent from LTMCTDimensionBase).

lemma single_amount_ne_one : single (.amount : ISQDimensionBase) ≠ 1 := ⊢ single amount ≠ 1 h:single amount = 1⊢ False h:single amount = 1this:(single amount).exponent amount = exponent 1 amount⊢ False All goals completed! 🐙

Luminous intensity is an independent base dimension (absent from LTMCTDimensionBase).

lemma single_luminousIntensity_ne_one : single (.luminousIntensity : ISQDimensionBase) ≠ 1 := ⊢ single luminousIntensity ≠ 1 h:single luminousIntensity = 1⊢ False h:single luminousIntensity = 1this:(single luminousIntensity).exponent luminousIntensity = exponent 1 luminousIntensity⊢ False All goals completed! 🐙