PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Basic

Jordan order-unit spaces

i. Overview

This is the next rung above `OrderUnit`, per the architecture

`AOU → JordanOrderUnit → JB → JBW (later)`.

An order-unit space only remembers `≤` and `1`. Quantum observables carry one more piece of structure that is *not* the full associative operator product (which loses self-adjointness for non-commuting `a`, `b`): the Jordan product `a ∘ b`, a commutative, generally non-associative multiplication satisfying the weak-associativity Jordan identity. This file adds the minimal compatibility condition: every square is a possible outcome, `0 ≤ a ∘ a`. In the operator picture `a ∘ a = a²`, and `⟨ψ, a²ψ⟩ = ‖aψ‖² ≥ 0` is the reason variances are never negative. Identifying *every* positive element with a square is deliberately not assumed here; that is a stronger spectral theorem of the JB layer.

We do not redefine Jordan algebras: `IsCommJordan` and the surrounding non-unital, non-associative commutative ring axioms are exactly mathlib's `Mathlib.Algebra.Jordan.Basic`, together with the real-linearity hypotheses (`Module ℝ E`, `SMulCommClass`, `IsScalarTower`) that its own module docstring already names as the standard setting for a *real* Jordan algebra. This file only adds this one order-compatibility axiom.

ii. Key definitions and results

`IsJordanOrderUnit E`
`IsJordanOrderUnit.mul_one`
`IsJordanOrderUnit.mul_self_nonneg`

iii. Table of contents

A. The compatibility class
B. Consequences

A. The compatibility class

B. Consequences

1 declaration

theorem

Squares are non-negative in Jordan order-unit spaces ( $0 \le a^2$ )

#sq_nonneg

In a Jordan order-unit space $E$ , for any element $a \in E$ , the Jordan square of $a$ is non-negative, i.e., $0 \le a \circ a$ . This represents the physical requirement that every Jordan square corresponds to a possible measurement outcome (a non-negative variance).