PhyslibAlpha.ProbabilisticTheory.Examples.Square

The `squareSubmodule` is the $\mathbb{R}$-linear subspace of $\mathbb{R}^4$ (represented as functions $v: \{0, 1, 2, 3\} \to \mathbb{R}$) consisting of vectors whose components satisfy the diagonal relation $v_0 + v_3 = v_1 + v_2$. This subspace represents the observables of a square state space, where the values at the four vertices are constrained by the equality of the sums of opposite vertices.

The type `Square` represents the space of observables on a square state space. It is defined as the $\mathbb{R}$-linear subspace of functions $v: \{0, 1, 2, 3\} \to \mathbb{R}$ (elements of $\mathbb{R}^4$) that satisfy the diagonal relation $v_0 + v_3 = v_1 + v_2$. These functions correspond to affine functions on the square, uniquely determined by their values at the four vertices.

The space `Square`, consisting of observables $v: \{0, 1, 2, 3\} \to \mathbb{R}$ that satisfy the diagonal relation $v_0 + v_3 = v_1 + v_2$, forms an additive commutative group.

The type `Square`, representing the space of observables on a square state space satisfying the diagonal relation $v_0 + v_3 = v_1 + v_2$, carries the structure of a module (vector space) over the real numbers $\mathbb{R}$.

For an observable $q$ in the space `Square` and a vertex index $i \in \{0, 1, 2, 3\}$, this function returns the value of the observable at the $i$-th vertex. The space `Square` is the $\mathbb{R}$-linear subspace of functions $v: \{0, 1, 2, 3\} \to \mathbb{R}$ that satisfy the diagonal relation $v_0 + v_3 = v_1 + v_2$.

Given a function $v: \{0, 1, 2, 3\} \to \mathbb{R}$ that satisfies the diagonal relation $v_0 + v_3 = v_1 + v_2$, this definition constructs the unique observable in the space $\text{Square}$ whose values at the vertices are given by $v$.

For any function $v: \{0, 1, 2, 3\} \to \mathbb{R}$ satisfying the diagonal relation $v_0 + v_3 = v_1 + v_2$, let $q$ be the observable in the space $\text{Square}$ constructed from $v$. Then for any index $i \in \{0, 1, 2, 3\}$, the value of the observable $q$ at the $i$-th vertex is equal to $v_i$.

Let $q$ and $r$ be observables in the space $\text{Square}$. If $q.\text{val}(i) = r.\text{val}(i)$ for all vertex indices $i \in \{0, 1, 2, 3\}$, then $q = r$. Here, $\text{Square}$ is the space of affine functions on a square determined by their values at four vertices satisfying the diagonal relation $v_0 + v_3 = v_1 + v_2$, and $q.\text{val}(i)$ denotes the value of the observable at the $i$-th vertex.

For any observable $q$ in the space `Square`, the values $q(i)$ at the four vertices $i \in \{0, 1, 2, 3\}$ satisfy the diagonal relation: $$q(0) + q(3) = q(1) + q(2).$$ This relation characterizes the affine functions on a square state space, where the vertices $0$ and $3$ are opposite to each other, as are the vertices $1$ and $2$.

For any observables $q$ and $r$ in the space `Square` (the space of affine functions on a square determined by their values at the vertices $\{0, 1, 2, 3\}$ satisfying $v_0 + v_3 = v_1 + v_2$) and for any vertex index $i \in \{0, 1, 2, 3\}$, the value of the sum of the observables at vertex $i$ is equal to the sum of their individual values at that vertex: $(q + r).val(i) = q.val(i) + r.val(i)$.

For any real number $c \in \mathbb{R}$, any observable $q$ in the space $\text{Square}$ (the space of affine functions on a square satisfying the diagonal relation $v_0 + v_3 = v_1 + v_2$), and any vertex index $i \in \{0, 1, 2, 3\}$, the value of the scalar product $c \cdot q$ at vertex $i$ is equal to $c$ multiplied by the value of $q$ at vertex $i$: $$(c \cdot q).\text{val}(i) = c \cdot q.\text{val}(i).$$

