PhyslibAlpha.AlgebraicFramework.CStarAlgebra.JordanSpecial

A JB-algebra $E$ is said to be **special** if there exists a $C^*$-algebra $A$ in the same universe such that $E$ embeds as a closed Jordan subalgebra into the self-adjoint part of $A$. This embedding (represented by the existence of an `IsSpecialWitness`) is a unital, Jordan-multiplicative linear isometry with a closed range.

Let $E$ be a JB-algebra and $A$ be a $C^*$-algebra. Let $j: E \to \text{selfAdjoint}(A)$ be a witness to the specialness of $E$ (a unital, Jordan-multiplicative linear isometry). If $x \in E$ is a non-negative element ($0 \le x$), then its image under $j$ is non-negative in the self-adjoint part of $A$ ($0 \le j(x)$).

Let $E$ be a JB-algebra and $A$ be a $C^*$-algebra. Suppose $j$ is a "special witness" embedding from $E$ into the self-adjoint part of $A$ (denoted $\text{selfAdjoint } A$), which is a unital, Jordan-multiplicative linear isometry. Then the map $j$ is monotone: for any $x, y \in E$, if $x \le y$, then $j(x) \le j(y)$ holds in the self-adjoint part of $A$.

Let $A$ be a unital $C^*$-algebra. The identity map on the space of self-adjoint elements, denoted $\text{selfAdjoint } A$, serves as a witness to the fact that $\text{selfAdjoint } A$ is a special JB-algebra. This witness is a linear isometry that preserves the unit element and the Jordan product, and its range is closed.

Let $A$ be a unital $C^*$-algebra. The space of self-adjoint elements of $A$, denoted by $\text{selfAdjoint}(A)$, is a special JB-algebra. (A JB-algebra is called **special** if it embeds as a norm-closed unital Jordan subalgebra into the self-adjoint part of some $C^*$-algebra.)