PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Compatibility

Jordan-intrinsic compatibility of observables

i. Overview

The physical notion of two observables being "compatible" (jointly measurable, simultaneously sharp) should not need the C⋆-commutator to state — that commutator does not exist at the bare Jordan level, and defining compatibility via it would put the cart before the horse (compatibility is exactly the *classical*, commuting fragment of the theory, the fragment that should not need the full C⋆ apparatus to talk about). The standard Jordan-algebraic substitute is **operator commutativity**: `a` and `b` are Jordan-compatible when their multiplication operators commute, `L_a ∘ L_b = L_b ∘ L_a`.

`CStarAlgebra/JordanCompatibility.lean` shows this is no idle abstraction: for `a`, `b` self-adjoint elements of a C⋆-algebra that already commute in the ordinary associative sense (`ab = ba`), `L_a` and `L_b` commute as Jordan operators too — so every associatively-compatible pair of observables is automatically Jordan-compatible, recovering the expected physics. The converse (Jordan compatibility implies associative commutativity) is *not* claimed here; it is a separate, harder question left open.

A genuinely stronger notion — that `a` and `b` *jointly generate an associative Jordan subalgebra*, giving a two-observable joint functional calculus — needs a two-generator analogue of `Power/GeneratedByOne.lean` and, in turn, a two-variable strengthening of `Power/Associative.lean`'s open power-associativity theorem. `FreeJordanTwo.lean`/ `FreeSpecialTwo.lean` lay the groundwork (the abstract and concrete special free Jordan algebras on two generators), but the two hard theorems connecting them — Shirshov (the abstract algebra embeds specially) and Cohn (every quotient of a special algebra stays special) — are real, disconnected future work, not attempted here.

ii. Key definitions and results

`IsJordanOrderUnit.IsJordanCompatible`
`IsJordanOrderUnit.isJordanCompatible_comm`, `.isJordanCompatible_one_left/right`

iii. Table of contents

A. The compatibility predicate

A. The compatibility predicate

6 declarations

definition

$a$ and $b$ are Jordan-compatible

#IsJordanCompatible

Two elements $a$ and $b$ of a Jordan algebra $E$ are Jordan-compatible if their left multiplication operators $L_a$ and $L_b$ commute, such that $L_a \circ L_b = L_b \circ L_a$ . Here, $L_x$ denotes the operator defined by $L_x(y) = x \circ y$ , where $\circ$ is the Jordan product.

theorem

$a$ is Jordan-compatible with $a$

#isJordanCompatible_self

In a Jordan algebra $E$ , every element $a \in E$ is Jordan-compatible with itself. This means that the left multiplication operator $L_a$ (defined by $L_a(x) = a \circ x$ , where $\circ$ is the Jordan product) commutes with itself, i.e., $L_a \circ L_a = L_a \circ L_a$ .

theorem

Jordan compatibility is symmetric

#isJordanCompatible_comm

Let $E$ be a Jordan algebra. For any elements $a, b \in E$ , if $a$ and $b$ are Jordan-compatible, then $b$ and $a$ are also Jordan-compatible. Here, $a$ and $b$ are Jordan-compatible if their left multiplication operators $L_a$ and $L_b$ commute ( $L_a \circ L_b = L_b \circ L_a$ ), where $L_x(y) = x \circ y$ is the Jordan product.

theorem

The multiplication operator $L_1$ is the identity map $\text{id}_E$

#mulLeft_one_eq_id

In a Jordan algebra $E$ over the real numbers $\mathbb{R}$ with identity element $1$ , the linear operator $L_1$ representing left-multiplication by $1$ is equal to the identity operator $\text{id}_E$ .

theorem

$1$ is Jordan-compatible with any $a$

#isJordanCompatible_one_left

In a Jordan algebra $E$ with identity element $1$ , the identity element is Jordan-compatible with any element $a \in E$ . This means that their left multiplication operators $L_1$ and $L_a$ commute, such that $L_1 \circ L_a = L_a \circ L_1$ . Since $L_1$ is the identity operator on $E$ , this condition is satisfied for all $a$ .

theorem

$a$ is Jordan-compatible with $1$

#isJordanCompatible_one_right

For any element $a$ in a Jordan algebra $E$ with identity element $1$ , the element $a$ is Jordan-compatible with $1$ .

PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.Compatibility

Jordan-intrinsic compatibility of observables

i. Overview

ii. Key definitions and results

iii. Table of contents

A. The compatibility predicate

aaa and bbb are Jordan-compatible

aaa is Jordan-compatible with aaa

Jordan compatibility is symmetric

The multiplication operator L1L_1L1​ is the identity map idE\text{id}_EidE​

111 is Jordan-compatible with any aaa

aaa is Jordan-compatible with 111

$a$ and $b$ are Jordan-compatible

$a$ is Jordan-compatible with $a$

The multiplication operator $L_1$ is the identity map $\text{id}_E$

$1$ is Jordan-compatible with any $a$

$a$ is Jordan-compatible with $1$