Physlib.Units.Basic

Given two sets of unit choices $u_1$ and $u_2$, this function defines a monoid homomorphism from physical dimensions to the non-negative real numbers $\mathbb{R}_{\ge 0}$. For a dimension $d$, it computes the scaling factor $\sigma \in \mathbb{R}_{\ge 0}$ used to convert a quantity of dimension $d$ from unit system $u_1$ to $u_2$. This factor is calculated as the product of the ratios of the fundamental units (length, time, mass, charge, and temperature) in $u_1$ and $u_2$, each raised to the power of the corresponding component in the dimension $d$: $$\sigma = \left(\frac{u_{1, \text{length}}}{u_{2, \text{length}}}\right)^{d.\text{length}} \cdot \left(\frac{u_{1, \text{time}}}{u_{2, \text{time}}}\right)^{d.\text{time}} \cdot \left(\frac{u_{1, \text{mass}}}{u_{2, \text{mass}}}\right)^{d.\text{mass}} \cdot \left(\frac{u_{1, \text{charge}}}{u_{2, \text{charge}}}\right)^{d.\text{charge}} \cdot \left(\frac{u_{1, \text{temp}}}{u_{2, \text{temp}}}\right)^{d.\text{temp}}$$ where the exponents $d.i$ are the rational powers associated with each fundamental dimension.

Given two sets of unit choices $u_1$ and $u_2$ and a physical dimension $d$, the scaling factor $\text{dimScale}(u_1, u_2, d)$ is calculated as the product of the ratios of the fundamental units in $u_1$ and $u_2$, each raised to the power of the corresponding component in the dimension $d$: $$\text{dimScale}(u_1, u_2, d) = \left(\frac{u_{1, \text{length}}}{u_{2, \text{length}}}\right)^{d.\text{length}} \cdot \left(\frac{u_{1, \text{time}}}{u_{2, \text{time}}}\right)^{d.\text{time}} \cdot \left(\frac{u_{1, \text{mass}}}{u_{2, \text{mass}}}\right)^{d.\text{mass}} \cdot \left(\frac{u_{1, \text{charge}}}{u_{2, \text{charge}}}\right)^{d.\text{charge}} \cdot \left(\frac{u_{1, \text{temp}}}{u_{2, \text{temp}}}\right)^{d.\text{temp}}$$ where $u_{i, \text{type}}$ represents the fundamental unit of a specific type (length, time, mass, charge, or temperature) in unit system $u_i$, and $d.\text{type}$ represents the rational exponent of that fundamental dimension in $d$.

For any set of unit choices $u$ and any physical dimension $d$, the scaling factor $\text{dimScale}(u, u, d)$ used to convert a quantity of dimension $d$ from unit system $u$ to itself is equal to $1$.

For any two systems of unit choices $u_1$ and $u_2$, the scaling factor associated with the identity dimension (dimensionless quantity) $1$ is equal to $1$.

For any three sets of unit choices $u_1, u_2, u_3$ and any physical dimension $d$, the scaling factor $\text{dimScale}(u_1, u_2, d) \in \mathbb{R}_{\ge 0}$ used to convert a quantity of dimension $d$ from unit system $u_1$ to $u_2$ satisfies the transitivity property: $$\text{dimScale}(u_1, u_2, d) \cdot \text{dimScale}(u_2, u_3, d) = \text{dimScale}(u_1, u_3, d)$$

For any two systems of unit choices $u_1$ and $u_2$ and any physical dimension $d$, the product of the scaling factor $\text{dimScale}(u_1, u_2, d) \in \mathbb{R}_{\ge 0}$ (used to convert a quantity of dimension $d$ from unit system $u_1$ to $u_2$) and the scaling factor $\text{dimScale}(u_2, u_1, d)$ (used for the reverse conversion) is equal to $1$: $$\text{dimScale}(u_1, u_2, d) \cdot \text{dimScale}(u_2, u_1, d) = 1$$