For any vertex $i \in \{0, 1, 2, 3\}$, the value of the zero observable $0$ in the space `Square` at vertex $i$ is $0$.

The space of square observables $\text{Square}$ is equipped with a partial order. For any two observables $q, r \in \text{Square}$, the relation $q \le r$ holds if and only if the value of $q$ is less than or equal to the value of $r$ at each vertex $i \in \{0, 1, 2, 3\}$, i.e., $q.\text{val } i \le r.\text{val } i$ for all $i$.

Let $\text{Square}$ be the space of observables on a square, where each observable $q \in \text{Square}$ is characterized by its values $q(i)$ at the vertices $i \in \{0, 1, 2, 3\}$ satisfying the diagonal relation $q(0) + q(3) = q(1) + q(2)$. For any two observables $q, r \in \text{Square}$, the relation $q \le r$ holds if and only if $q(i) \le r(i)$ for all $i \in \{0, 1, 2, 3\}$.

The space of square observables $\text{Square}$ forms an ordered additive monoid. This means that the partial order on $\text{Square}$ is compatible with addition: for any observables $q, r, s \in \text{Square}$, if $q \le r$, then $q + s \le r + s$. The addition and the partial order are defined pointwise at the four vertices $\{0, 1, 2, 3\}$.

In the space of square observables $\text{Square}$, scalar multiplication by non-negative real numbers preserves the partial order. Specifically, for any real number $c \ge 0$ and any observables $q, r \in \text{Square}$, if $q \le r$, then $c \cdot q \le c \cdot r$. Here, the space $\text{Square}$ consists of functions $v: \{0, 1, 2, 3\} \to \mathbb{R}$ satisfying $v_0 + v_3 = v_1 + v_2$, and the order $q \le r$ is defined pointwise as $q(i) \le r(i)$ for all $i \in \{0, 1, 2, 3\}$.

The unit $1$ in the space of observables $\text{Square}$ is defined as the unique observable whose value at each of the four vertices $\{0, 1, 2, 3\}$ is equal to $1$. This constant function satisfies the diagonal relation $1 + 1 = 1 + 1$.

For any vertex $i \in \{0, 1, 2, 3\}$, the value of the unit observable $1$ in the space $\text{Square}$ at that vertex is $1$.

The space of square observables $\text{Square}$, consisting of functions $v: \{0, 1, 2, 3\} \to \mathbb{R}$ satisfying the diagonal relation $v_0 + v_3 = v_1 + v_2$, is an order-unit space. The constant function $1$ (mapping each vertex to $1$) serves as the order unit. This implies that $1$ is non-negative ($1 \ge 0$) and that for any observable $q \in \text{Square}$, there exists a natural number $n$ such that $q \le n \cdot 1$ holds under the pointwise partial order on the vertices.

The space of square observables $\text{Square}$ is an Archimedean order-unit space. In this space, the order unit $1$ is the constant function mapping each vertex to $1$. The Archimedean property ensures that for any observable $q \in \text{Square}$, if $q \le \epsilon \cdot 1$ for all real $\epsilon > 0$, then $q \le 0$ under the pointwise partial order on the vertices.

For a vertex index $i \in \{0, 1, 2, 3\}$, the function $\text{ev}_i: \text{Square} \to \mathbb{R}$ is the positive linear map that sends an observable $q$ to its value at the $i$-th vertex, $q.\text{val}(i)$. This map corresponds to a pure state of the square state space.

For any vertex index $i \in \{0, 1, 2, 3\}$ and any observable $q \in \text{Square}$, the evaluation map $\text{ev}_i$ applied to $q$ yields the value of $q$ at the $i$-th vertex, i.e., $\text{ev}_i(q) = q.\text{val}(i)$.

