Physlib.SpaceAndTime.Time.Basic

The function $\text{val}$, which assigns a numerical value to an element of type `Time`, is injective. That is, for any two time points $t_1, t_2 \in \text{Time}$, if $\text{val}(t_1) = \text{val}(t_2)$, then $t_1 = t_2$.

The type `Time` admits a canonical coercion from the natural numbers. For any natural number $n \in \mathbb{N}$, it can be interpreted as an element of `Time` representing $n$ units of time relative to the chosen origin and orientation.

The type `Time` allows for the interpretation of natural number literals $n \in \mathbb{N}$ as elements of `Time`. This interpretation is based on a fixed choice of a zero point (origin) and a fixed unit of duration (defining the value $1$).

For any natural number $n \in \mathbb{N}$, the numerical value $\text{val}(n)$ of $n$ when interpreted as an element of the type $\text{Time}$ is equal to $n$.

The natural number $0$, when interpreted as an element of the type $\text{Time}$ via the canonical coercion, is equal to the zero element $0$ of $\text{Time}$.

The natural number $1$, when interpreted as an element of the type $\text{Time}$ via the canonical coercion, is equal to the element $1$ of $\text{Time}$.

For any natural number $n \in \mathbb{N}$, let $n$ be interpreted as an element of the type $\text{Time}$ (using the natural number literal coercion). The numerical value associated with this element, denoted by the function $\text{val}$, is equal to $n$.

In the type $\text{Time}$, which represents time with a fixed choice of units and origin, the element $1$ is not equal to the element $0$.

The numerical value associated with the zero element (the origin) of the type `Time` is equal to $0$. That is, $\text{val}(0) = 0$.

The numerical value of the constant $1$ in the type $\text{Time}$ is equal to $1$. Specifically, $\text{val}(1) = 1$, where $\text{val}$ is the function that returns the numerical representation of a $\text{Time}$ element.

This definition provides a coercion from the real numbers $\mathbb{R}$ to the type `Time`. It allows any real number $r \in \mathbb{R}$ to be treated as an instance of `Time`, where the numerical value representing the time is set to $r$.

This definition provides a coercion from the type `Time` to the real numbers $\mathbb{R}$. It allows any instance of `Time` to be treated as a real number by extracting its underlying numerical value.

For any real number $r \in \mathbb{R}$, the underlying numerical value of $r$ when cast into the type `Time` is equal to $r$.

For any natural number $n \in \mathbb{N}$, the value obtained by first casting $n$ to a real number $\mathbb{R}$ and then to the type `Time` is equal to the value obtained by casting $n$ directly to `Time`.

The type $\text{Time}$ is inhabited, meaning it has a designated default element. This default element is defined to be $0$.

The default value of the type `Time` is equal to $0$.

The type `Time` is equipped with a less-than-or-equal-to relation $\le$ that defines the orientation of time. For any two time points $t_1, t_2 \in \text{Time}$, the relation $t_1 \le t_2$ holds if and only if their underlying numerical values satisfy the inequality $t_1.\text{val} \le t_2.\text{val}$.

For any two time points $t_1, t_2 \in \text{Time}$, the relation $t_1 \le t_2$ holds if and only if their underlying numerical values satisfy the inequality $t_1.\text{val} \le t_2.\text{val}$.

The type $\text{Time}$ is equipped with a partial order structure. For any elements $t_1, t_2, t_3 \in \text{Time}$, the relation $\le$ (defined by the inequality of their underlying numerical values) satisfies the following properties: 1. **Reflexivity**: $t_1 \le t_1$. 2. **Transitivity**: If $t_1 \le t_2$ and $t_2 \le t_3$, then $t_1 \le t_3$. 3. **Antisymmetry**: If $t_1 \le t_2$ and $t_2 \le t_1$, then $t_1 = t_2$.

For any two time instances $t_1, t_2 \in \text{Time}$, the relation $t_1 < t_2$ holds if and only if their underlying numerical values satisfy the inequality $t_1.\text{val} < t_2.\text{val}$.

