Physlib.Units.UnitDependent

Let $M$ be a type whose elements depend on a choice of units (indicated by the `UnitDependent` typeclass). For any two unit choices $u_1, u_2 \in \text{UnitChoices}$ and any element $m \in M$, scaling $m$ from the representation of $u_1$ to $u_2$ and then scaling the result back from $u_2$ to $u_1$ returns the original element $m$. That is, $$\text{scaleUnit}(u_2, u_1, \text{scaleUnit}(u_1, u_2, m)) = m.$$

Let $M$ be a type whose elements depend on a choice of units (indicated by the `UnitDependent` typeclass). For any two unit choices $u_1, u_2 \in \text{UnitChoices}$ and any two elements $m_1, m_2 \in M$, the results of scaling $m_1$ and $m_2$ from the representation of $u_1$ to $u_2$ are equal if and only if $m_1$ and $m_2$ are equal. That is, $$\text{scaleUnit}(u_1, u_2, m_1) = \text{scaleUnit}(u_1, u_2, m_2) \iff m_1 = m_2.$$

For a type $M$ equipped with a `UnitDependent` instance and two unit choices $u_1, u_2 \in \text{UnitChoices}$, the function $\text{scaleUnit}(u_1, u_2, \cdot)$ defines an equivalence (a bijective map) from $M$ to itself. The forward map converts an element from the representation corresponding to unit choice $u_1$ to that of $u_2$, and its inverse is given by the scaling map from $u_2$ back to $u_1$.

For a real vector space $M$ that carries a linear unit dependency, and given two sets of unit choices $u_1, u_2 \in \text{UnitChoices}$, the function $\text{scaleUnit}(u_1, u_2): M \to M$ is defined as an $\mathbb{R}$-linear map. This map transforms an element $m \in M$ representing a physical quantity in the context of unit choice $u_1$ to its representation in unit choice $u_2$.

For a real vector space $M$ that carries a linear unit dependency, and given two sets of unit choices $u_1, u_2 \in \text{UnitChoices}$, the function $\text{scaleUnit}(u_1, u_2)$ is an $\mathbb{R}$-linear equivalence (a linear isomorphism) from $M$ to itself. This map transforms an element $m \in M$ from its representation under unit choice $u_1$ to its representation under unit choice $u_2$, with the inverse map being the scaling from $u_2$ back to $u_1$.

For a topological vector space $M$ over $\mathbb{R}$ that carries a continuous linear unit dependency, and given two sets of unit choices $u_1, u_2 \in \text{UnitChoices}$, the function $\text{scaleUnit}(u_1, u_2): M \to M$ is defined as a continuous $\mathbb{R}$-linear map. This map transforms an element $m \in M$ representing a physical quantity in the context of unit choice $u_1$ to its representation in unit choice $u_2$.

For a topological vector space $M$ over $\mathbb{R}$ that possesses a continuous linear unit dependency, and given two sets of unit choices $u_1, u_2 \in \text{UnitChoices}$, the function $\text{scaleUnit}(u_1, u_2)$ is a continuous $\mathbb{R}$-linear equivalence (a continuous linear isomorphism) from $M$ to itself. This map transforms an element $m \in M$ from its representation under unit choice $u_1$ to its representation under unit choice $u_2$, such that both the transformation and its inverse are continuous and linear.

Let $M$ be a topological vector space over $\mathbb{R}$ that possesses a continuous linear unit dependency. For any two sets of unit choices $u_1, u_2 \in \text{UnitChoices}$ and any element $m \in M$, the result of applying the continuous $\mathbb{R}$-linear equivalence $\text{scaleUnitContLinearEquiv}(u_1, u_2)$ to $m$ is equal to the scaling function $\text{scaleUnit}(u_1, u_2, m)$.