The function $\text{facet}: \{0, 1, 2, 3\} \to \text{Square}$ defines four specific observables on the square state space, where each $\text{facet}(j)$ is an affine function determined by its values at the four vertices. Specifically: - $\text{facet}(0)$ has vertex values $(0, 1, 0, 1)$ and vanishes on vertices $0$ and $2$. - $\text{facet}(1)$ has vertex values $(0, 0, 1, 1)$ and vanishes on vertices $0$ and $1$. - $\text{facet}(2)$ has vertex values $(1, 0, 1, 0)$ and vanishes on vertices $1$ and $3$. - $\text{facet}(3)$ has vertex values $(1, 1, 0, 0)$ and vanishes on vertices $2$ and $3$.

For any index $j \in \{0, 1, 2, 3\}$, the facet observable $\text{facet}(j)$ of the square state space is non-negative, meaning $0 \le \text{facet}(j)$. According to the partial order on the space of square observables, this implies that the value of $\text{facet}(j)$ at each vertex $i \in \{0, 1, 2, 3\}$ is greater than or equal to zero.

For any collection of observables $q_j \in \text{Square}$ indexed by $j \in \{0, 1, 2, 3\}$ and any vertex $i \in \{0, 1, 2, 3\}$, the value of the sum of the observables at vertex $i$ is equal to the sum of the individual values of each observable at that vertex. That is, $$\left( \sum_{j=0}^3 q_j \right)(i) = \sum_{j=0}^3 q_j(i)$$ where $q(i)$ denotes the value of the observable $q$ at the $i$-th vertex of the square.

Let $q$ be an observable on the square state space, which is characterized by its values at the four vertices $\{0, 1, 2, 3\}$ satisfying the diagonal relation $q(0) + q(3) = q(1) + q(2)$. If $q$ is non-negative (meaning $q(i) \ge 0$ for all $i \in \{0, 1, 2, 3\}$), then there exist non-negative real coefficients $c_j \ge 0$ for $j \in \{0, 1, 2, 3\}$ such that $q$ can be expressed as a linear combination of the four facet observables $\text{facet}_j$: $$q = \sum_{j=0}^3 c_j \cdot \text{facet}_j$$

The linear map $\text{vals} : E \otimes_{\mathbb{R}} \text{Square} \to (\{0, 1, 2, 3\} \to E)$ associates an observable $z$ in the composite system $E \otimes_{\mathbb{R}} \text{Square}$ with its values at the four vertices of the square. For a basic tensor $x \otimes q$, the value at vertex $i \in \{0, 1, 2, 3\}$ is $q(i) \cdot x$, where $q(i)$ is the value of the square observable $q$ at that vertex. The resulting values in $E$ satisfy the diagonal relation $\text{vals}(z)_0 + \text{vals}(z)_3 = \text{vals}(z)_1 + \text{vals}(z)_2$.

Let $E$ be a real vector space. For any element $x \in E$ and any observable $q \in \text{Square}$, the vertex values of the elementary tensor $x \otimes q$ at each vertex $i \in \{0, 1, 2, 3\}$ are given by the scalar multiplication of $x$ by the value of $q$ at that vertex: $$\text{vals}(x \otimes q)_i = q(i) \cdot x$$

Let $E$ be a real vector space. For any composite observable $z \in E \otimes_{\mathbb{R}} \text{Square}$, let $\text{vals}(z)_i \in E$ denote the value of the observable at the $i$-th vertex for $i \in \{0, 1, 2, 3\}$. These vertex values satisfy the diagonal relation: $$\text{vals}(z)_0 + \text{vals}(z)_3 = \text{vals}(z)_1 + \text{vals}(z)_2$$