The addition operation on the type `Time` is defined by summing the underlying numerical values of two time instances. For any $t_1, t_2 \in \text{Time}$, their sum $t_1 + t_2$ is the element of `Time` whose value is the sum of the values of $t_1$ and $t_2$, such that $(t_1 + t_2).\text{val} = t_1.\text{val} + t_2.\text{val}$.

For any two time instances $t_1, t_2$ of type `Time`, the underlying numerical value of their sum is equal to the sum of their individual numerical values: $(t_1 + t_2).\text{val} = t_1.\text{val} + t_2.\text{val}$.

The negation operation on the type `Time` is defined by negating the underlying numerical value of a time $t$. Specifically, for any $t \in \text{Time}$, its negation $-t$ is the element of `Time` whose value is the negative of the value of $t$ (i.e., $(-t).\text{val} = -t.\text{val}$).

For any time instance $t$ of type `Time`, the underlying numerical value of its negation $-t$ is equal to the negative of the numerical value of $t$. That is, $(-t).\text{val} = -t.\text{val}$.

For any two elements $t_1, t_2$ of the type $\text{Time}$, the subtraction $t_1 - t_2$ is defined as the element of $\text{Time}$ whose underlying numerical value is the difference between the value of $t_1$ and the value of $t_2$ (i.e., $(t_1 - t_2).\text{val} = t_1.\text{val} - t_2.\text{val}$).

For any two time instances $t_1, t_2 \in \text{Time}$, the underlying numerical value of their difference $t_1 - t_2$ is equal to the difference between the numerical value of $t_1$ and the numerical value of $t_2$. That is, $(t_1 - t_2).\text{val} = t_1.\text{val} - t_2.\text{val}$.

For any real number $k \in \mathbb{R}$ and any element $t$ of the type $\text{Time}$, the scalar multiplication $k \cdot t$ is defined by multiplying the underlying real-valued magnitude of $t$ (denoted $t.\text{val}$) by $k$.

In the context of the $\text{Time}$ type, which represents time with a fixed choice of units and origin, for any real number $k \in \mathbb{R}$ and any $t \in \text{Time}$, the underlying numerical value of the scalar product $k \cdot t$ is equal to the product of $k$ and the underlying value of $t$. That is, $(k \cdot t).\text{val} = k \cdot t.\text{val}$.

The type $\text{Time}$, representing time with a fixed choice of units and origin, is endowed with the structure of an additive group. Under this structure, addition is associative, i.e., $(t_1 + t_2) + t_3 = t_1 + (t_2 + t_3)$ for all $t_1, t_2, t_3 \in \text{Time}$. The element $0$ (origin) serves as the additive identity such that $0 + t = t$ and $t + 0 = t$, and every time $t$ has an additive inverse $-t$ satisfying $-t + t = 0$. These properties are derived from the arithmetic of the underlying numerical values representing the time instances.

The type $\text{Time}$, which represents time with a fixed choice of units and origin, is endowed with the structure of an additive commutative group (Abelian group). This structure implies that, in addition to the properties of an additive group (associativity, identity, and inverses), addition is commutative: $t_1 + t_2 = t_2 + t_1$ for all $t_1, t_2 \in \text{Time}$. These properties are inherited from the arithmetic of the underlying numerical values representing the time instances.

The type $\text{Time}$ is endowed with the structure of a module over the real numbers $\mathbb{R}$. This confirms that $\text{Time}$ functions as a one-dimensional real vector space, where scalar multiplication $k \cdot t$ for $k \in \mathbb{R}$ and $t \in \text{Time}$ satisfies the standard axioms: $1 \cdot t = t$, $a(b \cdot t) = (ab) \cdot t$, and distributivity over both scalar and time addition.

The norm on the space $\text{Time}$ is defined such that for any element $t \in \text{Time}$, its norm $\|t\|$ is equal to the absolute value (norm) of its underlying real-valued representation $t.\text{val}$.