For a topological vector space $M$ over $\mathbb{R}$ that carries a continuous linear unit dependency, given any two sets of unit choices $u_1, u_2 \in \text{UnitChoices}$ and an element $m \in M$, the inverse of the continuous $\mathbb{R}$-linear equivalence $\text{scaleUnitContLinearEquiv}(u_1, u_2)$ applied to $m$ is equal to the scaling operation from $u_2$ to $u_1$ applied to $m$. That is, $$(\text{scaleUnitContLinearEquiv}(u_1, u_2))^{-1}(m) = \text{scaleUnit}(u_2, u_1, m)$$ where $\text{scaleUnitContLinearEquiv}(u_1, u_2)$ is the continuous linear isomorphism that transforms representations of elements in $M$ from the unit system $u_1$ to $u_2$.

The type `UnitChoices`, which represents a set of base units for physical dimensions (length, time, mass, charge, and temperature), is an instance of the `UnitDependent` type class. This is defined by a scaling function $\text{scaleUnit}(u_1, u_2, u)$ that transforms a set of units $u$ based on a change of reference units from $u_1$ to $u_2$. The transformation is performed by scaling each base unit in $u$ by the ratio of the corresponding units in $u_2$ and $u_1$: \[ \text{scaleUnit}(u_1, u_2, u) = \left( \frac{L_{u_2}}{L_{u_1}} L_u, \frac{T_{u_2}}{T_{u_1}} T_u, \frac{M_{u_2}}{M_{u_1}} M_u, \frac{Q_{u_2}}{Q_{u_1}} Q_u, \frac{\Theta_{u_2}}{\Theta_{u_1}} \Theta_u \right) \] where $L, T, M, Q,$ and $\Theta$ represent the length, time, mass, charge, and temperature components of the unit choices, respectively.

For any two sets of base units $u_1, u_2 \in \text{UnitChoices}$, scaling the unit choice $u_1$ based on a change of reference units from $u_1$ to $u_2$ results in $u_2$. That is, \[ \text{scaleUnit}(u_1, u_2, u_1) = u_2 \] where $\text{UnitChoices}$ represents a set of base units for physical dimensions (length, time, mass, charge, and temperature), and $\text{scaleUnit}(u_1, u_2, u)$ is the transformation of a unit choice $u$ under the reference change from $u_1$ to $u_2$.

For any physical dimension $d \in \text{Dimension}$ and any sets of base units $u, u_1, u_2 \in \text{UnitChoices}$, the scaling factor for dimension $d$ between $u$ and the transformed unit system $\text{scaleUnit}(u_1, u_2, u)$ is equal to the scaling factor for dimension $d$ between $u_1$ and $u_2$: \[ \text{dimScale}(u, \text{scaleUnit}(u_1, u_2, u), d) = \text{dimScale}(u_1, u_2, d) \] Here, $\text{dimScale}(u_A, u_B, d)$ is the factor used to convert a quantity of dimension $d$ from unit system $u_A$ to $u_B$, and $\text{scaleUnit}(u_1, u_2, u)$ scales the base units of $u$ by the ratios of the corresponding base units in $u_2$ to $u_1$.

Let $M$ be a type that carries a physical dimension $d = \text{dim} M$. Let $c$ be a dimensionful quantity of type $M$, which is a function $c: \text{UnitChoices} \to M$ that scales consistently with the dimension $d$. For any sets of unit choices $u, u_1, u_2 \in \text{UnitChoices}$, the value of $c$ evaluated at the scaled unit system $\text{scaleUnit}(u_1, u_2, u)$ satisfies: $$c(\text{scaleUnit}(u_1, u_2, u)) = \text{dimScale}(u_1, u_2, d) \cdot c(u)$$ where $\text{scaleUnit}(u_1, u_2, u)$ is the transformation of the unit choice $u$ by the ratios of base units in $u_2$ relative to $u_1$, and $\text{dimScale}(u_1, u_2, d)$ is the scaling factor for dimension $d$ transitioning from $u_1$ to $u_2$.