Given a real vector space $E$ and a function $A: \{0, 1, 2, 3\} \to E$ representing values at the vertices of a square, this definition constructs a composite observable in the tensor product $E \otimes_{\mathbb{R}} \text{Square}$. The construction is defined as: $$A_0 \otimes 1 + (A_1 - A_0) \otimes \text{facet}_0 + (A_2 - A_0) \otimes \text{facet}_1$$ where $1$ is the identity observable and $\text{facet}_0, \text{facet}_1$ are specific facet observables of the square. Because observables of the square must satisfy the diagonal relation $v_0 + v_3 = v_1 + v_2$, the resulting composite observable is uniquely determined by the values at vertices $0, 1,$ and $2$, while the value $A_3$ provided in the input is ignored.

Let $E$ be a real vector space. For any two functions $A, B: \{0, 1, 2, 3\} \to E$ that assign values to the vertices of a square, the mapping `ofVals` (which constructs a composite observable in $E \otimes_{\mathbb{R}} \text{Square}$) is additive, such that $\text{ofVals}(A + B) = \text{ofVals}(A) + \text{ofVals}(B)$.

Let $E$ be a real vector space and $z \in E \otimes_{\mathbb{R}} \text{Square}$ be a composite observable. Mapping $z$ to its values at the four vertices of the square and then reconstructing an observable from these values using $\text{ofVals}$ recovers the original observable $z$. That is, $$\text{ofVals}(\text{vals}(z)) = z$$

Let $E$ be a real vector space and let $A: \{0, 1, 2, 3\} \to E$ be a function assigning values to the four vertices of a square. If the values $A_i$ satisfy the diagonal relation $A_0 + A_3 = A_1 + A_2$, then extracting the vertex values from the composite observable constructed from $A$ yields the original values. That is, $\text{vals}(\text{ofVals}(A)) = A$.

Let $E$ be a real vector space and $\text{Square}$ be the space of observables on a square state space, represented by the $\mathbb{R}$-linear subspace of functions $v: \{0, 1, 2, 3\} \to \mathbb{R}$ satisfying the diagonal relation $v_0 + v_3 = v_1 + v_2$. The linear map $\text{vals} : E \otimes_{\mathbb{R}} \text{Square} \to E^4$, which assigns to each composite observable its values at the four vertices of the square, is injective.

Let $E$ be an order-unit space and let $\text{Square}$ be the space of observables on a square (affine functions determined by values at vertices $i \in \{0, 1, 2, 3\}$ satisfying the diagonal relation). For any positive linear functional $\phi: E \to \mathbb{R}$ and any composite observable $z \in E \otimes_{\mathbb{R}} \text{Square}$, the value of the sliced observable $\text{lslice}(\phi, z) \in \text{Square}$ at vertex $i$ is equal to the functional $\phi$ applied to the $i$-th vertex value of $z$. That is, $$(\text{lslice}(\phi, z))_i = \phi(\text{vals}(z)_i)$$ where $\text{vals}(z)_i \in E$ denotes the value of the tensor $z$ at the $i$-th vertex.

Let $E$ be an ordered real vector space and $\text{Square}$ be the space of observables on a square (functions $v: \{0, 1, 2, 3\} \to \mathbb{R}$ satisfying $v_0 + v_3 = v_1 + v_2$). For any composite observable $z \in E \otimes_{\mathbb{R}} \text{Square}$, if the values at each vertex $i \in \{0, 1, 2, 3\}$ are non-negative, i.e., $\text{vals}(z)_i \ge 0$ for all $i$, then $z$ belongs to the maximal tensor cone $\text{maxTensorCone}(E, \text{Square})$.

Let $E$ be an Archimedean order-unit space. For any element $z$ in the composite system $E \otimes_{\mathbb{R}} \text{Square}$, $z$ belongs to the maximal tensor cone of $E \otimes_{\mathbb{R}} \text{Square}$ if and only if all its vertex values $\text{vals}(z)_i$ (for $i \in \{0, 1, 2, 3\}$) are non-negative in $E$.