For any element $t$ in the space $\text{Time}$, the norm $\|t\|$ is equal to the norm (absolute value) of its underlying real-valued representation $\|t.\text{val}\|$.

The type $\text{Time}$ is equipped with a metric space structure where the distance function $d(t_1, t_2)$ between two time points $t_1, t_2 \in \text{Time}$ is defined as the norm of their difference, $\|t_1 - t_2\|$.

For any two time points $t_1, t_2$ in the space $\text{Time}$, the distance $\text{dist}(t_1, t_2)$ between them is equal to the norm of the difference of their underlying real-valued representations, $\|t_1.\text{val} - t_2.\text{val}\|$.

For any two time points $t_1, t_2 \in \text{Time}$, the distance $d(t_1, t_2)$ between them is equal to the standard Euclidean distance $d(t_1.\text{val}, t_2.\text{val})$ between their underlying real-valued representations.

The type $\text{Time}$ is equipped with the structure of a seminormed additive commutative group. This means that $\text{Time}$ satisfies the axioms of an abelian group under addition and is endowed with a seminorm $\|\cdot\|$ such that the distance between any two time points $t_1, t_2 \in \text{Time}$ is given by $\text{dist}(t_1, t_2) = \|t_1 - t_2\|$. These properties, including the triangle inequality and the symmetry of the distance function, are inherited from the underlying real-valued representation of the time instances.

The type $\text{Time}$ is equipped with the structure of a normed additive commutative group. This means that $\text{Time}$ satisfies the axioms of an abelian group under addition and is endowed with a norm $\|\cdot\|$ such that the distance between any two time points $t_1, t_2 \in \text{Time}$, defined as $d(t_1, t_2) = \|t_1 - t_2\|$, satisfies the identity of indiscernibles ($d(t_1, t_2) = 0 \implies t_1 = t_2$). These properties are inherited from the underlying real-valued representation of the time instances.

The type $\text{Time}$ is endowed with the structure of a normed space over the field of real numbers $\mathbb{R}$. This means that $\text{Time}$ is a real vector space equipped with a norm $\|\cdot\|$ such that for any scalar $k \in \mathbb{R}$ and any $t \in \text{Time}$, the property $\|k \cdot t\| = |k| \|t\|$ is satisfied. This structure ensures that the algebraic operations on $\text{Time}$ (addition and scalar multiplication) are compatible with the topology induced by its norm.

The type `Time` is equipped with an inner product structure over the real numbers $\mathbb{R}$. For any two time values $t_1, t_2 \in \text{Time}$, the inner product is defined as the product of their underlying real values: $$\langle t_1, t_2 \rangle_{\mathbb{R}} = t_1 \cdot t_2$$

For any two time values $t_1, t_2 \in \text{Time}$, their inner product over the real numbers $\mathbb{R}$ is equal to the product of their underlying numerical values. That is, $$\langle t_1, t_2 \rangle_{\mathbb{R}} = t_1.\text{val} \cdot t_2.\text{val}$$ where $t.\text{val}$ represents the real number associated with the time $t$ in a given system of units and origin.

The type $\text{Time}$ is endowed with the structure of an inner product space over the field of real numbers $\mathbb{R}$. This structure defines an inner product $\langle \cdot, \cdot \rangle_{\mathbb{R}}$ that is compatible with the norm on $\text{Time}$, such that for any $t \in \text{Time}$, the relation $\|t\|^2 = \langle t, t \rangle_{\mathbb{R}}$ holds. It further satisfies the standard axioms of a real inner product space, including linearity in the first argument and symmetry ($\langle t_1, t_2 \rangle_{\mathbb{R}} = \langle t_2, t_1 \rangle_{\mathbb{R}}$).

For any two time values $t_1, t_2 \in \text{Time}$, the equality $t_1 = t_2$ is decidable.

The type $\text{Time}$ is equipped with a measurable space structure. This structure is defined by the Borel $\sigma$-algebra $\mathcal{B}(\text{Time})$, which is the $\sigma$-algebra generated by the open sets of the topology on $\text{Time}$.

