Physlib.Units.UnitSystem

Physlib
Units
UnitSystem

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.ParametricUnits

Unit systems, parametrised in a dimension basis

A unit system is the everyday physics object: a rule fixing one concrete unit for each base quantity. SI fixes the metre for length, the second for time, the kilogram for mass, …; CGS fixes the centimetre, second and gram. Choosing a system gives every quantity a numerical value; changing systems rescales those values.

This module makes that notion work for any dimension basis B (matching the basis-generic Dimension B), while keeping units typed: the unit in the length slot has type LengthUnit, the one in the time slot TimeUnit, so the checker rejects a mass unit in a length slot.

UnitMagnitudeCatalog B — the menu for basis B. For each base dimension b : B it gives a type Unit b of admissible units — so a dimension may offer many (length: metre, kilometre, micrometre, …) — and a function mag assigning each unit its one positive-real magnitude. The menu lists the options and picks none; many unit systems share one catalog.

UnitSystem B — the pick: a function choosing exactly one unit per base dimension. A single unit system therefore fixes one length unit — metre or kilometre, never both — so metre and kilometre are two menu entries selected by two different UnitSystems over the same catalog. SI and CGS are two such picks.

UnitSystem.toScale : UnitSystem B → UnitScale B — forget the unit types, keep only the magnitudes, landing in the bare magnitude layer UnitScale B where the scaling homomorphism UnitScale.dimScale is proved once.

