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.UnitSystem
public import Physlib.Units.ISQDimensionBaseA typed unit choice over the ISQ base quantities (the SI units)
LTMCTUnitChoices is the typed unit choice over PhysLib's default dimension basis
LTMCTDimensionBase. This module gives the second typed unit choice — over the
seven ISQ base quantities ISQDimensionBase — realised through the basis-generic
UnitMagnitudeCatalog / UnitSystem machinery of Physlib.Units.UnitSystem. It is the concrete
payoff of parametrising the unit side: the same generic layer produces a fully typed
unit choice over a different basis, and the scaling homomorphism comes for free from
UnitScale.dimScale — nothing is re-proved by hand.
The ISQ base quantities are length, mass, time, electric current, thermodynamic
temperature, amount of substance and luminous intensity. Four of the corresponding typed
unit types already exist (LengthUnit, MassUnit, TimeUnit, TemperatureUnit); the
remaining three — CurrentUnit, AmountUnit, LuminousIntensityUnit — are introduced
here. (They follow the LengthUnit convention of a positive-real magnitude; the full
division/scaling API can be filled in later and, following PhysLib's layout, they would
ultimately live under the relevant physics directories.)
SIUnitChoices := UnitSystem ISQDimensionBase is then the typed SI unit choice, and
SIUnitChoices.SI is the coherent SI choice (metre, kilogram, second, ampere, kelvin,
mole, candela). Contrast SIUnitChoices (current-based, seven typed slots) with
LTMCTUnitChoices (charge-based, five typed slots): the machinery supports both, and the
Dimension.ltmctToISQ / Dimension.isqToLTMCT bridge relates their bases.
@[expose] public sectionTyped unit types for the ISQ base quantities not already present
A unit of electric current — a choice of positive-real magnitude. The SI coherent choice is the ampere.
The underlying scale of the unit.
structure CurrentUnit where val : ℝ
property : 0 < val@[simp]
lemma val_ne_zero (x : CurrentUnit) : x.val ≠ 0 := Ne.symm (ne_of_lt x.property)lemma val_pos (x : CurrentUnit) : 0 < x.val := x.propertyinstance : Inhabited CurrentUnit where
default := ⟨1, ⊢ 0 < 1 All goals completed! 🐙⟩lemma div_eq_val (x y : CurrentUnit) :
x / y = (⟨x.val / y.val, div_nonneg x.val_pos.le y.val_pos.le⟩ : ℝ≥0) := rflThe SI coherent unit of electric current, the ampere.
def amperes : CurrentUnit := ⟨1, ⊢ 0 < 1 All goals completed! 🐙⟩A unit of amount of substance — a choice of positive-real magnitude. The SI coherent choice is the mole.
The underlying scale of the unit.
structure AmountUnit where val : ℝ
property : 0 < val@[simp]
lemma val_ne_zero (x : AmountUnit) : x.val ≠ 0 := Ne.symm (ne_of_lt x.property)lemma val_pos (x : AmountUnit) : 0 < x.val := x.propertyinstance : Inhabited AmountUnit where
default := ⟨1, ⊢ 0 < 1 All goals completed! 🐙⟩lemma div_eq_val (x y : AmountUnit) :
x / y = (⟨x.val / y.val, div_nonneg x.val_pos.le y.val_pos.le⟩ : ℝ≥0) := rflThe SI coherent unit of amount of substance, the mole.
def moles : AmountUnit := ⟨1, ⊢ 0 < 1 All goals completed! 🐙⟩A unit of luminous intensity — a choice of positive-real magnitude. The SI coherent choice is the candela.
The underlying scale of the unit.
structure LuminousIntensityUnit where val : ℝ
property : 0 < val@[simp]
lemma val_ne_zero (x : LuminousIntensityUnit) : x.val ≠ 0 := Ne.symm (ne_of_lt x.property)lemma val_pos (x : LuminousIntensityUnit) : 0 < x.val := x.propertyinstance : Inhabited LuminousIntensityUnit where
default := ⟨1, ⊢ 0 < 1 All goals completed! 🐙⟩lemma div_eq_val (x y : LuminousIntensityUnit) :
x / y = (⟨x.val / y.val, div_nonneg x.val_pos.le y.val_pos.le⟩ : ℝ≥0) := rflThe SI coherent unit of luminous intensity, the candela.
def candelas : LuminousIntensityUnit := ⟨1, ⊢ 0 < 1 All goals completed! 🐙⟩
The ISQ UnitMagnitudeCatalog instance
Each ISQ base quantity is assigned its typed unit type; the magnitude layer is the
positive-real val, exactly as for the LTMCTDimensionBase instance.
Folding over the ISQ base quantities
SIUnitChoices
A typed SI unit choice: a typed unit at every ISQ base quantity. This is the
seven-slot, current-based sibling of the five-slot, charge-based LTMCTUnitChoices,
produced by the same basis-generic UnitSystem / UnitMagnitudeCatalog machinery.
abbrev SIUnitChoices := UnitSystem ISQDimensionBase
Type-safety check: the current slot of a typed SI unit choice is a CurrentUnit —
a MassUnit cannot be placed there.
example (u : SIUnitChoices) : CurrentUnit := u .currentA quantity of ISQ dimension does not rescale between a unit choice and itself.
lemma dimScale_self (u : SIUnitChoices) (d : Dimension ISQDimensionBase) :
dimScale u u d = 1 := UnitScale.dimScale_self _ d