The type $\text{Time}$ is a Borel space, meaning that its measurable space structure is identical to the Borel $\sigma$-algebra $\mathcal{B}(\text{Time})$ generated by the open sets of the topology on $\text{Time}$.

The definition provides an orthonormal basis for the space $\text{Time}$ as a one-dimensional real inner product space. This basis is indexed by a single element (from the set $\{0\}$, represented by `Fin 1`) and is defined by the unit element $1 \in \text{Time}$.

For the unique index $i$ in the set $\{0\}$ (represented by `Fin 1`), the orthonormal basis element $\text{basis}_i$ of the space $\text{Time}$ is equal to $1$.

The dimension (rank) of the space $\text{Time}$ as a vector space over the real numbers $\mathbb{R}$ is 1.

The finite dimension of the space $\text{Time}$ as a vector space over the real numbers $\mathbb{R}$ is equal to $1$.

The space $\text{Time}$, representing time with a fixed choice of units and origin, is a finite-dimensional vector space over the real numbers $\mathbb{R}$.

The canonical volume measure on the space $\text{Time}$ is equal to the additive Haar measure normalized with respect to the standard orthonormal basis of $\text{Time}$.

The definition `Time.toRealCLM` is the continuous linear map from the space $\text{Time}$ to the real numbers $\mathbb{R}$. It associates each element $t \in \text{Time}$ with its corresponding real-valued representation $\text{val}(t)$. This map preserves the vector space structure (addition and scalar multiplication) and is continuous with respect to the standard topologies on $\text{Time}$ and $\mathbb{R}$.

The mapping is a continuous linear equivalence between the space $\text{Time}$ and the real numbers $\mathbb{R}$. This equivalence identifies a time instance $t \in \text{Time}$ with its underlying numerical value in $\mathbb{R}$ via the valuation function $t \mapsto \text{val}(t)$. As a continuous linear equivalence, the map preserves the additive and scalar multiplication structure of the 1-dimensional real vector space $\text{Time}$ and serves as a homeomorphism between $\text{Time}$ and $\mathbb{R}$.

The definition establishes a linear isometry equivalence between the space $\text{Time}$ and the real numbers $\mathbb{R}$. This mapping identifies a time instance $t \in \text{Time}$ with its numerical value in $\mathbb{R}$ via the valuation function $t \mapsto \text{val}(t)$. As a linear isometry, this equivalence preserves the vector space structure (addition and scalar multiplication) and the norm, such that the norm of a time $\|t\|$ is equal to the absolute value of its real-valued representation.

The valuation function $\text{val} : \text{Time} \to \mathbb{R}$, which assigns to each instance of time its corresponding numerical value in the real numbers, is a measurable function.

The valuation function $\text{val} : \text{Time} \to \mathbb{R}$, which assigns to each instance of time its corresponding numerical value in the real numbers, is a measurable embedding. This means that $\text{val}$ is an injective function such that a set $S \subseteq \text{Time}$ is measurable if and only if its image $\text{val}(S)$ is measurable in $\mathbb{R}$.

The valuation function $\text{val} : \text{Time} \to \mathbb{R}$, which identifies an element of the space $\text{Time}$ with its corresponding real number, is measure-preserving with respect to the canonical volume measures on $\text{Time}$ and $\mathbb{R}$. Specifically, for any measurable set $S \subseteq \mathbb{R}$, the volume of its preimage $\text{val}^{-1}(S)$ in $\text{Time}$ is equal to the Lebesgue measure (volume) of $S$ in $\mathbb{R}$.

The valuation function $\text{val} : \text{Time} \to \mathbb{R}$, which maps an element of the space $\text{Time}$ to its corresponding real-valued representation, is differentiable at all points with respect to the real numbers $\mathbb{R}$.

For any point $t$ in the space $\text{Time}$, the Fréchet derivative of the valuation function $\text{val}: \text{Time} \to \mathbb{R}$ at $t$, when applied to the unit vector $1 \in \text{Time}$, is equal to $1$.