Let $M$ be a type that carries a physical dimension $d = \text{dim} M$. This instance provides a multiplicative unit-dependent structure (`MulUnitDependent`) for $M$. For any two unit systems $u_1, u_2 \in \text{UnitChoices}$, the scaling function $\text{scaleUnit}: \text{UnitChoices} \to \text{UnitChoices} \to M \to M$ is defined by: $$\text{scaleUnit}(u_1, u_2, m) = \text{dimScale}(u_1, u_2, d) \cdot m$$ where $m \in M$ and $\text{dimScale}(u_1, u_2, d)$ is the scaling factor for dimension $d$ when transitioning from unit choice $u_1$ to $u_2$. This definition ensures that scaling is consistent with the physical dimension of $M$ and satisfies required properties such as transitivity, identity, and commutation with multiplication.

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 element $m \in M$, the scaling of $m$ according to the change in units from $u_1$ to $u_2$ is given by: $$\text{scaleUnit}(u_1, u_2, m) = \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 for dimension $d$ when transitioning from unit system $u_1$ to $u_2$, and the multiplication denotes the action of non-negative reals on $M$.

Let $M$ be a real vector space (specifically, an additive commutative monoid and a module over $\mathbb{R}$) that carries a physical dimension $d = \text{dim} M$. This instance provides a linear unit-dependent structure (`LinearUnitDependent`) for $M$. For any two unit systems $u_1, u_2 \in \text{UnitChoices}$, the scaling function $\text{scaleUnit}(u_1, u_2): M \to M$ is linear, satisfying: 1. $\text{scaleUnit}(u_1, u_2, m_1 + m_2) = \text{scaleUnit}(u_1, u_2, m_1) + \text{scaleUnit}(u_1, u_2, m_2)$ 2. $\text{scaleUnit}(u_1, u_2, r \cdot m) = r \cdot \text{scaleUnit}(u_1, u_2, m)$ for all $m, m_1, m_2 \in M$ and $r \in \mathbb{R}$. This linearity holds because the scaling operation is defined by multiplication by the real-valued factor $\text{dimScale}(u_1, u_2, d)$ associated with the dimension of $M$.

Let $M$ be a topological real vector space (formally, an additive commutative monoid and a module over $\mathbb{R}$ equipped with a topology) such that scalar multiplication by constants is continuous. If $M$ carries a physical dimension $d = \text{dim } M$, then $M$ possesses a continuous linear unit-dependent structure (`ContinuousLinearUnitDependent`). For any two systems of unit choices $u_1, u_2 \in \text{UnitChoices}$, the scaling operation $\text{scaleUnit}(u_1, u_2) : M \to M$ is defined by: $$\text{scaleUnit}(u_1, u_2, m) = \text{dimScale}(u_1, u_2, d) \cdot m$$ where $\text{dimScale}(u_1, u_2, d) \in \mathbb{R}$ is the scaling factor associated with the dimension $d$. This map is linear and continuous because it is defined as the action of a constant scalar on $M$.

If a type $M_2$ is unit-dependent, then the type of functions $M_1 \to M_2$ is also unit-dependent for any type $M_1$. For a function $f: M_1 \to M_2$ and unit choices $u_1, u_2$, the scaling operation $\text{scaleUnit}(u_1, u_2)$ on the function $f$ is defined pointwise: $(\text{scaleUnit}(u_1, u_2)(f))(m) = \text{scaleUnit}(u_1, u_2)(f(m))$ for all $m \in M_1$.

Let $M_1$ be a type and $M_2$ be a unit-dependent type. For any two unit choices $u_1, u_2$, any function $f: M_1 \to M_2$, and any element $m_1 \in M_1$, the result of applying the scaled function $\text{scaleUnit}(u_1, u_2) f$ to $m_1$ is equal to scaling the value $f(m_1)$ by the same unit choices. That is, $$(\text{scaleUnit}(u_1, u_2) f)(m_1) = \text{scaleUnit}(u_1, u_2) (f(m_1)).$$ This confirms that the unit scaling for the function type $M_1 \to M_2$ is defined pointwise.

Suppose $M_1$ and $M_2$ are modules over $\mathbb{R}$. If $M_2$ carries a linear unit-dependent structure, then the space of $\mathbb{R}$-linear maps $M_1 \to_{\mathbb{R}} M_2$ is also linear unit-dependent. For a linear map $f: M_1 \to_{\mathbb{R}} M_2$ and two choices of units $u_1$ and $u_2$, the scaling operation $\text{scaleUnit}(u_1, u_2)$ on $f$ is defined pointwise: $(\text{scaleUnit}(u_1, u_2)f)(m) = \text{scaleUnit}(u_1, u_2)(f(m))$ for all $m \in M_1$.

