Physlib.Units.Exponent

The definition provides a `DecidableEq` instance for the `Exponent` type, which represents the rational exponents used in dimensional analysis. This signifies that for any two dimension exponents $x, y \in \text{Exponent}$, there exists an algorithmic procedure to determine whether $x = y$ or $x \neq y$.

The definition provides a `Repr` instance for the `Exponent` type, which is used for displaying dimension exponents. It specifies that the string representation of an `Exponent` value $x$ is obtained by applying the standard rational number representation to its underlying rational value $x.\text{toRat} \in \mathbb{Q}$.

This definition establishes a canonical equivalence (bijection) between the type `Exponent`, which represents the rational exponents used in dimensional analysis, and the set of rational numbers $\mathbb{Q}$. The equivalence is formed by the mapping of an `Exponent` to its underlying rational value and the corresponding inverse mapping.

The function maps a rational number $q \in \mathbb{Q}$ to its representation as a dimension exponent of type `Exponent`. This type is a wrapper around the rational numbers used to ensure that arithmetic on physical dimensions is computationally reducible.

For any rational number $q \in \mathbb{Q}$, converting $q$ to a dimension exponent (using the function `ofRat`) and then extracting the underlying rational value (using the function `toRat`) returns the original value $q$. That is, $\text{toRat}(\text{ofRat}(q)) = q$.

The function `gcdAux` takes three natural numbers as arguments: a "fuel" parameter $f$, and two integers $m$ and $n$. It implements a fuel-bounded version of the Euclidean algorithm to compute the greatest common divisor (GCD) of $m$ and $n$. Specifically: - If the fuel $f$ is 0, it returns $n$. - If the fuel is $f + 1$: - If $m = 0$, it returns $n$. - Otherwise, it recursively calls itself with fuel $f$, the new first integer as $n \pmod m$, and the new second integer as $m$. This auxiliary function is used to ensure that the normalization of rational exponents in dimensional analysis is computationally reducible within Lean's kernel.

The function $\text{gcd}(m, n)$ computes the greatest common divisor of two natural numbers $m$ and $n$. It is implemented using a fuel-bounded Euclidean algorithm (calling `gcdAux` with a fuel parameter of $m + 1$) to ensure the calculation is computationally reducible within Lean's kernel, which facilitates the normalization of rational dimension exponents.

For any natural numbers $m$ and $n$, the greatest common divisor $\gcd(m, n)$ calculated using the specific implementation for dimension exponents (`Dimension.Exponent.gcd`) is equal to the standard greatest common divisor for natural numbers (`Nat.gcd`).

The function `Dimension.Exponent.normalize` takes an integer numerator $n \in \mathbb{Z}$, a natural number denominator $d \in \mathbb{N}$, and a proof that $d \neq 0$. It returns a dimension exponent (of type `Exponent`) representing the rational number $n/d$ in its reduced form. This is achieved by dividing both $n$ and $d$ by their greatest common divisor $\text{gcd}(|n|, d)$, utilizing a computationally reducible algorithm to facilitate definitional equality in dimensional analysis.

For any integer $n \in \mathbb{Z}$ and any natural number $d \in \mathbb{N}$ such that $d \neq 0$, the rational value of the dimension exponent obtained via `Dimension.Exponent.normalize` is equal to the standard rational number obtained via `Rat.normalize`. That is, $(\text{normalize}(n, d)).\text{toRat} = \text{Rat.normalize}(n, d)$.

The function maps a dimension exponent $x$ to the normalized numerator $n \in \mathbb{Z}$ of its underlying rational value.

For a dimension exponent $x$, the function returns its normalized denominator $d \in \mathbb{N}$ such that $x$ represents a rational number $q = \frac{n}{d}$ in reduced form.

For two dimension exponents $a$ and $b$, represented as rational numbers $\frac{n_a}{d_a}$ and $\frac{n_b}{d_b}$ respectively, their sum is defined as the normalized dimension exponent corresponding to the rational number $\frac{n_a d_b + n_b d_a}{d_a d_b}$. This addition is implemented using a reducible algorithm to ensure that concrete calculations can be evaluated by definitional equality.

This definition provides the addition operation for the `Exponent` type, allowing the use of the symbol $+$ to represent the sum of two dimension exponents $a$ and $b$. The operation $a + b$ is defined by the `Dimension.Exponent.add` function, which performs rational addition in a way that ensures concrete calculations are reducible to definitional equality.

For any dimension exponents $a$ and $b$, let $\text{equivRat}$ denote the canonical equivalence between the type of dimension exponents and the rational numbers $\mathbb{Q}$. The rational number corresponding to the sum of $a$ and $b$ is equal to the sum of the rational numbers corresponding to $a$ and $b$ individually, satisfying the relation $\text{equivRat}(a + b) = \text{equivRat}(a) + \text{equivRat}(b)$.

For two dimension exponents $a$ and $b$, which are represented as rational numbers, their difference $a - b$ is defined as the sum of $a$ and the negation of $b$. This subtraction is implemented using a reducible algorithm to ensure that concrete calculations can be evaluated by definitional equality.