Menu vs. pick. The catalog is a menu, not a choice: it says which units exist and what each weighs, but selects none — a UnitSystem makes the selection. And in PhysLib a base unit is a positive real ({ val : ℝ // 0 < val }), i.e. its own magnitude, so the magnitude comes fixed with the unit; there is no separate "assign a magnitude" step. Hence metre, micrometre and kilometre are three different units on the one length menu, and "SI in metres" versus "the same in micrometres" are two different UnitSystems over the same catalog — related by UnitScale.dimScale, which computes the 10⁶ factor between them. (The multiplicity one might expect from "many magnitudes" lives here, among the unit systems, not in many catalogs.)

The LTMCTDimensionBase catalog recovers PhysLib's five named unit types, and LTMCTUnitChoices ≃ UnitSystem LTMCTDimensionBase exhibits the bespoke five-field record as that instance. Scaling laws are not re-proved here — they live once on UnitScale B, and the typed layer is a thin faithful wrapper projecting onto it via toScale.

This is the typed, basis-generic layer discussed as "Option D" in the review of the dimension-parametrisation PR; it is the only design that keeps both basis-genericity and typed-unit safety.

@[expose] public section

A menu of typed units for a basis B: for each base dimension b : B, a type Unit b of admissible units (a dimension may offer several — metre, kilometre, …) and a function mag giving each its single positive-real magnitude. It lists the options and picks none — a UnitSystem makes the pick. One catalog underlies many unit systems (SI, CGS, …); the magnitude is the data toScale reads to drive rescaling.

The typed unit type at each base dimension.

The positive-real magnitude of a typed unit.

Every typed unit has a positive magnitude.

              class UnitMagnitudeCatalog (B : Type) where  Unit : B → Type  mag : {b : B} → Unit b → ℝ≥0  mag_pos : ∀ {b : B} (u : Unit b), 0 < mag u

A unit system over a basis B with a UnitMagnitudeCatalog: one typed unit chosen per base dimension — the pick off the catalog's menu, and the formal counterpart of SI, CGS, …. Over the default basis, u .length : LengthUnit, and a MassUnit cannot be placed in the length slot.

def UnitSystem (B : Type) [UnitMagnitudeCatalog B] := (b : B) → UnitMagnitudeCatalog.Unit b

Two unit systems agree once they pick the same unit at every base dimension: UnitSystem is extensional, as befits a choice-per-dimension.

@[ext]
theorem ext {u v : UnitSystem B} (h : ∀ b, u b = v b) : u = v := funext h

@[simp]
lemma toScale_scale (u : UnitSystem B) (b : B) :
    (toScale u).scale b = UnitMagnitudeCatalog.mag (u b) := rfl

The `LTMCTDimensionBase` catalog

The default basis's UnitMagnitudeCatalog recovers exactly PhysLib's five named typed unit types, so UnitSystem LTMCTDimensionBase is the typed five-slot unit system and u .length : LengthUnit, LengthUnit.meters, … all still work — and a MassUnit cannot be placed in the length slot.

Type-safety check: a unit system over LTMCTDimensionBase projects onto the named typed unit types, so the length slot is a LengthUnit (and cannot hold a MassUnit).

example (u : UnitSystem LTMCTDimensionBase) : LengthUnit := u .length

example : UnitSystem LTMCTDimensionBase := fun
  | .length => LengthUnit.meters
  | .time => TimeUnit.seconds
  | .mass => MassUnit.kilograms
  | .charge => ChargeUnit.coulombs
  | .temperature => TemperatureUnit.kelvin

`LTMCTUnitChoices` is `UnitSystem LTMCTDimensionBase`

The bespoke five-field record and the generic unit system over the default basis carry the same data.

The bespoke five-field LTMCTUnitChoices and the generic UnitSystem LTMCTDimensionBase are the same data.

def equivUnitSystem : LTMCTUnitChoices ≃ UnitSystem LTMCTDimensionBase where
  toFun u := fun
    | .length => u.length
    | .time => u.time
    | .mass => u.mass
    | .charge => u.charge
    | .temperature => u.temperature
  invFun f :=
    { length := f .length
      time := f .time
      mass := f .mass
      charge := f .charge
      temperature := f .temperature }
  left_inv u := byu:LTMCTUnitChoices⊢ (fun f =>
      { length := f LTMCTDimensionBase.length, time := f LTMCTDimensionBase.time, mass := f LTMCTDimensionBase.mass,
        charge := f LTMCTDimensionBase.charge, temperature := f LTMCTDimensionBase.temperature })
    ((fun u x =>
        match x with
        | LTMCTDimensionBase.length => u.length
        | LTMCTDimensionBase.time => u.time
        | LTMCTDimensionBase.mass => u.mass
        | LTMCTDimensionBase.charge => u.charge
        | LTMCTDimensionBase.temperature => u.temperature)
      u) =
  u cases umklength✝:LengthUnittime✝:TimeUnitmass✝:MassUnitcharge✝:ChargeUnittemperature✝:TemperatureUnit⊢ (fun f =>
      { length := f LTMCTDimensionBase.length, time := f LTMCTDimensionBase.time, mass := f LTMCTDimensionBase.mass,
        charge := f LTMCTDimensionBase.charge, temperature := f LTMCTDimensionBase.temperature })
    ((fun u x =>
        match x with
        | LTMCTDimensionBase.length => u.length
        | LTMCTDimensionBase.time => u.time
        | LTMCTDimensionBase.mass => u.mass
        | LTMCTDimensionBase.charge => u.charge
        | LTMCTDimensionBase.temperature => u.temperature)
      { length := length✝, time := time✝, mass := mass✝, charge := charge✝, temperature := temperature✝ }) =
  { length := length✝, time := time✝, mass := mass✝, charge := charge✝, temperature := temperature✝ }; rflAll goals completed! 🐙
  right_inv f := byf:UnitSystem LTMCTDimensionBase⊢ (fun u x =>
      match x with
      | LTMCTDimensionBase.length => u.length
      | LTMCTDimensionBase.time => u.time
      | LTMCTDimensionBase.mass => u.mass
      | LTMCTDimensionBase.charge => u.charge
      | LTMCTDimensionBase.temperature => u.temperature)
    ((fun f =>
        { length := f LTMCTDimensionBase.length, time := f LTMCTDimensionBase.time, mass := f LTMCTDimensionBase.mass,
          charge := f LTMCTDimensionBase.charge, temperature := f LTMCTDimensionBase.temperature })
      f) =
  f funext bf:UnitSystem LTMCTDimensionBaseb:LTMCTDimensionBase⊢ (fun u x =>
      match x with
      | LTMCTDimensionBase.length => u.length
      | LTMCTDimensionBase.time => u.time
      | LTMCTDimensionBase.mass => u.mass
      | LTMCTDimensionBase.charge => u.charge
      | LTMCTDimensionBase.temperature => u.temperature)
    ((fun f =>
        { length := f LTMCTDimensionBase.length, time := f LTMCTDimensionBase.time, mass := f LTMCTDimensionBase.mass,
          charge := f LTMCTDimensionBase.charge, temperature := f LTMCTDimensionBase.temperature })
      f)
    b =
  f b; cases blengthf:UnitSystem LTMCTDimensionBase⊢ (fun u x =>
      match x with
      | LTMCTDimensionBase.length => u.length
      | LTMCTDimensionBase.time => u.time
      | LTMCTDimensionBase.mass => u.mass
      | LTMCTDimensionBase.charge => u.charge
      | LTMCTDimensionBase.temperature => u.temperature)
    ((fun f =>
        { length := f LTMCTDimensionBase.length, time := f LTMCTDimensionBase.time, mass := f LTMCTDimensionBase.mass,
          charge := f LTMCTDimensionBase.charge, temperature := f LTMCTDimensionBase.temperature })
      f)
    LTMCTDimensionBase.length =
  f LTMCTDimensionBase.lengthtimef:UnitSystem LTMCTDimensionBase⊢ (fun u x =>
      match x with
      | LTMCTDimensionBase.length => u.length
      | LTMCTDimensionBase.time => u.time
      | LTMCTDimensionBase.mass => u.mass
      | LTMCTDimensionBase.charge => u.charge
      | LTMCTDimensionBase.temperature => u.temperature)
    ((fun f =>
        { length := f LTMCTDimensionBase.length, time := f LTMCTDimensionBase.time, mass := f LTMCTDimensionBase.mass,
          charge := f LTMCTDimensionBase.charge, temperature := f LTMCTDimensionBase.temperature })
      f)
    LTMCTDimensionBase.time =
  f LTMCTDimensionBase.timemassf:UnitSystem LTMCTDimensionBase⊢ (fun u x =>
      match x with
      | LTMCTDimensionBase.length => u.length
      | LTMCTDimensionBase.time => u.time
      | LTMCTDimensionBase.mass => u.mass
      | LTMCTDimensionBase.charge => u.charge
      | LTMCTDimensionBase.temperature => u.temperature)
    ((fun f =>
        { length := f LTMCTDimensionBase.length, time := f LTMCTDimensionBase.time, mass := f LTMCTDimensionBase.mass,
          charge := f LTMCTDimensionBase.charge, temperature := f LTMCTDimensionBase.temperature })
      f)
    LTMCTDimensionBase.mass =
  f LTMCTDimensionBase.masschargef:UnitSystem LTMCTDimensionBase⊢ (fun u x =>
      match x with
      | LTMCTDimensionBase.length => u.length
      | LTMCTDimensionBase.time => u.time
      | LTMCTDimensionBase.mass => u.mass
      | LTMCTDimensionBase.charge => u.charge
      | LTMCTDimensionBase.temperature => u.temperature)
    ((fun f =>
        { length := f LTMCTDimensionBase.length, time := f LTMCTDimensionBase.time, mass := f LTMCTDimensionBase.mass,
          charge := f LTMCTDimensionBase.charge, temperature := f LTMCTDimensionBase.temperature })
      f)
    LTMCTDimensionBase.charge =
  f LTMCTDimensionBase.chargetemperaturef:UnitSystem LTMCTDimensionBase⊢ (fun u x =>
      match x with
      | LTMCTDimensionBase.length => u.length
      | LTMCTDimensionBase.time => u.time
      | LTMCTDimensionBase.mass => u.mass
      | LTMCTDimensionBase.charge => u.charge
      | LTMCTDimensionBase.temperature => u.temperature)
    ((fun f =>
        { length := f LTMCTDimensionBase.length, time := f LTMCTDimensionBase.time, mass := f LTMCTDimensionBase.mass,
          charge := f LTMCTDimensionBase.charge, temperature := f LTMCTDimensionBase.temperature })
      f)
    LTMCTDimensionBase.temperature =
  f LTMCTDimensionBase.temperature <;>lengthf:UnitSystem LTMCTDimensionBase⊢ (fun u x =>
      match x with
      | LTMCTDimensionBase.length => u.length
      | LTMCTDimensionBase.time => u.time
      | LTMCTDimensionBase.mass => u.mass
      | LTMCTDimensionBase.charge => u.charge
      | LTMCTDimensionBase.temperature => u.temperature)
    ((fun f =>
        { length := f LTMCTDimensionBase.length, time := f LTMCTDimensionBase.time, mass := f LTMCTDimensionBase.mass,
          charge := f LTMCTDimensionBase.charge, temperature := f LTMCTDimensionBase.temperature })
      f)
    LTMCTDimensionBase.length =
  f LTMCTDimensionBase.lengthtimef:UnitSystem LTMCTDimensionBase⊢ (fun u x =>
      match x with
      | LTMCTDimensionBase.length => u.length
      | LTMCTDimensionBase.time => u.time
      | LTMCTDimensionBase.mass => u.mass
      | LTMCTDimensionBase.charge => u.charge
      | LTMCTDimensionBase.temperature => u.temperature)
    ((fun f =>
        { length := f LTMCTDimensionBase.length, time := f LTMCTDimensionBase.time, mass := f LTMCTDimensionBase.mass,
          charge := f LTMCTDimensionBase.charge, temperature := f LTMCTDimensionBase.temperature })
      f)
    LTMCTDimensionBase.time =
  f LTMCTDimensionBase.timemassf:UnitSystem LTMCTDimensionBase⊢ (fun u x =>
      match x with
      | LTMCTDimensionBase.length => u.length
      | LTMCTDimensionBase.time => u.time
      | LTMCTDimensionBase.mass => u.mass
      | LTMCTDimensionBase.charge => u.charge
      | LTMCTDimensionBase.temperature => u.temperature)
    ((fun f =>
        { length := f LTMCTDimensionBase.length, time := f LTMCTDimensionBase.time, mass := f LTMCTDimensionBase.mass,
          charge := f LTMCTDimensionBase.charge, temperature := f LTMCTDimensionBase.temperature })
      f)
    LTMCTDimensionBase.mass =
  f LTMCTDimensionBase.masschargef:UnitSystem LTMCTDimensionBase⊢ (fun u x =>
      match x with
      | LTMCTDimensionBase.length => u.length
      | LTMCTDimensionBase.time => u.time
      | LTMCTDimensionBase.mass => u.mass
      | LTMCTDimensionBase.charge => u.charge
      | LTMCTDimensionBase.temperature => u.temperature)
    ((fun f =>
        { length := f LTMCTDimensionBase.length, time := f LTMCTDimensionBase.time, mass := f LTMCTDimensionBase.mass,
          charge := f LTMCTDimensionBase.charge, temperature := f LTMCTDimensionBase.temperature })
      f)
    LTMCTDimensionBase.charge =
  f LTMCTDimensionBase.chargetemperaturef:UnitSystem LTMCTDimensionBase⊢ (fun u x =>
      match x with
      | LTMCTDimensionBase.length => u.length
      | LTMCTDimensionBase.time => u.time
      | LTMCTDimensionBase.mass => u.mass
      | LTMCTDimensionBase.charge => u.charge
      | LTMCTDimensionBase.temperature => u.temperature)
    ((fun f =>
        { length := f LTMCTDimensionBase.length, time := f LTMCTDimensionBase.time, mass := f LTMCTDimensionBase.mass,
          charge := f LTMCTDimensionBase.charge, temperature := f LTMCTDimensionBase.temperature })
      f)
    LTMCTDimensionBase.temperature =
  f LTMCTDimensionBase.temperature rflAll goals completed! 🐙

The typed generic projection agrees with the bespoke LTMCTUnitChoices.toScale: reading LTMCTUnitChoices as a UnitSystem and forgetting to the magnitude layer is the same as the bespoke toScale.

lemma toScale_equivUnitSystem (u : LTMCTUnitChoices) :
    (equivUnitSystem u).toScale = u.toScale := byu:LTMCTUnitChoices⊢ (equivUnitSystem u).toScale = u.toScale
  refine UnitScale.ext ?_u:LTMCTUnitChoices⊢ (equivUnitSystem u).toScale.scale = u.toScale.scale
  funext bu:LTMCTUnitChoicesb:LTMCTDimensionBase⊢ (equivUnitSystem u).toScale.scale b = u.toScale.scale b
  cases blengthu:LTMCTUnitChoices⊢ (equivUnitSystem u).toScale.scale LTMCTDimensionBase.length = u.toScale.scale LTMCTDimensionBase.lengthtimeu:LTMCTUnitChoices⊢ (equivUnitSystem u).toScale.scale LTMCTDimensionBase.time = u.toScale.scale LTMCTDimensionBase.timemassu:LTMCTUnitChoices⊢ (equivUnitSystem u).toScale.scale LTMCTDimensionBase.mass = u.toScale.scale LTMCTDimensionBase.masschargeu:LTMCTUnitChoices⊢ (equivUnitSystem u).toScale.scale LTMCTDimensionBase.charge = u.toScale.scale LTMCTDimensionBase.chargetemperatureu:LTMCTUnitChoices⊢ (equivUnitSystem u).toScale.scale LTMCTDimensionBase.temperature = u.toScale.scale LTMCTDimensionBase.temperature <;>lengthu:LTMCTUnitChoices⊢ (equivUnitSystem u).toScale.scale LTMCTDimensionBase.length = u.toScale.scale LTMCTDimensionBase.lengthtimeu:LTMCTUnitChoices⊢ (equivUnitSystem u).toScale.scale LTMCTDimensionBase.time = u.toScale.scale LTMCTDimensionBase.timemassu:LTMCTUnitChoices⊢ (equivUnitSystem u).toScale.scale LTMCTDimensionBase.mass = u.toScale.scale LTMCTDimensionBase.masschargeu:LTMCTUnitChoices⊢ (equivUnitSystem u).toScale.scale LTMCTDimensionBase.charge = u.toScale.scale LTMCTDimensionBase.chargetemperatureu:LTMCTUnitChoices⊢ (equivUnitSystem u).toScale.scale LTMCTDimensionBase.temperature = u.toScale.scale LTMCTDimensionBase.temperature rflAll goals completed! 🐙

The bespoke scaling law is the generic fold

LTMCTUnitChoices.dimScale — the five explicit rpow factors written out by hand in Basic.lean — is exactly the generic UnitScale.dimScale fold (a Finset.prod over the basis) at the LTMCTDimensionBase instance, applied to toScale. This is what makes the typed layer a faithful wrapper rather than a second, independent statement of the scaling law: there is one source of truth, the generic fold on UnitScale B.

              

private lemma length_ratio (u1 u2 : LTMCTUnitChoices) :
    u1.length / u2.length = u1.toScale.scale .length / u2.toScale.scale .length := byu1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ u1.length / u2.length = u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length
  apply NNReal.equ1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑(u1.length / u2.length) = ↑(u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length); rw [LengthUnit.div_eq_val,u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.length.val / u2.length.val, ⋯⟩ =
  ↑(u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length)u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.length.val / u2.length.val, ⋯⟩ =
  ↑(u1.toScale.scale LTMCTDimensionBase.length) / ↑(u2.toScale.scale LTMCTDimensionBase.length) NNReal.coe_divu1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.length.val / u2.length.val, ⋯⟩ =
  ↑(u1.toScale.scale LTMCTDimensionBase.length) / ↑(u2.toScale.scale LTMCTDimensionBase.length)u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.length.val / u2.length.val, ⋯⟩ =
  ↑(u1.toScale.scale LTMCTDimensionBase.length) / ↑(u2.toScale.scale LTMCTDimensionBase.length)]u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.length.val / u2.length.val, ⋯⟩ =
  ↑(u1.toScale.scale LTMCTDimensionBase.length) / ↑(u2.toScale.scale LTMCTDimensionBase.length); rflAll goals completed! 🐙

private lemma time_ratio (u1 u2 : LTMCTUnitChoices) :
    u1.time / u2.time = u1.toScale.scale .time / u2.toScale.scale .time := byu1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ u1.time / u2.time = u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time
  apply NNReal.equ1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑(u1.time / u2.time) = ↑(u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time); rw [TimeUnit.div_eq_val,u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.time.val / u2.time.val, ⋯⟩ = ↑(u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time)u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.time.val / u2.time.val, ⋯⟩ =
  ↑(u1.toScale.scale LTMCTDimensionBase.time) / ↑(u2.toScale.scale LTMCTDimensionBase.time) NNReal.coe_divu1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.time.val / u2.time.val, ⋯⟩ =
  ↑(u1.toScale.scale LTMCTDimensionBase.time) / ↑(u2.toScale.scale LTMCTDimensionBase.time)u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.time.val / u2.time.val, ⋯⟩ =
  ↑(u1.toScale.scale LTMCTDimensionBase.time) / ↑(u2.toScale.scale LTMCTDimensionBase.time)]u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.time.val / u2.time.val, ⋯⟩ =
  ↑(u1.toScale.scale LTMCTDimensionBase.time) / ↑(u2.toScale.scale LTMCTDimensionBase.time); rflAll goals completed! 🐙

private lemma mass_ratio (u1 u2 : LTMCTUnitChoices) :
    u1.mass / u2.mass = u1.toScale.scale .mass / u2.toScale.scale .mass := byu1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ u1.mass / u2.mass = u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass
  apply NNReal.equ1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑(u1.mass / u2.mass) = ↑(u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass); rw [MassUnit.div_eq_val,u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.mass.val / u2.mass.val, ⋯⟩ = ↑(u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass)u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.mass.val / u2.mass.val, ⋯⟩ =
  ↑(u1.toScale.scale LTMCTDimensionBase.mass) / ↑(u2.toScale.scale LTMCTDimensionBase.mass) NNReal.coe_divu1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.mass.val / u2.mass.val, ⋯⟩ =
  ↑(u1.toScale.scale LTMCTDimensionBase.mass) / ↑(u2.toScale.scale LTMCTDimensionBase.mass)u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.mass.val / u2.mass.val, ⋯⟩ =
  ↑(u1.toScale.scale LTMCTDimensionBase.mass) / ↑(u2.toScale.scale LTMCTDimensionBase.mass)]u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.mass.val / u2.mass.val, ⋯⟩ =
  ↑(u1.toScale.scale LTMCTDimensionBase.mass) / ↑(u2.toScale.scale LTMCTDimensionBase.mass); rflAll goals completed! 🐙

private lemma charge_ratio (u1 u2 : LTMCTUnitChoices) :
    u1.charge / u2.charge = u1.toScale.scale .charge / u2.toScale.scale .charge := byu1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ u1.charge / u2.charge = u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge
  apply NNReal.equ1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑(u1.charge / u2.charge) = ↑(u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge); rw [ChargeUnit.div_eq_val,u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.charge.val / u2.charge.val, ⋯⟩ =
  ↑(u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge)u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.charge.val / u2.charge.val, ⋯⟩ =
  ↑(u1.toScale.scale LTMCTDimensionBase.charge) / ↑(u2.toScale.scale LTMCTDimensionBase.charge) NNReal.coe_divu1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.charge.val / u2.charge.val, ⋯⟩ =
  ↑(u1.toScale.scale LTMCTDimensionBase.charge) / ↑(u2.toScale.scale LTMCTDimensionBase.charge)u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.charge.val / u2.charge.val, ⋯⟩ =
  ↑(u1.toScale.scale LTMCTDimensionBase.charge) / ↑(u2.toScale.scale LTMCTDimensionBase.charge)]u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.charge.val / u2.charge.val, ⋯⟩ =
  ↑(u1.toScale.scale LTMCTDimensionBase.charge) / ↑(u2.toScale.scale LTMCTDimensionBase.charge); rflAll goals completed! 🐙

private lemma temperature_ratio (u1 u2 : LTMCTUnitChoices) :
    u1.temperature / u2.temperature =
      u1.toScale.scale .temperature / u2.toScale.scale .temperature := byu1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ u1.temperature / u2.temperature =
  u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature
  apply NNReal.equ1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑(u1.temperature / u2.temperature) =
  ↑(u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature); rw [TemperatureUnit.div_eq_val,u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.temperature.val / u2.temperature.val, ⋯⟩ =
  ↑(u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature)u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.temperature.val / u2.temperature.val, ⋯⟩ =
  ↑(u1.toScale.scale LTMCTDimensionBase.temperature) / ↑(u2.toScale.scale LTMCTDimensionBase.temperature) NNReal.coe_divu1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.temperature.val / u2.temperature.val, ⋯⟩ =
  ↑(u1.toScale.scale LTMCTDimensionBase.temperature) / ↑(u2.toScale.scale LTMCTDimensionBase.temperature)u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.temperature.val / u2.temperature.val, ⋯⟩ =
  ↑(u1.toScale.scale LTMCTDimensionBase.temperature) / ↑(u2.toScale.scale LTMCTDimensionBase.temperature)]u1:LTMCTUnitChoicesu2:LTMCTUnitChoices⊢ ↑⟨u1.temperature.val / u2.temperature.val, ⋯⟩ =
  ↑(u1.toScale.scale LTMCTDimensionBase.temperature) / ↑(u2.toScale.scale LTMCTDimensionBase.temperature); rflAll goals completed! 🐙

The hand-rolled five-factor LTMCTUnitChoices.dimScale equals the basis-generic UnitScale.dimScale fold at LTMCTDimensionBase, applied to toScale. The scaling law therefore has a single source of truth on the magnitude layer UnitScale B.


lemma dimScale_eq_toScale_dimScale (u1 u2 : LTMCTUnitChoices) (d : Dimension LTMCTDimensionBase) :
    u1.dimScale u2 d = UnitScale.dimScale u1.toScale u2.toScale d := byu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u1.dimScale u2) d = (u1.toScale.dimScale u2.toScale) d
  rw [dimScale_apply,u1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u1.length / u2.length) ^ ↑d.length * (u1.time / u2.time) ^ ↑d.time * (u1.mass / u2.mass) ^ ↑d.mass *
      (u1.charge / u2.charge) ^ ↑d.charge *
    (u1.temperature / u2.temperature) ^ ↑d.temperature =
  (u1.toScale.dimScale u2.toScale) du1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^ ↑d.length *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^ ↑d.time *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^ ↑d.mass *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^ ↑d.charge *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑d.temperature =
  (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^
            ↑(d.exponent LTMCTDimensionBase.length) *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^
            ↑(d.exponent LTMCTDimensionBase.time) *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^
          ↑(d.exponent LTMCTDimensionBase.mass) *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^
        ↑(d.exponent LTMCTDimensionBase.charge) *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑(d.exponent LTMCTDimensionBase.temperature) length_ratio,u1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^ ↑d.length *
          (u1.time / u2.time) ^ ↑d.time *
        (u1.mass / u2.mass) ^ ↑d.mass *
      (u1.charge / u2.charge) ^ ↑d.charge *
    (u1.temperature / u2.temperature) ^ ↑d.temperature =
  (u1.toScale.dimScale u2.toScale) du1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^ ↑d.length *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^ ↑d.time *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^ ↑d.mass *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^ ↑d.charge *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑d.temperature =
  (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^
            ↑(d.exponent LTMCTDimensionBase.length) *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^
            ↑(d.exponent LTMCTDimensionBase.time) *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^
          ↑(d.exponent LTMCTDimensionBase.mass) *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^
        ↑(d.exponent LTMCTDimensionBase.charge) *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑(d.exponent LTMCTDimensionBase.temperature) time_ratio,u1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^ ↑d.length *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^ ↑d.time *
        (u1.mass / u2.mass) ^ ↑d.mass *
      (u1.charge / u2.charge) ^ ↑d.charge *
    (u1.temperature / u2.temperature) ^ ↑d.temperature =
  (u1.toScale.dimScale u2.toScale) du1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^ ↑d.length *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^ ↑d.time *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^ ↑d.mass *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^ ↑d.charge *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑d.temperature =
  (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^
            ↑(d.exponent LTMCTDimensionBase.length) *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^
            ↑(d.exponent LTMCTDimensionBase.time) *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^
          ↑(d.exponent LTMCTDimensionBase.mass) *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^
        ↑(d.exponent LTMCTDimensionBase.charge) *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑(d.exponent LTMCTDimensionBase.temperature) mass_ratio,u1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^ ↑d.length *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^ ↑d.time *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^ ↑d.mass *
      (u1.charge / u2.charge) ^ ↑d.charge *
    (u1.temperature / u2.temperature) ^ ↑d.temperature =
  (u1.toScale.dimScale u2.toScale) du1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^ ↑d.length *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^ ↑d.time *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^ ↑d.mass *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^ ↑d.charge *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑d.temperature =
  (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^
            ↑(d.exponent LTMCTDimensionBase.length) *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^
            ↑(d.exponent LTMCTDimensionBase.time) *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^
          ↑(d.exponent LTMCTDimensionBase.mass) *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^
        ↑(d.exponent LTMCTDimensionBase.charge) *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑(d.exponent LTMCTDimensionBase.temperature) charge_ratio,u1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^ ↑d.length *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^ ↑d.time *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^ ↑d.mass *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^ ↑d.charge *
    (u1.temperature / u2.temperature) ^ ↑d.temperature =
  (u1.toScale.dimScale u2.toScale) du1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^ ↑d.length *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^ ↑d.time *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^ ↑d.mass *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^ ↑d.charge *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑d.temperature =
  (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^
            ↑(d.exponent LTMCTDimensionBase.length) *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^
            ↑(d.exponent LTMCTDimensionBase.time) *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^
          ↑(d.exponent LTMCTDimensionBase.mass) *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^
        ↑(d.exponent LTMCTDimensionBase.charge) *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑(d.exponent LTMCTDimensionBase.temperature) temperature_ratio,u1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^ ↑d.length *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^ ↑d.time *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^ ↑d.mass *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^ ↑d.charge *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑d.temperature =
  (u1.toScale.dimScale u2.toScale) du1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^ ↑d.length *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^ ↑d.time *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^ ↑d.mass *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^ ↑d.charge *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑d.temperature =
  (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^
            ↑(d.exponent LTMCTDimensionBase.length) *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^
            ↑(d.exponent LTMCTDimensionBase.time) *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^
          ↑(d.exponent LTMCTDimensionBase.mass) *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^
        ↑(d.exponent LTMCTDimensionBase.charge) *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑(d.exponent LTMCTDimensionBase.temperature)
    UnitScale.dimScale,u1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^ ↑d.length *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^ ↑d.time *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^ ↑d.mass *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^ ↑d.charge *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑d.temperature =
  { toFun := fun d => ∏ b, (u1.toScale.scale b / u2.toScale.scale b) ^ ↑(d.exponent b), map_one' := ⋯, map_mul' := ⋯ } du1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^ ↑d.length *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^ ↑d.time *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^ ↑d.mass *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^ ↑d.charge *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑d.temperature =
  (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^
            ↑(d.exponent LTMCTDimensionBase.length) *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^
            ↑(d.exponent LTMCTDimensionBase.time) *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^
          ↑(d.exponent LTMCTDimensionBase.mass) *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^
        ↑(d.exponent LTMCTDimensionBase.charge) *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑(d.exponent LTMCTDimensionBase.temperature) MonoidHom.coe_mk,u1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^ ↑d.length *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^ ↑d.time *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^ ↑d.mass *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^ ↑d.charge *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑d.temperature =
  { toFun := fun d => ∏ b, (u1.toScale.scale b / u2.toScale.scale b) ^ ↑(d.exponent b), map_one' := ⋯ } du1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^ ↑d.length *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^ ↑d.time *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^ ↑d.mass *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^ ↑d.charge *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑d.temperature =
  (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^
            ↑(d.exponent LTMCTDimensionBase.length) *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^
            ↑(d.exponent LTMCTDimensionBase.time) *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^
          ↑(d.exponent LTMCTDimensionBase.mass) *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^
        ↑(d.exponent LTMCTDimensionBase.charge) *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑(d.exponent LTMCTDimensionBase.temperature) OneHom.coe_mk,u1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^ ↑d.length *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^ ↑d.time *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^ ↑d.mass *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^ ↑d.charge *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑d.temperature =
  ∏ b, (u1.toScale.scale b / u2.toScale.scale b) ^ ↑(d.exponent b)u1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^ ↑d.length *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^ ↑d.time *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^ ↑d.mass *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^ ↑d.charge *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑d.temperature =
  (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^
            ↑(d.exponent LTMCTDimensionBase.length) *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^
            ↑(d.exponent LTMCTDimensionBase.time) *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^
          ↑(d.exponent LTMCTDimensionBase.mass) *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^
        ↑(d.exponent LTMCTDimensionBase.charge) *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑(d.exponent LTMCTDimensionBase.temperature) prod_univ_LTMCTDimensionBaseu1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^ ↑d.length *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^ ↑d.time *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^ ↑d.mass *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^ ↑d.charge *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑d.temperature =
  (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^
            ↑(d.exponent LTMCTDimensionBase.length) *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^
            ↑(d.exponent LTMCTDimensionBase.time) *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^
          ↑(d.exponent LTMCTDimensionBase.mass) *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^
        ↑(d.exponent LTMCTDimensionBase.charge) *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑(d.exponent LTMCTDimensionBase.temperature)u1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^ ↑d.length *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^ ↑d.time *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^ ↑d.mass *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^ ↑d.charge *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑d.temperature =
  (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^
            ↑(d.exponent LTMCTDimensionBase.length) *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^
            ↑(d.exponent LTMCTDimensionBase.time) *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^
          ↑(d.exponent LTMCTDimensionBase.mass) *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^
        ↑(d.exponent LTMCTDimensionBase.charge) *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑(d.exponent LTMCTDimensionBase.temperature)]u1:LTMCTUnitChoicesu2:LTMCTUnitChoicesd:Dimension LTMCTDimensionBase⊢ (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^ ↑d.length *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^ ↑d.time *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^ ↑d.mass *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^ ↑d.charge *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑d.temperature =
  (u1.toScale.scale LTMCTDimensionBase.length / u2.toScale.scale LTMCTDimensionBase.length) ^
            ↑(d.exponent LTMCTDimensionBase.length) *
          (u1.toScale.scale LTMCTDimensionBase.time / u2.toScale.scale LTMCTDimensionBase.time) ^
            ↑(d.exponent LTMCTDimensionBase.time) *
        (u1.toScale.scale LTMCTDimensionBase.mass / u2.toScale.scale LTMCTDimensionBase.mass) ^
          ↑(d.exponent LTMCTDimensionBase.mass) *
      (u1.toScale.scale LTMCTDimensionBase.charge / u2.toScale.scale LTMCTDimensionBase.charge) ^
        ↑(d.exponent LTMCTDimensionBase.charge) *
    (u1.toScale.scale LTMCTDimensionBase.temperature / u2.toScale.scale LTMCTDimensionBase.temperature) ^
      ↑(d.exponent LTMCTDimensionBase.temperature)
  simp only [Dimension.length, Dimension.time, Dimension.mass, Dimension.charge,
    Dimension.temperature]All goals completed! 🐙

Unit systems, parametrised in a dimension basis

The LTMCTDimensionBase catalog

LTMCTUnitChoices is UnitSystem LTMCTDimensionBase

The bespoke scaling law is the generic fold

The `LTMCTDimensionBase` catalog

`LTMCTUnitChoices` is `UnitSystem LTMCTDimensionBase`