Let $M_1$ and $M_2$ be topological vector spaces over $\mathbb{R}$ (where $M_2$ is a topological additive group with continuous scalar multiplication). If $M_2$ possesses a continuous linear unit-dependent structure, then the space of continuous $\mathbb{R}$-linear maps $M_1 \toL[\mathbb{R}] M_2$ is also a continuous linear unit-dependent type. For a continuous linear map $f: M_1 \toL[\mathbb{R}] M_2$ and any two unit choices $u_1, u_2 \in \text{UnitChoices}$, the scaling operation $\text{scaleUnit}(u_1, u_2)$ is defined by post-composing $f$ with the scaling map of the codomain. That is, $$(\text{scaleUnit}(u_1, u_2) f)(m) = \text{scaleUnit}(u_1, u_2) (f(m))$$ for all $m \in M_1$.

Given a unit-dependent type $M_1$ and any type $M_2$, the space of functions $M_1 \to M_2$ is unit-dependent. For a function $f: M_1 \to M_2$ and two choices of units $u_1$ and $u_2$, the scaled function is defined by applying $f$ to the input scaled in the reverse direction: $(\text{scaleUnit}(u_1, u_2, f))(m_1) = f(\text{scaleUnit}(u_2, u_1, m_1))$ for all $m_1 \in M_1$.

Let $M_1$ and $M_2$ be types, where $M_1$ is unit-dependent. For any two choices of units $u_1$ and $u_2$, any function $f: M_1 \to M_2$, and any element $m_1 \in M_1$, the evaluation of the unit-scaled function $\text{scaleUnit}(u_1, u_2, f)$ at the point $m_1$ is given by: $$(\text{scaleUnit}(u_1, u_2, f))(m_1) = f(\text{scaleUnit}(u_2, u_1, m_1))$$ where $\text{scaleUnit}(u_a, u_b, \cdot)$ denotes the transformation of an element from unit choice $u_a$ to unit choice $u_b$.

Given two unit-dependent types $M_1$ and $M_2$, the space of functions $M_1 \to M_2$ inherits a unit-dependent structure. For a function $f: M_1 \to M_2$ and two choices of units $u_1$ and $u_2$, the scaled function $\text{scaleUnit}(u_1, u_2, f)$ is defined by transforming the input from $u_2$ back to $u_1$, applying the function $f$, and then transforming the result from $u_1$ to $u_2$: $$(\text{scaleUnit}(u_1, u_2, f))(m_1) = \text{scaleUnit}(u_1, u_2, f(\text{scaleUnit}(u_2, u_1, m_1)))$$ for all $m_1 \in M_1$.

Let $M_1$ and $M_2$ be unit-dependent types, and let $u_1$ and $u_2$ be two choices of units. For any function $f: M_1 \to M_2$ and any element $m_1 \in M_1$, the evaluation of the unit-scaled function $\text{scaleUnit}(u_1, u_2, f)$ at $m_1$ is given by: $$(\text{scaleUnit}(u_1, u_2, f))(m_1) = \text{scaleUnit}(u_1, u_2, f(\text{scaleUnit}(u_2, u_1, m_1)))$$ where $\text{scaleUnit}(u_a, u_b, \cdot)$ denotes the transformation of an element from unit choice $u_a$ to unit choice $u_b$.

Given a unit-dependent type $M_1$ and a type $M_2$ that is multiplicatively unit-dependent (equipped with a scalar action by the non-negative real numbers $\mathbb{R}_{\ge 0}$), the space of functions $M_1 \to M_2$ inherits a multiplicatively unit-dependent structure. For a function $f: M_1 \to M_2$ and two unit choices $u_1, u_2$, the scaled function $\text{scaleUnit}(u_1, u_2, f)$ evaluated at an element $m_1 \in M_1$ is defined by: $$(\text{scaleUnit}(u_1, u_2, f))(m_1) = \text{scaleUnit}(u_1, u_2, f(\text{scaleUnit}(u_2, u_1, m_1)))$$ This definition ensures that the transformation of the function space correctly accounts for the unit scaling of both the domain and the codomain while remaining compatible with the scalar action of $\mathbb{R}_{\ge 0}$ on $M_2$.