For any two systems of unit choices $u_1, u_2$ and any physical dimension $d$, let $\text{dimScale}(u_1, u_2, d) \in \mathbb{R}_{\ge 0}$ be the factor used to convert a quantity of dimension $d$ from unit system $u_1$ to $u_2$. The product of this scaling factor and its reverse counterpart $\text{dimScale}(u_2, u_1, d)$, when converted to real numbers, is equal to $1$: $$\text{toReal}(\text{dimScale}(u_1, u_2, d)) \cdot \text{toReal}(\text{dimScale}(u_2, u_1, d)) = 1$$

For any two systems of unit choices $u_1, u_2 \in \text{UnitChoices}$ and any physical dimension $d \in \text{Dimension}$, the scaling factor $\text{dimScale}(u_1, u_2, d) \in \mathbb{R}_{\ge 0}$ is non-zero. This scaling factor represents the product of the ratios of fundamental units in $u_1$ and $u_2$ raised to the powers specified by the dimension $d$, used to convert physical quantities between the two unit systems.

For any two systems of unit choices $u_1, u_2 \in \text{UnitChoices}$ and any physical dimension $d \in \text{Dimension}$, the scaling factor $\text{dimScale}(u_1, u_2, d) \in \mathbb{R}_{\ge 0}$ used to convert quantities of dimension $d$ from unit system $u_1$ to $u_2$ is the multiplicative inverse of the scaling factor for the reverse conversion. That is, $$\text{dimScale}(u_1, u_2, d) = (\text{dimScale}(u_2, u_1, d))^{-1}$$

For any two systems of unit choices $u_1, u_2 \in \text{UnitChoices}$ and any physical dimension $d \in \text{Dimension}$, the scaling factor for the inverse dimension $d^{-1}$ from unit system $u_1$ to $u_2$ is equal to the scaling factor for the original dimension $d$ when converting from unit system $u_2$ to $u_1$. That is, $$\text{dimScale}(u_1, u_2, d^{-1}) = \text{dimScale}(u_2, u_1, d)$$

Let $M$ be a type equipped with a scalar action of the non-negative real numbers $\mathbb{R}_{\ge 0}$. For any two systems of unit choices $u_1, u_2$ and any physical dimension $d$, let $\sigma = \text{dimScale}(u_1, u_2, d) \in \mathbb{R}_{\ge 0}$ be the scaling factor associated with converting quantities of dimension $d$ from unit system $u_1$ to $u_2$. For any two elements $m_1, m_2 \in M$, the result of scaling by $\sigma$ is equal if and only if the original elements are equal: $$\sigma \cdot m_1 = \sigma \cdot m_2 \iff m_1 = m_2$$

For any two systems of unit choices $u_1, u_2 \in \text{UnitChoices}$ and any physical dimension $d \in \text{Dimension}$, the scaling factor $\text{dimScale}(u_1, u_2, d) \in \mathbb{R}_{\ge 0}$ used to convert physical quantities of dimension $d$ from unit system $u_1$ to $u_2$ is strictly positive: $$\text{dimScale}(u_1, u_2, d) > 0$$

The definition `UnitChoices.SI` represents the choice of base physical units corresponding to the International System of Units (SI). It is a structure of type `UnitChoices` where the fundamental units are assigned as follows: - The unit of length is meters. - The unit of time is seconds. - The unit of mass is kilograms. - The unit of charge is coulombs. - The unit of temperature is kelvin.

In the International System of Units ($\text{SI}$), the base unit assigned to the length dimension is the meter: $$\text{SI.length} = \text{LengthUnit.meters}$$

In the International System of Units ($SI$), the fundamental unit chosen for the dimension of time is the second ($TimeUnit.seconds$).

In the International System of Units (SI), the designated fundamental unit for the mass dimension is the kilogram.

In the International System of Units (SI), the assigned base unit for physical charge is the coulomb.

In the International System of Units (SI), the base unit for temperature is defined as Kelvin.