This definition provides the subtraction operator $-$ for the type `Exponent`, which represents dimension exponents. It allows for the notation $a - b$ for two dimension exponents $a$ and $b$, utilizing the underlying reducible subtraction function `sub` specifically defined for this type.

For any dimension exponents $a$ and $b$, the rational number associated with their difference $a - b$ is equal to the difference of the rational numbers associated with $a$ and $b$. That is, $\text{equivRat}(a - b) = \text{equivRat}(a) - \text{equivRat}(b)$, where $\text{equivRat}$ is the canonical equivalence mapping between the type of dimension exponents and the rational numbers $\mathbb{Q}$.

The function computes the product of two dimension exponents $a$ and $b$. Given $a$ with numerator $n_a \in \mathbb{Z}$ and denominator $d_a \in \mathbb{N}$, and $b$ with numerator $n_b \in \mathbb{Z}$ and denominator $d_b \in \mathbb{N}$, the function returns the normalized dimension exponent representing the rational number $\frac{n_a \cdot n_b}{d_a \cdot d_b}$. This multiplication is implemented to be computationally reducible to support definitional equality in dimensional analysis.

This instance defines the multiplication operation for dimension exponents. For any two exponents $a, b \in \text{Exponent}$, their product is denoted by $a \cdot b$. This operation is implemented using a reducible form of rational multiplication to facilitate definitional equality in dimensional analysis calculations.

Let $a$ and $b$ be dimension exponents, and let $\text{equivRat} : \text{Exponent} \simeq \mathbb{Q}$ be the canonical equivalence between the type of dimension exponents and the rational numbers. Then the rational value of the product of $a$ and $b$ is equal to the product of their individual rational values: $$\text{equivRat}(a \cdot b) = \text{equivRat}(a) \cdot \text{equivRat}(b)$$ where the multiplication on the left is the specific multiplication defined for dimension exponents and the multiplication on the right is the standard multiplication in $\mathbb{Q}$.

The function computes the multiplicative inverse $a^{-1}$ of a dimension exponent $a$. If $a$ represents a non-zero rational number $q$, the function returns the exponent corresponding to $1/q$. If $a = 0$, the inverse is defined to be $0$.

This definition provides the multiplicative inverse operation for dimension exponents. For any dimension exponent $a$, its inverse $a^{-1}$ is determined by the inverse of its underlying rational value, where the inverse of $0$ is defined to be $0$.

For any dimension exponent $a$, let $\text{equivRat} : \text{Exponent} \to \mathbb{Q}$ be the equivalence mapping between dimension exponents and rational numbers. The rational number corresponding to the multiplicative inverse of $a$ is equal to the multiplicative inverse of the rational number corresponding to $a$, i.e., $$\text{equivRat}(\text{inv } a) = (\text{equivRat } a)^{-1}$$ where $\text{inv}$ denotes the inverse operation on $\text{Exponent}$ and $^{-1}$ denotes the standard inverse on $\mathbb{Q}$.

The function computes the division of two dimension exponents $a$ and $b$, defined as the product $a \cdot b^{-1}$ of $a$ and the multiplicative inverse of $b$.

This instance provides the division operator $a / b$ for dimension exponents $a, b \in \text{Exponent}$.

For any two dimension exponents $a, b \in \text{Exponent}$, let $\text{equivRat}$ denote the canonical equivalence between the type `Exponent` (a wrapper for rational numbers used in dimensional analysis) and the rational numbers $\mathbb{Q}$. The division operation in `Exponent` is preserved under this equivalence, such that: $$\text{equivRat}(a / b) = \text{equivRat}(a) / \text{equivRat}(b)$$ where the division on the left is performed in `Exponent` and the division on the right is performed in $\mathbb{Q}$.

This definition establishes that the type `Exponent`, which represents dimension exponents, forms a field. The field structure is inherited from the rational numbers $\mathbb{Q}$ through the canonical equivalence $\text{equivRat} : \text{Exponent} \simeq \mathbb{Q}$. It ensures that the specific arithmetic operations—addition, subtraction, multiplication, inversion, and division—defined for `Exponent` satisfy the axioms of a field.

This definition establishes a ring isomorphism between the type of dimension exponents, $\text{Exponent}$, and the rational numbers, $\mathbb{Q}$. This isomorphism, denoted as $\text{Exponent} \simeq+* \mathbb{Q}$, maps a dimension exponent to its underlying rational value while preserving the operations of addition and multiplication.

This instance defines a canonical coercion from the type `Exponent` to the set of rational numbers $\mathbb{Q}$, which allows a dimension exponent to be regarded as a rational number.

Let $\text{Exponent}$ be a type representing dimension exponents, which is a wrapper around the rational numbers $\mathbb{Q}$. For any two exponents $a, b \in \text{Exponent}$, their coerced rational values in $\mathbb{Q}$ are equal if and only if $a$ and $b$ are equal.

