1. Physlib
  2. Units
  3. LTMCTDimensionBase
Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.Units.Dimension

PhysLib's default dimension basis

LTMCTDimensionBase is PhysLib's default basis of base dimensions β€” length, time, mass, charge and temperature. Dimension LTMCTDimensionBase is the familiar five-exponent dimension, and this module provides the concrete API on top of the generic Dimension B:

    the .length, .time, .mass, .charge, .temperature exponent projections;

    the ofLTMCTDimensionBase constructor from five exponents; and

    the named generators L𝓭, T𝓭, M𝓭, C𝓭, Ξ˜π“­, shown to be the generic single base vectors.

This basis is charge-based with five generators, so it is deliberately not the SI/ISQ base-quantity set (which takes electric current as base and adds amount of substance and luminous intensity); see ISQDimensionBase.

@[expose] public section

PhysLib's default basis of base dimensions β€” length, time, mass, charge, temperature. Note this is charge-based, so it is not the SI/ISQ base-quantity set; see Dimension.

The length base dimension.

The time base dimension.

The mass base dimension.

The charge base dimension.

The temperature base dimension.

inductive LTMCTDimensionBase where | length | time | mass | charge | temperature deriving DecidableEq, Fintype

The LTMCTDimensionBase projections

The five base-dimension exponents of a Dimension LTMCTDimensionBase, provided so that the familiar .length, .time, .mass, .charge, .temperature API is available.

The length exponent of a LTMCTDimensionBase dimension.

def length (d : Dimension LTMCTDimensionBase) : β„š := d.exponent .length

The time exponent of a LTMCTDimensionBase dimension.

def time (d : Dimension LTMCTDimensionBase) : β„š := d.exponent .time

The mass exponent of a LTMCTDimensionBase dimension.

def mass (d : Dimension LTMCTDimensionBase) : β„š := d.exponent .mass

The charge exponent of a LTMCTDimensionBase dimension.

def charge (d : Dimension LTMCTDimensionBase) : β„š := d.exponent .charge

The temperature exponent of a LTMCTDimensionBase dimension.

def temperature (d : Dimension LTMCTDimensionBase) : β„š := d.exponent .temperature

Build a LTMCTDimensionBase dimension from its five exponents, in the order ⟨length, time, mass, charge, temperature⟩.