`UnitChoices.SIPrimed` is a specific set of unit choices derived from the International System of Units (SI) where each base unit is scaled by a distinct prime number. It is defined as follows: - Length: $2 \times \text{meters}$ - Time: $3 \times \text{seconds}$ - Mass: $5 \times \text{kilograms}$ - Charge: $7 \times \text{coulombs}$ - Temperature: $11 \times \text{kelvin}$ This configuration is primarily used to verify the dimensional correctness of physical expressions, as the prime scaling ensures that different combinations of base dimensions result in unique scaling factors.

For any physical dimension $d$, the scaling factor $\text{dimScale}(SI, SI', d)$ required to convert a quantity from the International System of Units ($SI$) to the prime-scaled system ($SI'$) is given by the product: $$\text{dimScale}(SI, SI', d) = (2^{-1})^{d.\text{length}} \cdot (3^{-1})^{d.\text{time}} \cdot (5^{-1})^{d.\text{mass}} \cdot (7^{-1})^{d.\text{charge}} \cdot (11^{-1})^{d.\text{temperature}}$$ where $d.\text{length}, d.\text{time}, d.\text{mass}, d.\text{charge}$, and $d.\text{temperature}$ are the rational components of the dimension $d$. This factor arises because the base units in $SI'$ (meters, seconds, kilograms, coulombs, and kelvin) are scaled by the factors 2, 3, 5, 7, and 11, respectively, relative to $SI$.

For any physical dimension $d$, the scaling factor $\text{dimScale}(SI', SI, d)$ required to convert a quantity from the prime-scaled system ($SI'$) to the International System of Units ($SI$) is given by the product: $$\text{dimScale}(SI', SI, d) = 2^{d.\text{length}} \cdot 3^{d.\text{time}} \cdot 5^{d.\text{mass}} \cdot 7^{d.\text{charge}} \cdot 11^{d.\text{temperature}}$$ where $d.\text{length}, d.\text{time}, d.\text{mass}, d.\text{charge}$, and $d.\text{temperature}$ are the rational components (exponents) of the dimension $d$. This factor corresponds to the ratios of the base units in $SI'$ relative to $SI$, which are scaled by factors of 2 (length), 3 (time), 5 (mass), 7 (charge), and 11 (temperature).

Let $M$ be a type that carries a physical dimension, denoted as $d = \text{dim} M$. A function $f: \text{UnitChoices} \to M$, representing a quantity whose value depends on the chosen system of units, satisfies the property **HasDimension** if it scales correctly under a change of units. Specifically, for any two unit choices $u_1, u_2 \in \text{UnitChoices}$, the value of the function at $u_2$ must relate to the value at $u_1$ by: $$f(u_2) = \text{dimScale}(u_1, u_2, d) \cdot f(u_1)$$ where $\text{dimScale}(u_1, u_2, d) \in \mathbb{R}_{\ge 0}$ is the scaling factor associated with dimension $d$ for the transition from unit system $u_1$ to $u_2$, and the multiplication represents the action of non-negative reals on $M$.

Let $M$ be a type that carries a physical dimension, denoted as $\text{dim} M$. For any function $f: \text{UnitChoices} \to M$, the property **HasDimension** $f$ holds if and only if for all unit choices $u_1, u_2 \in \text{UnitChoices}$, the value of the function at $u_2$ is related to the value at $u_1$ by the scaling factor associated with the dimension of $M$: $$f(u_2) = \text{dimScale}(u_1, u_2, \text{dim} M) \cdot f(u_1)$$ where $\text{dimScale}(u_1, u_2, \text{dim} M) \in \mathbb{R}_{\ge 0}$ is the scaling factor for the transition from unit system $u_1$ to $u_2$, and the multiplication represents the action of non-negative reals on $M$.

Let $M$ be a type that carries a physical dimension, denoted as $\text{dim} M$. The type **Dimensionful $M$** is defined as the set of functions $f: \text{UnitChoices} \to M$ that are consistent with the dimension of $M$. Specifically, a function $f$ belongs to this type if, for all pairs of unit choices $u_1, u_2 \in \text{UnitChoices}$, it satisfies the scaling relation: $$f(u_2) = \text{dimScale}(u_1, u_2, \text{dim} M) \cdot f(u_1)$$ where $\text{dimScale}(u_1, u_2, \text{dim} M) \in \mathbb{R}_{\ge 0}$ is the scaling factor associated with the dimension of $M$ for the transition from the unit system $u_1$ to $u_2$, and the multiplication denotes the action of non-negative reals on $M$.

For any type $M$ that carries a physical dimension, an element $f$ of the type **Dimensionful $M$** can be treated as a function from the set of unit choices $\text{UnitChoices}$ to $M$. This coercion allows a dimensionful quantity to be evaluated at a specific system of units $u \in \text{UnitChoices}$ to return its value in $M$.

Let $M$ be a type that carries a physical dimension. For any two dimensionful quantities $f_1, f_2 \in \text{Dimensionful } M$, if their underlying functions $f_1, f_2: \text{UnitChoices} \to M$ are equal, then the dimensionful quantities themselves are equal ($f_1 = f_2$).

Let $M$ be a type that carries a physical dimension. The space of dimensionful quantities of type $M$, denoted as $\text{Dimensionful } M$, is equipped with a scalar action by the non-negative real numbers $\mathbb{R}_{\ge 0}$. For any scalar $a \in \mathbb{R}_{\ge 0}$ and any dimensionful quantity $f \in \text{Dimensionful } M$, the action $a \cdot f$ is defined pointwise for each choice of units $u \in \text{UnitChoices}$ as: $$(a \cdot f)(u) = a \cdot f(u)$$ where the right-hand side is the action of $\mathbb{R}_{\ge 0}$ on $M$. This operation satisfies the axioms of a multiplicative action: $1 \cdot f = f$ and $(a \cdot b) \cdot f = a \cdot (b \cdot f)$.

Let $M$ be a type that carries a physical dimension. For any non-negative real number $a \in \mathbb{R}_{\ge 0}$, any dimensionful quantity $f \in \text{Dimensionful } M$ (represented as a function from unit choices to $M$), and any specific choice of units $u \in \text{UnitChoices}$, the value of the scaled dimensionful quantity $a \cdot f$ at $u$ is equal to the scalar $a$ acting on the value of $f$ at $u$: $$(a \cdot f)(u) = a \cdot f(u)$$ where the multiplication on the right-hand side is the action of $\mathbb{R}_{\ge 0}$ on the type $M$.

Let $M$ be a type that carries a physical dimension $d = \text{dim} M$. Given a specific system of units $u \in \text{UnitChoices}$, there exists an equivalence (bijection) $M \simeq \text{Dimensionful } M$ between the type $M$ and the type of functions that scale correctly under a change of units. An element $m \in M$ corresponds to the dimensionful quantity $f: \text{UnitChoices} \to M$ defined by: $$f(u') = \text{dimScale}(u, u', d) \cdot m$$ where $\text{dimScale}(u, u', d)$ is the scaling factor for dimension $d$ when transitioning from unit system $u$ to $u'$. Conversely, a dimensionful quantity $f$ is mapped to the value it takes in the unit system $u$, given by $f(u)$.

Let $M$ be a type that carries a physical dimension $d = \text{dim } M$. For any two systems of unit choices $u_1, u_2 \in \text{UnitChoices}$ and any value $m \in M$, let $f$ be the dimensionful quantity (an element of the type **Dimensionful $M$**) that corresponds to $m$ in the unit system $u_1$. The value of $f$ when evaluated at the unit system $u_2$ is given by: $$f(u_2) = \text{dimScale}(u_1, u_2, d) \cdot m$$ where $\text{dimScale}(u_1, u_2, d) \in \mathbb{R}_{\ge 0}$ is the scaling factor associated with dimension $d$ for the transition from unit system $u_1$ to $u_2$, and the multiplication denotes the action of non-negative reals on $M$.