For any two topological vector spaces $M_1$ and $M_2$ over $\mathbb{R}$ that possess continuous linear unit-dependent structures, the space of continuous linear maps $M_1 \to L[\mathbb{R}] M_2$ (the set of continuous $\mathbb{R}$-linear maps from $M_1$ to $M_2$) is also continuous linear unit-dependent. Given two unit choices $u_1, u_2 \in \text{UnitChoices}$, the transformation of a continuous linear map $f: M_1 \to L[\mathbb{R}] M_2$ is defined by: $$\text{scaleUnit}(u_1, u_2, f) = \mathcal{S}_{M_2}(u_1, u_2) \circ f \circ \mathcal{S}_{M_1}(u_2, u_1)$$ where $\mathcal{S}_{M_i}(u, u')$ represents the continuous linear equivalence on $M_i$ that scales an element from its representation in unit choice $u$ to its representation in unit choice $u'$. This construction ensures that the unit scaling is compatible with the linear and topological structures of the map space.

Let $M_1$ and $M_2$ be topological vector spaces over $\mathbb{R}$ equipped with continuous linear unit-dependent structures. For any continuous linear map $f: M_1 \to L[\mathbb{R}] M_2$, any two unit choices $u_1, u_2 \in \text{UnitChoices}$, and any element $m_1 \in M_1$, the application of the scaled function to $m_1$ satisfies: $$\text{scaleUnit}(u_1, u_2, f)(m_1) = \text{scaleUnit}(u_1, u_2, f(\text{scaleUnit}(u_2, u_1, m_1)))$$ Here, $\text{scaleUnit}(u, u', \cdot)$ denotes the transformation of an element or map from its representation in unit choice $u'$ to its representation in unit choice $u$.

For a type $M$ with a defined unit dependency, an element $m \in M$ is **dimensionally correct** if its value is invariant under a change of unit systems. Formally, for any two systems of units $u_1, u_2 \in \text{UnitChoices}$, the scaling function $\text{scaleUnit}$ must satisfy: \[ \text{scaleUnit}(u_1, u_2, m) = m \] This property indicates that the element $m$ (which could represent a value, a function, or a proposition) does not depend on the specific units chosen to represent it.

Let $M$ be a unit-dependent type and $m$ be an element of $M$. Then $m$ is **dimensionally correct** if and only if for all systems of units $u_1, u_2 \in \text{UnitChoices}$, the scaling function $\text{scaleUnit}$ leaves $m$ invariant: \[ \text{scaleUnit}(u_1, u_2, m) = m \] This means that an element is dimensionally correct precisely when its value does not depend on the specific choice of units used to represent it.

Let $M_1$ and $M_2$ be unit-dependent types. A function $f: M_1 \to M_2$ is **dimensionally correct** if and only if for all systems of units $u_1, u_2 \in \text{UnitChoices}$ and all $m \in M_1$, the following condition is satisfied: \[ \text{scaleUnit}(u_1, u_2, f(\text{scaleUnit}(u_2, u_1, m))) = f(m) \] This signifies that the function $f$ is dimensionally correct when its output, after scaling the input to a different unit system and then scaling the result back, remains identical to the original output.

Let $M_1$ be a unit-dependent type and $M_2$ be any type. A function $f: M_1 \to M_2$ is **dimensionally correct** if and only if for all unit systems $u_1, u_2 \in \text{UnitChoices}$ and all $m \in M_1$, the function satisfies: \[ f(\text{scaleUnit}(u_2, u_1, m)) = f(m) \] This property states that $f$ is dimensionally correct if its output remains invariant when its input is scaled according to a change in unit systems.

Let $M_1$ be a type and $M_2$ be a unit-dependent type. A function $f: M_1 \to M_2$ is **dimensionally correct** if and only if for all unit systems $u_1, u_2 \in \text{UnitChoices}$ and for all $m \in M_1$, the scaling operation satisfies: \[ \text{scaleUnit}(u_1, u_2, f(m)) = f(m) \] This means that a function into a unit-dependent type is dimensionally correct if and only if its output values $f(m)$ are themselves invariant under any change of unit systems.

Let $M_1, M_2$, and $M_3$ be types that carry physical dimensions, and let there be a dimensionful multiplication operation $* : M_1 \times M_2 \to M_3$. For any elements $m_1 \in M_1$ and $m_2 \in M_2$, and any two unit systems $u_1, u_2 \in \text{UnitChoices}$, the product of the elements scaled from $u_1$ to $u_2$ is equal to the scaling of their product: $$\text{scaleUnit}(u_1, u_2, m_1) * \text{scaleUnit}(u_1, u_2, m_2) = \text{scaleUnit}(u_1, u_2, m_1 * m_2)$$ where $\text{scaleUnit}(u_1, u_2, m)$ denotes the conversion of a quantity $m$ from unit system $u_1$ to $u_2$ according to its physical dimension.

Given a type $M$ equipped with a scalar action of the non-negative real numbers $\mathbb{R}_{\ge 0}$ and a unit-dependent structure, and a physical dimension $d \in \text{Dimension}$, the set $\text{DimSet}(M, d)$ is the collection of elements $m \in M$ that scale according to the dimension $d$ under a change of units. Specifically, an element $m$ belongs to this set if for any two unit systems $u_1, u_2 \in \text{UnitChoices}$, the scaling operation satisfies: $$\text{scaleUnit}(u_1, u_2, m) = \sigma(u_1, u_2, d) \cdot m$$ where $\sigma(u_1, u_2, d) \in \mathbb{R}_{\ge 0}$ is the scaling factor associated with the dimension $d$ when converting from unit choice $u_1$ to $u_2$.

Given a type $M$ equipped with a multiplicative action of non-negative real numbers $\mathbb{R}_{\ge 0}$ and a unit-dependent structure, the subset $\text{DimSet}(M, d)$ consisting of elements with physical dimension $d$ is also equipped with a multiplicative action of $\mathbb{R}_{\ge 0}$. Specifically, for any $\alpha \in \mathbb{R}_{\ge 0}$ and $m \in \text{DimSet}(M, d)$, the scalar product $\alpha \cdot m$ remains an element of $\text{DimSet}(M, d)$, as it scales correctly according to dimension $d$ under a change of units.

Let $M$ be a type equipped with a multiplicative action of the non-negative real numbers $\mathbb{R}_{\ge 0}$ and a unit-dependent structure. For any physical dimension $d \in \text{Dimension}$, the set $\text{DimSet}(M, d)$, which consists of elements $m \in M$ that scale according to $d$ under a change of units, is assigned the physical dimension $d$.

Let $M$ be a type equipped with a multiplicative action of the non-negative real numbers $\mathbb{R}_{\ge 0}$ and a unit-dependent structure. For any physical dimension $d \in \text{Dimension}$, let $\text{DimSet}(M, d)$ be the set of elements in $M$ that scale according to $d$ under a change of units. For any element $m \in \text{DimSet}(M, d)$ and any two unit systems $u_1, u_2 \in \text{UnitChoices}$, the underlying value in $M$ of the scaled element $\text{scaleUnit}(u_1, u_2, m)$ is equal to the scaling of the underlying value $m_{val}$ directly in $M$: $$(\text{scaleUnit}(u_1, u_2, m))_{val} = \text{scaleUnit}(u_1, u_2, m_{val})$$

Let $M$ be a type equipped with a scalar action of the non-negative real numbers $\mathbb{R}_{\ge 0}$ and a unit-dependent structure. For any physical dimension $d \in \text{Dimension}$ and any element $m \in M$, $m$ belongs to the set $\text{DimSet}(M, d)$ if and only if for all pairs of unit choices $u_1, u_2 \in \text{UnitChoices}$, the scaling operation satisfies: $$\text{scaleUnit}(u_1, u_2, m) = \sigma(u_1, u_2, d) \cdot m$$ where $\sigma(u_1, u_2, d)$ is the scaling factor for dimension $d$ between unit choices $u_1$ and $u_2$.