def ofLTMCTDimensionBase (length time mass charge temperature : β„š) : Dimension LTMCTDimensionBase := ⟨fun | .length => length | .time => time | .mass => mass | .charge => charge | .temperature => temperature⟩
@[simp] lemma ofLTMCTDimensionBase_length (l t m c ΞΈ : β„š) : (ofLTMCTDimensionBase l t m c ΞΈ).length = l := rfl@[simp] lemma ofLTMCTDimensionBase_time (l t m c ΞΈ : β„š) : (ofLTMCTDimensionBase l t m c ΞΈ).time = t := rfl@[simp] lemma ofLTMCTDimensionBase_mass (l t m c ΞΈ : β„š) : (ofLTMCTDimensionBase l t m c ΞΈ).mass = m := rfl@[simp] lemma ofLTMCTDimensionBase_charge (l t m c ΞΈ : β„š) : (ofLTMCTDimensionBase l t m c ΞΈ).charge = c := rfl@[simp] lemma ofLTMCTDimensionBase_temperature (l t m c ΞΈ : β„š) : (ofLTMCTDimensionBase l t m c ΞΈ).temperature = ΞΈ := rfl@[simp] lemma time_mul (d1 d2 : Dimension LTMCTDimensionBase) : (d1 * d2).time = d1.time + d2.time := rfl@[simp] lemma length_mul (d1 d2 : Dimension LTMCTDimensionBase) : (d1 * d2).length = d1.length + d2.length := rfl@[simp] lemma mass_mul (d1 d2 : Dimension LTMCTDimensionBase) : (d1 * d2).mass = d1.mass + d2.mass := rfl@[simp] lemma charge_mul (d1 d2 : Dimension LTMCTDimensionBase) : (d1 * d2).charge = d1.charge + d2.charge := rfl@[simp] lemma temperature_mul (d1 d2 : Dimension LTMCTDimensionBase) : (d1 * d2).temperature = d1.temperature + d2.temperature := rfl@[simp] lemma one_length : (1 : Dimension LTMCTDimensionBase).length = 0 := rfl@[simp] lemma one_time : (1 : Dimension LTMCTDimensionBase).time = 0 := rfl@[simp] lemma one_mass : (1 : Dimension LTMCTDimensionBase).mass = 0 := rfl@[simp] lemma one_charge : (1 : Dimension LTMCTDimensionBase).charge = 0 := rfl@[simp] lemma one_temperature : (1 : Dimension LTMCTDimensionBase).temperature = 0 := rfl@[simp] lemma inv_length (d : Dimension LTMCTDimensionBase) : d⁻¹.length = -d.length := rfl@[simp] lemma inv_time (d : Dimension LTMCTDimensionBase) : d⁻¹.time = -d.time := rfl@[simp] lemma inv_mass (d : Dimension LTMCTDimensionBase) : d⁻¹.mass = -d.mass := rfl@[simp] lemma inv_charge (d : Dimension LTMCTDimensionBase) : d⁻¹.charge = -d.charge := rfl@[simp] lemma inv_temperature (d : Dimension LTMCTDimensionBase) : d⁻¹.temperature = -d.temperature := rfl@[simp] lemma div_length (d1 d2 : Dimension LTMCTDimensionBase) : (d1 / d2).length = d1.length - d2.length := d1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBase⊒ (d1 / d2).length = d1.length - d2.length All goals completed! πŸ™@[simp] lemma div_time (d1 d2 : Dimension LTMCTDimensionBase) : (d1 / d2).time = d1.time - d2.time := d1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBase⊒ (d1 / d2).time = d1.time - d2.time All goals completed! πŸ™@[simp] lemma div_mass (d1 d2 : Dimension LTMCTDimensionBase) : (d1 / d2).mass = d1.mass - d2.mass := d1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBase⊒ (d1 / d2).mass = d1.mass - d2.mass All goals completed! πŸ™@[simp] lemma div_charge (d1 d2 : Dimension LTMCTDimensionBase) : (d1 / d2).charge = d1.charge - d2.charge := d1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBase⊒ (d1 / d2).charge = d1.charge - d2.charge All goals completed! πŸ™@[simp] lemma div_temperature (d1 d2 : Dimension LTMCTDimensionBase) : (d1 / d2).temperature = d1.temperature - d2.temperature := d1:Dimension LTMCTDimensionBased2:Dimension LTMCTDimensionBase⊒ (d1 / d2).temperature = d1.temperature - d2.temperature All goals completed! πŸ™@[simp] lemma npow_length (d : Dimension LTMCTDimensionBase) (n : β„•) : (d ^ n).length = n β€’ d.length := d:Dimension LTMCTDimensionBasen:β„•βŠ’ (d ^ n).length = n β€’ d.length All goals completed! πŸ™@[simp] lemma npow_time (d : Dimension LTMCTDimensionBase) (n : β„•) : (d ^ n).time = n β€’ d.time := d:Dimension LTMCTDimensionBasen:β„•βŠ’ (d ^ n).time = n β€’ d.time All goals completed! πŸ™@[simp] lemma npow_mass (d : Dimension LTMCTDimensionBase) (n : β„•) : (d ^ n).mass = n β€’ d.mass := d:Dimension LTMCTDimensionBasen:β„•βŠ’ (d ^ n).mass = n β€’ d.mass All goals completed! πŸ™@[simp] lemma npow_charge (d : Dimension LTMCTDimensionBase) (n : β„•) : (d ^ n).charge = n β€’ d.charge := d:Dimension LTMCTDimensionBasen:β„•βŠ’ (d ^ n).charge = n β€’ d.charge All goals completed! πŸ™@[simp] lemma npow_temperature (d : Dimension LTMCTDimensionBase) (n : β„•) : (d ^ n).temperature = n β€’ d.temperature := d:Dimension LTMCTDimensionBasen:β„•βŠ’ (d ^ n).temperature = n β€’ d.temperature All goals completed! πŸ™

