Physlib.Units.SIUnitChoices

For any unit of electric current $x$ (of type `CurrentUnit`), its numerical magnitude $x.\text{val}$ is non-zero.

For any electric current unit $x$, its numerical magnitude $x.\text{val}$ is strictly greater than zero ($x.\text{val} > 0$).

The type `CurrentUnit` is inhabited, meaning it has a designated default element. This default current unit is defined to have a magnitude of $1$.

For any two current units $x$ and $y$ of type `CurrentUnit`, their division $x / y$ is defined as the ratio of their numerical magnitudes, $\frac{x.\text{val}}{y.\text{val}}$, resulting in a non-negative real number in $\mathbb{R}_{\ge 0}$.

For any two electric current units $x$ and $y$ of type `CurrentUnit`, the quotient $x / y$ is equal to the ratio of their numerical magnitudes $\frac{x.\text{val}}{y.\text{val}}$, expressed as a non-negative real number in $\mathbb{R}_{\ge 0}$.

The constant `CurrentUnit.amperes` represents the ampere, which is the coherent SI unit of electric current. It is defined as an element of the type `CurrentUnit` with a numerical magnitude of $1$.

For any unit of amount of substance $x$ (an element of the type `AmountUnit`), its numerical magnitude $x.\text{val}$ is non-zero, i.e., $x.\text{val} \neq 0$.

For any unit of amount of substance $x$, its numerical magnitude $x.\text{val}$ is strictly positive, such that $x.\text{val} > 0$.

The type $\text{AmountUnit}$, which represents units for the amount of substance, is inhabited. Its default element is defined as the unit with a numerical magnitude of $1$.

The division of two units of amount of substance $x, y \in \text{AmountUnit}$ is defined as the ratio of their magnitudes, resulting in a non-negative real number $x/y \in \mathbb{R}_{\ge 0}$.

For any two units of amount of substance $x$ and $y$, their quotient $x / y$ is equal to the non-negative real number formed by the ratio of their numerical magnitudes, $\frac{x.\text{val}}{y.\text{val}}$.

The mole ($\text{mol}$) is defined as the coherent SI unit for the base quantity of amount of substance, represented as an element of `AmountUnit` with a magnitude of $1$.

For any unit of luminous intensity $x$, its numerical magnitude $x.\text{val}$ is non-zero.

For any luminous intensity unit $x$, its numerical magnitude $x.\text{val}$ is strictly greater than zero ($x.\text{val} > 0$).

The type `LuminousIntensityUnit`, which represents units of luminous intensity, is inhabited. Its default element is defined as the unit with a magnitude of $1$.

The division operator between two units of luminous intensity, $x$ and $y$, results in a non-negative real number $\mathbb{R}_{\ge 0}$. The value of $x / y$ is defined as the ratio of their underlying magnitudes $\frac{x.\text{val}}{y.\text{val}}$.

For any two units of luminous intensity $x$ and $y$, the result of the division $x / y$ is the non-negative real number $\mathbb{R}_{\ge 0}$ obtained by taking the ratio of their respective numerical magnitudes, $\frac{x.\text{val}}{y.\text{val}}$.

The constant represents the candela, which is the coherent SI unit for luminous intensity. It is defined as an element of the `LuminousIntensityUnit` type with a numerical magnitude of $1$.

This instance defines the `UnitMagnitudeCatalog` for the seven base quantities of the International System of Quantities (ISQ). It maps each base dimension in `ISQDimensionBase` to its corresponding unit type: - Length $\to$ `LengthUnit` - Mass $\to$ `MassUnit` - Time $\to$ `TimeUnit` - Electric current $\to$ `CurrentUnit` - Thermodynamic temperature $\to$ `TemperatureUnit` - Amount of substance $\to$ `AmountUnit` - Luminous intensity $\to$ `LuminousIntensityUnit` For any unit $u$ belonging to one of these types, the magnitude function $\text{mag}(u)$ returns its underlying value $u.\text{val}$ as a positive real number in $\mathbb{R}_{>0}$.

Let $M$ be a commutative monoid and $f : \text{ISQDimensionBase} \to M$ be a function. The product of $f(b)$ over all base quantities $b$ in the International System of Quantities (ISQ) is given by: $$\prod_{b \in \text{ISQDimensionBase}} f(b) = f(\text{length}) \cdot f(\text{mass}) \cdot f(\text{time}) \cdot f(\text{current}) \cdot f(\text{temperature}) \cdot f(\text{amount}) \cdot f(\text{luminousIntensity})$$ Here, $\text{ISQDimensionBase}$ is the set of the seven fundamental base quantities: length, mass, time, electric current, thermodynamic temperature, amount of substance, and luminous intensity.

