1. Physlib
  2. Units
  3. ParametricUnits
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.Basic

The unit side, parametrised in the same basis

The dimension basis is parametric (Dimension B), but the unit side of the bridge is hardwired in parallel: UnitChoices has five named unit fields and UnitChoices.dimScale folds over exactly those five. This module provides the generic twin, parametrised in the same basis B.

Every PhysLib base unit (LengthUnit, TimeUnit, …) is, structurally, a positive real ({ val : ℝ // 0 < val }); the typed names carry no extra algebraic content. So a unit choice over a basis B is a positive real per base dimension, and the scaling homomorphism folds the per-base unit ratio over B:

    UnitScale B — a positive-real magnitude for each b : B.

    UnitScale.dimScale : UnitScale B → UnitScale B → Dimension B →* ℝ≥0 — the MonoidHom d ↦ ∏ b, (u₁ b / u₂ b) ^ d.exponent b, generic in B.

The current five-field UnitChoices.dimScale is the LTMCTDimensionBase instance of this fold, written out by hand; UnitChoices.toScale exhibits the correspondence.

@[expose] public section

A choice of unit for each base dimension of B: a positive-real magnitude per base. This is the basis-generic form of UnitChoices.

The positive-real magnitude of the chosen unit at each base dimension.

Each chosen unit has a positive magnitude.

structure UnitScale (B : Type) where scale : B → ℝ≥0 scale_pos : ∀ b, 0 < scale b
lemma ratio_ne_zero (u1 u2 : UnitScale B) (b : B) : u1.scale b / u2.scale b ≠ 0 := (div_pos (u1.scale_pos b) (u2.scale_pos b)).ne'All goals completed! 🐙@[simp] lemma dimScale_one [Fintype B] (u1 u2 : UnitScale B) : dimScale u1 u2 1 = 1 := map_one _

The scaling is transitive (a cocycle in the unit choices).

All goals completed! 🐙

The current five-field UnitChoices is the LTMCTDimensionBase instance

UnitChoices.toScale reads the five typed units as a UnitScale LTMCTDimensionBase, exhibiting the existing bespoke dimScale as the LTMCTDimensionBase case of the generic fold.