The dimension corresponding to length.

def L𝓭 : Dimension LTMCTDimensionBase := ofLTMCTDimensionBase 1 0 0 0 0
@[simp] lemma L𝓭_length : L𝓭.length = 1 := ⊒ L𝓭.length = 1 All goals completed! πŸ™@[simp] lemma L𝓭_time : L𝓭.time = 0 := ⊒ L𝓭.time = 0 All goals completed! πŸ™@[simp] lemma L𝓭_mass : L𝓭.mass = 0 := ⊒ L𝓭.mass = 0 All goals completed! πŸ™@[simp] lemma L𝓭_charge : L𝓭.charge = 0 := ⊒ L𝓭.charge = 0 All goals completed! πŸ™@[simp] lemma L𝓭_temperature : L𝓭.temperature = 0 := ⊒ L𝓭.temperature = 0 All goals completed! πŸ™

The dimension corresponding to time.

def T𝓭 : Dimension LTMCTDimensionBase := ofLTMCTDimensionBase 0 1 0 0 0
@[simp] lemma T𝓭_length : T𝓭.length = 0 := ⊒ T𝓭.length = 0 All goals completed! πŸ™@[simp] lemma T𝓭_time : T𝓭.time = 1 := ⊒ T𝓭.time = 1 All goals completed! πŸ™@[simp] lemma T𝓭_mass : T𝓭.mass = 0 := ⊒ T𝓭.mass = 0 All goals completed! πŸ™@[simp] lemma T𝓭_charge : T𝓭.charge = 0 := ⊒ T𝓭.charge = 0 All goals completed! πŸ™@[simp] lemma T𝓭_temperature : T𝓭.temperature = 0 := ⊒ T𝓭.temperature = 0 All goals completed! πŸ™

The dimension corresponding to mass.

def M𝓭 : Dimension LTMCTDimensionBase := ofLTMCTDimensionBase 0 0 1 0 0

The dimension corresponding to charge.

def C𝓭 : Dimension LTMCTDimensionBase := ofLTMCTDimensionBase 0 0 0 1 0

The dimension corresponding to temperature.

def Ξ˜π“­ : Dimension LTMCTDimensionBase := ofLTMCTDimensionBase 0 0 0 0 1

The named generators are the base vectors

Each named generator L𝓭, T𝓭, … is the generic single base vector at the corresponding base dimension, exhibiting them as instances of the basis-generic API.

