Physlib.Units.LTMCTDimensionBase

The type `LTMCTDimensionBase` is an inductive type representing the five base physical dimensions used as the default basis in PhysLib: length ($L$), time ($T$), mass ($M$), charge ($C$), and temperature ($\Theta$). This basis is specifically constructed to be charge-based rather than current-based, distinguishing it from the standard SI/ISQ base-quantity set.

For any two base dimensions $d_1, d_2$ in the set $\{L, T, M, C, \Theta\}$ represented by the type `LTMCTDimensionBase`, it is algorithmically decidable whether $d_1 = d_2$. This set comprises the five base physical dimensions: length ($L$), time ($T$), mass ($M$), charge ($C$), and temperature ($\Theta$).

The type `LTMCTDimensionBase`, which represents the set of five base physical dimensions—length ($L$), time ($T$), mass ($M$), charge ($C$), and temperature ($\Theta$)—is a finite type.

The function maps a physical dimension to the rational number $q \in \mathbb{Q}$ representing its exponent of the base dimension of length.

The function maps a physical dimension to a rational number $\mathbb{Q}$ representing the exponent of the base dimension of time within that dimension.

Given a physical dimension $D$, the function returns the rational number $q \in \mathbb{Q}$ representing the exponent of the mass base dimension in the dimensional representation of $D$.

Given a physical dimension $D$, this function returns the rational number $q \in \mathbb{Q}$ representing the exponent of the charge component in the dimensional representation of $D$.

The function maps a physical dimension $D$ to the rational number representing the exponent of thermodynamic temperature (often denoted by the symbol $\Theta$) in its decomposition into base dimensions.

Given five rational numbers $l, t, m, c, \theta \in \mathbb{Q}$, this function constructs a physical dimension $D$ in the $LTMCT$ basis (representing length, time, mass, charge, and temperature) such that the exponents of its base components are respectively $l, t, m, c,$ and $\theta$. Symbolically, this represents the dimension $L^l T^t M^m C^c \Theta^\theta$.

For any rational numbers $l, t, m, c, \theta \in \mathbb{Q}$, the length exponent of the physical dimension constructed from these exponents (representing length, time, mass, charge, and temperature respectively) is equal to $l$. Symbolically, $(\text{ofLTMCTDimensionBase}(l, t, m, c, \theta)).\text{length} = l$.

For any rational numbers $l, t, m, c, \theta \in \mathbb{Q}$, the time exponent of the physical dimension $L^l T^t M^m C^c \Theta^\theta$ (constructed via `ofLTMCTDimensionBase`) is equal to $t$.

For any rational numbers $l, t, m, c, \theta \in \mathbb{Q}$, the mass exponent of the physical dimension constructed with exponents $l, t, m, c, \theta$ (representing the dimension $L^l T^t M^m C^c \Theta^\theta$) is equal to $m$.

For any rational numbers $l, t, m, c, \theta \in \mathbb{Q}$, the charge exponent of the physical dimension constructed with these five values as the exponents for length, time, mass, charge, and temperature respectively, is equal to $c$.

For any rational numbers $l, t, m, c,$ and $\theta$, the temperature exponent of the physical dimension $D = L^l T^t M^m C^c \Theta^\theta$ (constructed via the $LTMCT$ basis) is equal to $\theta$.

For any physical dimension $d$ represented in the $LTMCT$ basis (comprising length, time, mass, charge, and temperature), the temperature component of its exponent vector is equal to its temperature projection $d.\text{temperature}$.

The physical dimension of length $L_{\mathfrak{d}}$ is equal to the single basis vector corresponding to the base dimension of length, denoted as $\text{single}(\text{length})$. This represents a dimension vector where the exponent for length is $1$ and all other base dimensions (time, mass, charge, and temperature) have an exponent of $0$.

The time dimension $T_d$ is equal to the basis vector $\text{single}(\text{time})$. Here, $\text{single}(\text{time})$ represents the dimension vector where the exponent for the time dimension is $1$ and the exponents for all other base dimensions (length, mass, charge, and temperature) are $0$.

In the LTMCT (Length, Time, Mass, Charge, Temperature) dimension basis, the named mass dimension generator $\mathsf{M}_d$ is equal to the base vector corresponding to the mass dimension (the vector where the exponent of mass is 1 and all other exponents are 0).

The physical dimension of electric charge, denoted as $C𝓭$, is equal to the basis vector in the $LTMCT$ (length, time, mass, charge, temperature) system that has a unit exponent for the charge dimension and zero for all other base dimensions.

In the $LTMCT$ dimension system, the base dimension for thermodynamic temperature, denoted as $\Theta_d$, is equal to the basis vector created by the `single` function for the temperature component (representing a dimension vector where the temperature exponent is 1 and all other exponents—length, time, mass, and charge—are 0).