The zero element of the type $\text{Exponent}$, which represents dimension exponents, is equal to the rational number $0$ when coerced to $\mathbb{Q}$.

The coercion of the dimension exponent $1$ to a rational number is equal to the rational number $1$.

For any natural number $n \ge 2$, the coercion of $n$ (when treated as a dimension exponent) to the rational numbers $\mathbb{Q}$ is equal to the natural number $n$ as a rational number.

For any two dimension exponents $a$ and $b$, the coercion of their sum $a + b$ to a rational number is equal to the sum of their individual rational coercions.

For any two dimension exponents $a$ and $b$, the coercion of their difference $a - b$ to a rational number is equal to the subtraction of their values as rational numbers in $\mathbb{Q}$.

For any dimension exponent $a$, the coercion of its negation $-a$ to a rational number is equal to the negation of the rational number corresponding to $a$, expressed as $(-a : \mathbb{Q}) = -(a : \mathbb{Q})$.

For any two dimension exponents $a$ and $b$, the rational number obtained by coercing their product $a \cdot b$ is equal to the product of their values when viewed as rational numbers in $\mathbb{Q}$.

For any dimension exponent $a$, the rational number corresponding to the inverse $a^{-1}$ is equal to the multiplicative inverse of the rational number corresponding to $a$, written as $(a^{-1} : \mathbb{Q}) = (a : \mathbb{Q})^{-1}$.

For any dimension exponents $a$ and $b$, the rational number corresponding to their quotient $a / b$ is equal to the quotient of the rational numbers corresponding to $a$ and $b$, written as $(a / b : \mathbb{Q}) = (a : \mathbb{Q}) / (b : \mathbb{Q})$.

This definition equips the type `Exponent`, which represents the rational exponents used in dimensional analysis, with a linear order structure. This order is induced by the standard linear order on the rational numbers $\mathbb{Q}$ via the canonical equivalence $\text{Exponent} \simeq \mathbb{Q}$, meaning that for any $a, b \in \text{Exponent}$, $a \leq b$ holds if and only if their corresponding rational values satisfy the relation in $\mathbb{Q}$.

Let $a$ and $b$ be elements of the type `Exponent`, which represents rational exponents used in dimensional analysis. The inequality $a \leq b$ holds in the `Exponent` type if and only if their corresponding rational values in $\mathbb{Q}$ satisfy the inequality $(a : \mathbb{Q}) \leq (b : \mathbb{Q})$.

For any two dimension exponents $a, b \in \text{Exponent}$, the strict inequality $a < b$ holds if and only if their corresponding rational values in $\mathbb{Q}$ satisfy $(a : \mathbb{Q}) < (b : \mathbb{Q})$.

The type `Exponent`, which represents dimension exponents as a wrapper around the rational numbers $\mathbb{Q}$, forms a strictly ordered ring. This means that the ring operations are compatible with the linear order; specifically, for any $a, b, c \in \text{Exponent}$, if $a < b$ then $a + c < b + c$, and if $0 < a$ and $0 < b$ then $0 < a \cdot b$.

The type `Exponent`, which represents dimension exponents, has characteristic zero. This means that the canonical ring homomorphism from the natural numbers $\mathbb{N}$ to `Exponent` is injective; in other words, for any natural number $n$, the sum of $n$ copies of the multiplicative identity $1$ in `Exponent` is zero if and only if $n = 0$.

The custom addition operation `add` defined for the `Exponent` type is equal to the addition operation provided by the field instance on `Exponent`.

The custom subtraction operation $\text{sub}$ defined for the type of dimension exponents $\text{Exponent}$ is equal to the subtraction operation provided by the field instance structure $\text{instField}$ of $\text{Exponent}$.

For the type `Exponent` representing dimension exponents, the specifically defined multiplicative inverse function `inv` is equal to the inverse operation provided by its `Field` instance.

On the type of dimension exponents $\text{Exponent}$, the custom multiplication operation $\text{mul}$ is equal to the multiplication operation provided by the field structure instance $\text{instField}$ on $\text{Exponent}$.

The custom division operation on the type $\text{Exponent}$ (dimension exponents), denoted as $\text{div}$, is equal to the division operation provided by the field structure ($\text{instField}$) of the $\text{Exponent}$ type.

Let $\text{Length} = (1, 0)$ and $\text{Time} = (0, 1)$ be elements of the product space $\text{Exponent} \times \text{Exponent}$, where $\text{Exponent}$ represents dimension exponents (rationals with reducible arithmetic). If we define $\text{Speed} = \text{Length} - \text{Time}$, then the following equality holds: $\text{Length} = \text{Time} + \text{Speed}$.

For the type `Exponent`, which represents dimension exponents as rational numbers, the following arithmetic equality holds: $$\left( \frac{2}{3} + \frac{5}{7} \right) \cdot \left( \frac{11}{13} - \frac{1}{2} \right) = \frac{87}{182}$$

In the type `Exponent`, which represents rational numbers used for physical dimension exponents, the following arithmetic identity holds: $(-3/4)^{-1} + 5/6 = -1/2$.