lemma L𝓭_eq_single : L𝓭 = single .length := ⊒ L𝓭 = single LTMCTDimensionBase.length b:LTMCTDimensionBase⊒ L𝓭.exponent b = (single LTMCTDimensionBase.length).exponent b; ⊒ L𝓭.exponent LTMCTDimensionBase.length = (single LTMCTDimensionBase.length).exponent LTMCTDimensionBase.length⊒ L𝓭.exponent LTMCTDimensionBase.time = (single LTMCTDimensionBase.length).exponent LTMCTDimensionBase.time⊒ L𝓭.exponent LTMCTDimensionBase.mass = (single LTMCTDimensionBase.length).exponent LTMCTDimensionBase.mass⊒ L𝓭.exponent LTMCTDimensionBase.charge = (single LTMCTDimensionBase.length).exponent LTMCTDimensionBase.charge⊒ L𝓭.exponent LTMCTDimensionBase.temperature = (single LTMCTDimensionBase.length).exponent LTMCTDimensionBase.temperature ⊒ L𝓭.exponent LTMCTDimensionBase.length = (single LTMCTDimensionBase.length).exponent LTMCTDimensionBase.length⊒ L𝓭.exponent LTMCTDimensionBase.time = (single LTMCTDimensionBase.length).exponent LTMCTDimensionBase.time⊒ L𝓭.exponent LTMCTDimensionBase.mass = (single LTMCTDimensionBase.length).exponent LTMCTDimensionBase.mass⊒ L𝓭.exponent LTMCTDimensionBase.charge = (single LTMCTDimensionBase.length).exponent LTMCTDimensionBase.charge⊒ L𝓭.exponent LTMCTDimensionBase.temperature = (single LTMCTDimensionBase.length).exponent LTMCTDimensionBase.temperature All goals completed! πŸ™lemma T𝓭_eq_single : T𝓭 = single .time := ⊒ T𝓭 = single LTMCTDimensionBase.time b:LTMCTDimensionBase⊒ T𝓭.exponent b = (single LTMCTDimensionBase.time).exponent b; ⊒ T𝓭.exponent LTMCTDimensionBase.length = (single LTMCTDimensionBase.time).exponent LTMCTDimensionBase.length⊒ T𝓭.exponent LTMCTDimensionBase.time = (single LTMCTDimensionBase.time).exponent LTMCTDimensionBase.time⊒ T𝓭.exponent LTMCTDimensionBase.mass = (single LTMCTDimensionBase.time).exponent LTMCTDimensionBase.mass⊒ T𝓭.exponent LTMCTDimensionBase.charge = (single LTMCTDimensionBase.time).exponent LTMCTDimensionBase.charge⊒ T𝓭.exponent LTMCTDimensionBase.temperature = (single LTMCTDimensionBase.time).exponent LTMCTDimensionBase.temperature ⊒ T𝓭.exponent LTMCTDimensionBase.length = (single LTMCTDimensionBase.time).exponent LTMCTDimensionBase.length⊒ T𝓭.exponent LTMCTDimensionBase.time = (single LTMCTDimensionBase.time).exponent LTMCTDimensionBase.time⊒ T𝓭.exponent LTMCTDimensionBase.mass = (single LTMCTDimensionBase.time).exponent LTMCTDimensionBase.mass⊒ T𝓭.exponent LTMCTDimensionBase.charge = (single LTMCTDimensionBase.time).exponent LTMCTDimensionBase.charge⊒ T𝓭.exponent LTMCTDimensionBase.temperature = (single LTMCTDimensionBase.time).exponent LTMCTDimensionBase.temperature All goals completed! πŸ™lemma M𝓭_eq_single : M𝓭 = single .mass := ⊒ M𝓭 = single LTMCTDimensionBase.mass b:LTMCTDimensionBase⊒ M𝓭.exponent b = (single LTMCTDimensionBase.mass).exponent b; ⊒ M𝓭.exponent LTMCTDimensionBase.length = (single LTMCTDimensionBase.mass).exponent LTMCTDimensionBase.length⊒ M𝓭.exponent LTMCTDimensionBase.time = (single LTMCTDimensionBase.mass).exponent LTMCTDimensionBase.time⊒ M𝓭.exponent LTMCTDimensionBase.mass = (single LTMCTDimensionBase.mass).exponent LTMCTDimensionBase.mass⊒ M𝓭.exponent LTMCTDimensionBase.charge = (single LTMCTDimensionBase.mass).exponent LTMCTDimensionBase.charge⊒ M𝓭.exponent LTMCTDimensionBase.temperature = (single LTMCTDimensionBase.mass).exponent LTMCTDimensionBase.temperature ⊒ M𝓭.exponent LTMCTDimensionBase.length = (single LTMCTDimensionBase.mass).exponent LTMCTDimensionBase.length⊒ M𝓭.exponent LTMCTDimensionBase.time = (single LTMCTDimensionBase.mass).exponent LTMCTDimensionBase.time⊒ M𝓭.exponent LTMCTDimensionBase.mass = (single LTMCTDimensionBase.mass).exponent LTMCTDimensionBase.mass⊒ M𝓭.exponent LTMCTDimensionBase.charge = (single LTMCTDimensionBase.mass).exponent LTMCTDimensionBase.charge⊒ M𝓭.exponent LTMCTDimensionBase.temperature = (single LTMCTDimensionBase.mass).exponent LTMCTDimensionBase.temperature All goals completed! πŸ™lemma C𝓭_eq_single : C𝓭 = single .charge := ⊒ C𝓭 = single LTMCTDimensionBase.charge b:LTMCTDimensionBase⊒ C𝓭.exponent b = (single LTMCTDimensionBase.charge).exponent b; ⊒ C𝓭.exponent LTMCTDimensionBase.length = (single LTMCTDimensionBase.charge).exponent LTMCTDimensionBase.length⊒ C𝓭.exponent LTMCTDimensionBase.time = (single LTMCTDimensionBase.charge).exponent LTMCTDimensionBase.time⊒ C𝓭.exponent LTMCTDimensionBase.mass = (single LTMCTDimensionBase.charge).exponent LTMCTDimensionBase.mass⊒ C𝓭.exponent LTMCTDimensionBase.charge = (single LTMCTDimensionBase.charge).exponent LTMCTDimensionBase.charge⊒ C𝓭.exponent LTMCTDimensionBase.temperature = (single LTMCTDimensionBase.charge).exponent LTMCTDimensionBase.temperature ⊒ C𝓭.exponent LTMCTDimensionBase.length = (single LTMCTDimensionBase.charge).exponent LTMCTDimensionBase.length⊒ C𝓭.exponent LTMCTDimensionBase.time = (single LTMCTDimensionBase.charge).exponent LTMCTDimensionBase.time⊒ C𝓭.exponent LTMCTDimensionBase.mass = (single LTMCTDimensionBase.charge).exponent LTMCTDimensionBase.mass⊒ C𝓭.exponent LTMCTDimensionBase.charge = (single LTMCTDimensionBase.charge).exponent LTMCTDimensionBase.charge⊒ C𝓭.exponent LTMCTDimensionBase.temperature = (single LTMCTDimensionBase.charge).exponent LTMCTDimensionBase.temperature All goals completed! πŸ™lemma Ξ˜π“­_eq_single : Ξ˜π“­ = single .temperature := ⊒ Ξ˜π“­ = single LTMCTDimensionBase.temperature b:LTMCTDimensionBase⊒ Ξ˜π“­.exponent b = (single LTMCTDimensionBase.temperature).exponent b; ⊒ Ξ˜π“­.exponent LTMCTDimensionBase.length = (single LTMCTDimensionBase.temperature).exponent LTMCTDimensionBase.length⊒ Ξ˜π“­.exponent LTMCTDimensionBase.time = (single LTMCTDimensionBase.temperature).exponent LTMCTDimensionBase.time⊒ Ξ˜π“­.exponent LTMCTDimensionBase.mass = (single LTMCTDimensionBase.temperature).exponent LTMCTDimensionBase.mass⊒ Ξ˜π“­.exponent LTMCTDimensionBase.charge = (single LTMCTDimensionBase.temperature).exponent LTMCTDimensionBase.charge⊒ Ξ˜π“­.exponent LTMCTDimensionBase.temperature = (single LTMCTDimensionBase.temperature).exponent LTMCTDimensionBase.temperature ⊒ Ξ˜π“­.exponent LTMCTDimensionBase.length = (single LTMCTDimensionBase.temperature).exponent LTMCTDimensionBase.length⊒ Ξ˜π“­.exponent LTMCTDimensionBase.time = (single LTMCTDimensionBase.temperature).exponent LTMCTDimensionBase.time⊒ Ξ˜π“­.exponent LTMCTDimensionBase.mass = (single LTMCTDimensionBase.temperature).exponent LTMCTDimensionBase.mass⊒ Ξ˜π“­.exponent LTMCTDimensionBase.charge = (single LTMCTDimensionBase.temperature).exponent LTMCTDimensionBase.charge⊒ Ξ˜π“­.exponent LTMCTDimensionBase.temperature = (single LTMCTDimensionBase.temperature).exponent LTMCTDimensionBase.temperature All goals completed! πŸ™