PhyslibAlpha.AlgebraicFramework.OrderUnit.Basic

Let $E$ be an ordered additive commutative monoid. An element $u \in E$ is an order unit element if $0 \le u$ and for every $x \in E$, there exists a natural number $n \in \mathbb{N}$ such that $x \le n \cdot u$.

Let $E$ be a partially ordered real vector space (formally, an additive commutative group that is a module over $\mathbb{R}$ equipped with a partial order $\le$). An element $u \in E$ is an **Archimedean order unit element** if it satisfies the following two conditions: 1. $u$ is an order unit element, meaning $u \ge 0$ and for every $x \in E$, there exists a natural number $n \in \mathbb{N}$ such that $x \le n \cdot u$. 2. For any $x \in E$, if $x \le \epsilon \cdot u$ for all real $\epsilon > 0$, then $x \le 0$.

Let $E$ be an ordered additive commutative monoid with a distinguished unit element $1$. If $E$ satisfies the property of being an order-unit space (expressed by the `IsOrderUnit` typeclass), then the element $1$ is an order unit element. This means that $0 \le 1$ and for every element $x \in E$, there exists a natural number $n \in \mathbb{N}$ such that $x \le n \cdot 1$.

Let $E$ be a partially ordered real vector space (specifically, an additive commutative group that is a module over $\mathbb{R}$ equipped with a partial order $\le$) with a distinguished element $1$. If $E$ satisfies the property of being an Archimedean order-unit space (expressed by the `IsArchimedeanOrderUnit` typeclass), then the element $1$ is an Archimedean order unit element. This means that $1$ satisfies the following conditions: 1. $1 \ge 0$, and for every $x \in E$, there exists a natural number $n \in \mathbb{N}$ such that $x \le n \cdot 1$. 2. For any $x \in E$, if $x \le \epsilon \cdot 1$ for all real $\epsilon > 0$, then $x \le 0$.

Let $E$ be an ordered additive commutative group. If $u \in E$ is an order unit element (meaning $0 \le u$ and for every $x \in E$ there exists a natural number $n$ such that $x \le n \cdot u$), then every element $x \in E$ can be expressed as the difference $x = x_p - x_n$ of two non-negative elements $x_p, x_n \in E$ (where $0 \le x_p$ and $0 \le x_n$).

In an order-unit space $E$, every element $x \in E$ can be expressed as the difference of two non-negative elements. That is, for any $x \in E$, there exist $x_p, x_n \in E$ such that $0 \le x_p$, $0 \le x_n$, and $x = x_p - x_n$. This property demonstrates that the positive cone of an order-unit space is reproducing.

Given a type $E$ equipped with an additive commutative monoid structure and a partial order, the positive cone $\text{PosCone}(E)$ is defined as the set of all elements $x \in E$ such that $0 \le x$. In the context of quantum measurement, this represents the collection of all possible non-negative measurement outcomes or expectation values.

Given an ordered additive commutative monoid $E$, the positive cone $\text{PosCone}(E) = \{x \in E \mid 0 \le x\}$ forms an additive commutative monoid under the addition and zero element inherited from $E$. This is possible because the sum of any two non-negative elements $x, y$ satisfies $0 \le x + y$, and the zero element satisfies $0 \le 0$.

Given a real vector space $E$ equipped with a partial order, the positive cone $\text{PosCone}(E) = \{x \in E \mid 0 \le x\}$ is a module over the semiring of non-negative real numbers $\mathbb{R}_{\ge 0}$. For any scalar $c \in \mathbb{R}_{\ge 0}$ and element $x \in \text{PosCone}(E)$, the scalar multiplication $c \cdot x$ is inherited from the action of $\mathbb{R}$ on $E$, and the result remains within the positive cone.

Let $E$ be an ordered real vector space and $\text{PosCone}(E) = \{x \in E \mid 0 \le x\}$ be its positive cone. For any non-negative real number $c \in \mathbb{R}_{\ge 0}$ and any element $x \in \text{PosCone}(E)$, the scalar multiplication $c \cdot x$ defined on the positive cone is equal to the scalar multiplication $(c : \mathbb{R}) \cdot (x : E)$ performed in the underlying vector space $E$.

Let $E$ be an ordered real vector space and $\text{PosCone}(E) = \{x \in E \mid 0 \le x\}$ be its positive cone. For any non-negative real scalar $c \in \mathbb{R}_{\ge 0}$ and any element $x \in E$ such that $0 \le x$, the scalar multiplication of $c$ and $x$ within the positive cone is equal to the scalar multiplication $(c : \mathbb{R}) \cdot x$ performed in the underlying space $E$, which is guaranteed to be non-negative.