Koecher / Alfsen–Shultz

The statement

Take a finite-dimensional formally real Jordan algebra with a unit. A real-linear bijection that fixes the unit and preserves its sums-of-squares cone in both directions must preserve the Jordan product. Under these hypotheses, the order and unit determine the multiplication.

Φ(x ∘ y) = Φ(x) ∘ Φ(y).

The cone predicate IsSoS m z means that z is a finite sum of terms m a a. The empty sum is allowed.

Hypotheses

• J carries a real module structure, is finitely generated over ℝ, and has a NormedAddCommGroup instance.
• The bundled real-bilinear map m is commutative and satisfies the Jordan identity. Formal reality means a finite sum of squares vanishes only when all its arguments vanish.
• e is a unit. The real-linear equivalence Φ fixes e.
• The cone condition is a biconditional: IsSoS m x ↔ IsSoS m (Φ x) for every x. Preservation in just one direction isn’t the stated hypothesis.

The normed carrier is part of the formal signature; the argument doesn’t use the norm. No inner product or trace form is assumed.

What’s not proved

Linearity and bijectivity are inputs, encoded by J ≃ₗ[ℝ] J. This isn’t a theorem deriving linearity from an arbitrary order isomorphism, and it doesn’t address general JB-algebras.

It doesn’t construct a Jordan algebra from a homogeneous cone, classify Jordan algebras, or identify the carrier with a matrix algebra.

variable {J : Type*} [NormedAddCommGroup J] [Module ℝ J] [Module.Finite ℝ J]

theorem orderIso_preservesJordan (m : J →ₗ[ℝ] J →ₗ[ℝ] J)
    (hcomm : ∀ x y : J, m x y = m y x)
    (hjordan : ∀ a b : J, m (m a b) (m a a) = m a (m b (m a a)))
    (hfr : ∀ (k : ℕ) (f : Fin k → J), (∑ i, m (f i) (f i)) = 0 → ∀ i, f i = 0)
    (e : J) (he : ∀ y : J, m e y = y)
    (Φ : J ≃ₗ[ℝ] J) (hunital : Φ e = e)
    (horder : ∀ x : J, IsSoS m x ↔ IsSoS m (Φ x)) (x y : J) :
    Φ (m x y) = m (Φ x) (Φ y)