Classification of sequential products

The statement

On the real Hermitian matrices of size N ≥ 1, a sequential product satisfying S1–S7 agrees with the Lüders formula on effects. On the complex Hermitian matrices of size N ≥ 3, it has the twist form for a unique real parameter t. The complex conclusion holds for every pair of effects, including singular ones.

Real: a & b = √a · b · √a.

Complex: a & b = a¹ᐟ²⁺ⁱᵗ · b · a¹ᐟ²⁻ⁱᵗ.

An effect is a Hermitian matrix in the Loewner interval 0 ≤ a ≤ 1. The complex powers are defined by continuous functional calculus, with the twist factor taking value zero at the zero eigenvalue.

Hypotheses

• A supplied SeqProd N ℝ or SeqProd N ℂ carries closure on effects and the algebraic axioms S1 and S3–S7 of van de Wetering.
• The separate hypothesis S2 P requires continuity in the first argument for each fixed effect in the second argument, measured in the order-unit norm.
• The real theorem assumes 0 < N; the complex theorem assumes 3 ≤ N. The equations concern effect pairs only.

The full axiom definitions are in the statement file. S2 is explicit in both theorem declarations; it isn’t hidden in SeqProd.

What’s not proved

Both conclusions are necessity statements for a supplied product. The unique-existence quantifier gives a unique parameter for that product; it doesn’t assert that products exist.

Neither converse is registered in this entry. The repository proves complex-family admissibility elsewhere; it doesn’t construct the real Lüders product as an admissible SeqProd satisfying S2.

This entry doesn’t classify complex 2 × 2 products, quaternionic or exceptional Jordan cases, or all simple Euclidean Jordan algebras. Values of the total operation off the effect interval aren’t constrained by the conclusion.

open scoped Matrix ComplexOrder

theorem real_classification {N : ℕ} (hN : 0 < N)
    (P : SeqProd N ℝ) (hS2 : S2 P)
    {a b : Mat N ℝ} (ha : IsEffect a) (hb : IsEffect b) :
    P.sp a b = luders a b

theorem complex_classification {N : ℕ} (hN : 3 ≤ N)
    (P : SeqProd N ℂ) (hS2 : S2 P) :
    ∃! t : ℝ, ∀ a b : Mat N ℂ, IsEffect a → IsEffect b →
      P.sp a b = twist t a b