`SIUnitChoices` is the type of unit systems defined over the seven base quantities of the International System of Quantities (ISQ). An element of this type is a function $u$ that assigns a specific typed unit to each of the seven fundamental dimensions: 1. Length ($L$) $\to u(L) \in \text{LengthUnit}$ 2. Mass ($M$) $\to u(M) \in \text{MassUnit}$ 3. Time ($T$) $\to u(T) \in \text{TimeUnit}$ 4. Electric current ($I$) $\to u(I) \in \text{CurrentUnit}$ 5. Thermodynamic temperature ($\Theta$) $\to u(\Theta) \in \text{TemperatureUnit}$ 6. Amount of substance ($N$) $\to u(N) \in \text{AmountUnit}$ 7. Luminous intensity ($J$) $\to u(J) \in \text{LuminousIntensityUnit}$ This structure allows for the formal representation of specific unit systems (such as the coherent SI system) by providing a "slot" for a unit of the appropriate type for every ISQ base dimension.

The coherent SI unit choice is the specific element of `SIUnitChoices` that maps each of the seven base quantities of the International System of Quantities (ISQ) to its standard coherent SI base unit. This mapping $u_{\text{SI}}$ is defined as: - $u_{\text{SI}}(\text{length}) = \text{metre}$ - $u_{\text{SI}}(\text{mass}) = \text{kilogram}$ - $u_{\text{SI}}(\text{time}) = \text{second}$ - $u_{\text{SI}}(\text{current}) = \text{ampere}$ - $u_{\text{SI}}(\text{temperature}) = \text{kelvin}$ - $u_{\text{SI}}(\text{amount}) = \text{mole}$ - $u_{\text{SI}}(\text{luminousIntensity}) = \text{candela}$

For two unit systems $u_1, u_2 \in \text{SIUnitChoices}$ defined over the seven ISQ base quantities (length, mass, time, electric current, thermodynamic temperature, amount of substance, and luminous intensity), `SIUnitChoices.dimScale u1 u2` is the group homomorphism from the group of physical dimensions $\text{Dimension}(\text{ISQDimensionBase})$ to the non-negative real numbers $\mathbb{R}_{\ge 0}$. For any dimension $d$, this homomorphism returns the numerical scaling factor between the units chosen by system $u_1$ and those chosen by system $u_2$.

For any unit system $u \in \text{SIUnitChoices}$ and any physical dimension $d$ defined over the seven ISQ base quantities (length, mass, time, electric current, thermodynamic temperature, amount of substance, and luminous intensity), the numerical scaling factor between the unit system $u$ and itself for the dimension $d$ is $1$. That is, $\text{dimScale}(u, u, d) = 1$.

For any unit of luminous intensity $x$ and any positive real number $r$, the ratio of the unit $x$ scaled by $r$ (denoted $\text{scale}(r, x)$) to the original unit $x$ is equal to $r$. Here, the division of two units results in a non-negative real number $\mathbb{R}_{\ge 0}$.

For any unit of luminous intensity $x$ and any positive real number $r > 0$, the ratio of $x$ to the unit $x$ scaled by $r$ (denoted by $\text{scale}(r, x)$) is equal to the non-negative real number $1/r \in \mathbb{R}_{\ge 0}$.

For any unit of luminous intensity $x$, scaling $x$ by a factor of $1$ is equal to $x$.

For any units of luminous intensity $x_1$ and $x_2$, and any positive real numbers $r_1, r_2 > 0$, the ratio of the scaled units is given by $$\frac{\text{scale}(r_1, x_1)}{\text{scale}(r_2, x_2)} = \frac{r_1}{r_2} \cdot \frac{x_1}{x_2}$$ where $\text{scale}(r, x)$ denotes the unit $x$ scaled by the factor $r$, and the division of units results in a value in the non-negative real numbers $\mathbb{R}_{\ge 0}$.

Let $x$ be a unit of luminous intensity. For any positive real numbers $r_1, r_2 \in \mathbb{R}$, scaling the unit $x$ by $r_2$ and then scaling the resulting unit by $r_1$ is equivalent to scaling the original unit $x$ by the product $r_1 r_2$. That is, $$\text{scale}(r_1, \text{scale}(r_2, x)) = \text{scale}(r_1 r_2, x).$$