PhyslibAlpha.AlgebraicFramework.CStarAlgebra.JordanPositivity

Jordan positivity and decomposition in a Cstar algebra

i. Overview

The exact cone theorem `a ≥ 0 ⟺ ∃ b, a = b²` and the decomposition `a = a₊ - a₋` with `a₊ ∘ a₋ = 0` are already available for the canonical realization: `CStarAlgebra/JordanDecomposition.lean` has `Observable.nonneg_iff_exists_observable_sq`, `Observable.posPart`/`Observable.negPart`, `Observable.posPart_sub_negPart`, and `Observable.posPart_mul_negPart`/`.negPart_mul_posPart` — using the *ordinary* associative square and product, since it predates the Jordan layer. This file is the two-line connection to the Jordan-native statements, using `mul_self_eq` from `CStarAlgebra/Jordan.lean` (the Jordan square of a single element is the ordinary square) and ordinary two-sided vanishing to obtain Jordan orthogonality.

Square roots, `|a|`, and the CFC-based characterization `a ≥ 0 ⟺ σ(a) ⊆ [0,∞)` are not duplicated here: their abstract versions already live on the single-observable JB functional calculus path, `JordanOrderUnit/JB/GeneratedByOne/CFC.lean` (`jordanAbs`, `jordanPosPart`/`jordanNegPart`, `jordanCfc_nonneg_iff`), which applies uniformly to this realization's `selfAdjoint A` once it is known to be a `JBAlgebra` — no realization-specific restatement is needed.

ii. Key definitions and results

`JB.nonneg_iff_exists_jpow_two`
`JB.jordanOrthogonal_posPart_negPart`

iii. Table of contents

A. Positivity via the Jordan square
B. Orthogonality of the Jordan decomposition

A. Positivity via the Jordan square

B. Orthogonality of the Jordan decomposition

5 declarations

theorem

Positivity of self-adjoint elements via Jordan squares ( $a \ge 0 \iff \exists b, a = b^2$ )

#nonneg_iff_exists_jpow_two

Let $a$ be a self-adjoint element (also called an observable) of a $C^*$ -algebra $A$ . Then $a$ is non-negative ( $a \ge 0$ ) if and only if there exists a self-adjoint element $b \in A$ such that $a$ is the Jordan square of $b$ , denoted as $a = b^{[2]}$ .

theorem

$b \geq 0 \implies U_a(b) \geq 0$ for self-adjoint elements in a $C^*$ -algebra

#quadRep_nonneg

Let $A$ be a $C^*$ -algebra and let $a, b \in A$ be self-adjoint elements. If $b$ is non-negative ( $b \geq 0$ ), then the quadratic representation of $a$ acting on $b$ , defined as $U_a(b) = aba$ , is also non-negative ( $U_a(b) \geq 0$ ).

instance

Quadratic Positivity of Self-Adjoint Elements in a $C^*$ -algebra

#instIsQuadraticallyPositiveSubtypeMemAddSubgroupSelfAdjoint

Let $A$ be a $C^*$ -algebra. The space of self-adjoint elements (observables) of $A$ , denoted by $\text{selfAdjoint}(A)$ , is quadratically positive. This implies that for any self-adjoint element $a \in \text{selfAdjoint}(A)$ , the quadratic representation operator $U_a$ maps the cone of non-negative elements to itself; specifically, if $b \ge 0$ is a self-adjoint element, then $U_a(b) \ge 0$ . In the context of a $C^*$ -algebra, this corresponds to the property that if $b \ge 0$ , then $aba \ge 0$ for any self-adjoint $a$ .

definition

Conditioned state $\omega|_p$ for a projection $p$ in a $C^*$ -algebra

#conditionCStar

Let $A$ be a $C^*$ -algebra and let $\text{selfAdjoint}(A)$ be the Jordan algebra of its self-adjoint elements. Given a Jordan projection $p \in \text{selfAdjoint}(A)$ (satisfying $p \circ p = p$ ) and a state $\omega \in \mathcal{S}(\mathbb{R}, \text{selfAdjoint}(A))$ such that $\omega(p) > 0$ , the conditioned state $\omega|_p$ is defined as the map: $x \mapsto \frac{\omega(p x p)}{\omega(p)}$ where $p x p$ corresponds to the quadratic representation $U_p(x)$ in the $C^*$ -algebraic setting. This definition specializes the general Jordan algebraic conditioning to $C^*$ -algebras, automatically satisfying the required quadratic positivity conditions.

theorem

The positive and negative parts of an observable are Jordan-orthogonal ( $a^+ \circ a^- = 0$ )

#jordanOrthogonal_posPart_negPart

Let $A$ be a $C^*$ -algebra. For any self-adjoint element $a \in A$ (an observable), let $a^+$ and $a^-$ denote its positive and negative parts, respectively. Then $a^+$ and $a^-$ are Jordan-orthogonal, meaning their Jordan product vanishes: $a^+ \circ a^- = 0$ .

PhyslibAlpha.AlgebraicFramework.CStarAlgebra.JordanPositivity

Jordan positivity and decomposition in a Cstar algebra

i. Overview

ii. Key definitions and results

iii. Table of contents

A. Positivity via the Jordan square

B. Orthogonality of the Jordan decomposition

Positivity of self-adjoint elements via Jordan squares (a≥0 ⟺ ∃b,a=b2a \ge 0 \iff \exists b, a = b^2a≥0⟺∃b,a=b2)

b≥0 ⟹ Ua(b)≥0b \geq 0 \implies U_a(b) \geq 0b≥0⟹Ua​(b)≥0 for self-adjoint elements in a C∗C^*C∗-algebra

Quadratic Positivity of Self-Adjoint Elements in a C∗C^*C∗-algebra

Conditioned state ω∣p\omega|_pω∣p​ for a projection ppp in a C∗C^*C∗-algebra

The positive and negative parts of an observable are Jordan-orthogonal (a+∘a−=0a^+ \circ a^- = 0a+∘a−=0)

Positivity of self-adjoint elements via Jordan squares ( $a \ge 0 \iff \exists b, a = b^2$ )

$b \geq 0 \implies U_a(b) \geq 0$ for self-adjoint elements in a $C^*$ -algebra

Quadratic Positivity of Self-Adjoint Elements in a $C^*$ -algebra

Conditioned state $\omega|_p$ for a projection $p$ in a $C^*$ -algebra

The positive and negative parts of an observable are Jordan-orthogonal ( $a^+ \circ a^- = 0$ )