Physlib.Units.UnitSystem

Given a dimension basis $B$ and a unit magnitude catalog that provides a type of units $\text{Unit}(b)$ for each base dimension $b \in B$, a **unit system** is defined as a function $u$ that maps each base dimension $b \in B$ to a specific unit $u(b)$ of type $\text{Unit}(b)$. This structure serves as the formal representation of physical unit systems such as SI or CGS, ensuring that for every base dimension, exactly one unit is chosen from the available options in the catalog.

Let $B$ be a dimension basis. For any two unit systems $u$ and $v$ over $B$, if they select the same unit for every base dimension $b \in B$ (i.e., $u(b) = v(b)$ for all $b \in B$), then the unit systems are equal ($u = v$).

The function maps a unit system $u$ over a dimension basis $B$ to its corresponding `UnitScale B`. For each base dimension $b \in B$, the resulting scale value is the numerical magnitude $\text{mag}(u(b))$ of the unit $u(b)$ chosen by the system. This transformation effectively "forgets" the specific unit types associated with the system $u$ and retains only their positive real magnitudes.

Let $B$ be a dimension basis and $u$ be a unit system over $B$. For any base dimension $b \in B$, the numerical scale value of the unit system at $b$, denoted by $(\text{toScale}(u)).\text{scale}(b)$, is equal to the magnitude of the unit $u(b)$ chosen by the system for that dimension, denoted by $\text{mag}(u(b))$.

The `UnitMagnitudeCatalog` instance for the basis of physical dimensions consisting of length, time, mass, charge, and temperature (LTMCT). For each dimension in the basis $b \in \{ \text{length, time, mass, charge, temperature} \}$, the catalog specifies the set of available units as the types `LengthUnit`, `TimeUnit`, `MassUnit`, `ChargeUnit`, and `TemperatureUnit`, respectively. The magnitude function $\text{mag}$ maps a unit $u$ to its underlying numerical value in $\mathbb{R}_{>0}$.

The equivalence $\text{LTMCTUnitChoices} \simeq \text{UnitSystem LTMCTDimensionBase}$ establishes that the bespoke record type containing five fields (length, time, mass, charge, and temperature) and the generic unit system defined over the LTMCT dimension basis represent the same data. The mapping identifies the record fields $u.\text{length}$, $u.\text{time}$, $u.\text{mass}$, $u.\text{charge}$, and $u.\text{temperature}$ with the values of a function $f$ applied to the corresponding elements of the basis $\text{LTMCTDimensionBase} = \{\text{length}, \text{time}, \text{mass}, \text{charge}, \text{temperature}\}$.

For any choice of base units $u$ represented by the record type `LTMCTUnitChoices`, the `UnitScale` obtained by viewing $u$ as a generic unit system (via the equivalence $\text{equivUnitSystem}: \text{LTMCTUnitChoices} \simeq \text{UnitSystem LTMCTDimensionBase}$) and then projecting it to its numerical magnitudes is equal to the scale obtained through the specific `toScale` function defined for `LTMCTUnitChoices`. That is, $(\text{equivUnitSystem}(u)).\text{toScale} = u.\text{toScale}$.

Let $M$ be a commutative monoid and $f: \text{LTMCTDimensionBase} \to M$ be a function. The product of $f(b)$ over all elements $b$ in the set of base dimensions $\text{LTMCTDimensionBase} = \{\text{length}, \text{time}, \text{mass}, \text{charge}, \text{temperature}\}$ is equal to the product of the function values for each specific dimension in their canonical order: $$\prod_{b \in \text{LTMCTDimensionBase}} f(b) = f(\text{length}) \cdot f(\text{time}) \cdot f(\text{mass}) \cdot f(\text{charge}) \cdot f(\text{temperature})$$

For any two unit systems $u_1$ and $u_2$ represented as `LTMCTUnitChoices` (which define specific units for length, time, mass, charge, and temperature) and for any physical dimension $d$ in the $LTMCT$ basis, the bespoke scaling factor $u_1.\text{dimScale}(u_2, d)$ is equal to the generic scaling factor $\text{UnitScale.dimScale}(\text{toScale}(u_1), \text{toScale}(u_2), d)$ calculated at the magnitude layer. This result establishes that the explicitly defined five-factor scaling law matches the general basis-generic product definition.