The Jordan trace form

The statement

Let Lₓ be left multiplication by x, and define τ(x, y) = tr(Lₓ∘ᵧ). This bilinear form is symmetric and associative against the Jordan product. In finite dimension, formal reality makes it positive definite, without assuming an inner product.

τ(x ∘ y, z) = τ(y, x ∘ z), and τ(x, x) > 0 for x ≠ 0.

The entry registers four declarations: symmetry, associativity, nonnegativity on the diagonal, and the equivalence τ(x, x) = 0 ↔ x = 0.

Hypotheses

• All four declarations use a nonunital nonassociative commutative ring with a real module structure and IsScalarTower ℝ J J, making multiplication real-bilinear.
• Symmetry needs no Jordan identity, finite-dimensionality, or formal reality.
• Associativity of the form adds IsCommJordan J, with no dimension or formal-reality hypothesis.
• Nonnegativity and definiteness add the Jordan identity, Module.Finite ℝ J, and formal reality in the finite-sum sense.

The trace is Mathlib’s total LinearMap.trace. The form isn’t normalized; the stated symmetry and associativity extend to carriers without a finite basis, where that trace takes value zero.

What’s not proved

No unit is assumed or produced. These results supply the Euclidean form; by themselves they don’t supply every part of a unital Euclidean Jordan algebra structure.

The entry doesn’t prove a normalization giving trace one to primitive idempotents, uniqueness of an associative positive definite form, or a relation to an existing inner product. It doesn’t classify the algebra or describe its cone of squares.

variable {J : Type*} [NonUnitalNonAssocCommRing J] [Module ℝ J] [IsScalarTower ℝ J J]

theorem traceForm_comm (x y : J) : traceForm x y = traceForm y x

theorem traceForm_assoc [IsCommJordan J] (x y z : J) :
    traceForm (x * y) z = traceForm y (x * z)

theorem traceForm_self_nonneg [IsCommJordan J] [Module.Finite ℝ J]
    (hfr : ∀ (k : ℕ) (f : Fin k → J), (∑ i, f i * f i) = 0 → ∀ i, f i = 0) (x : J) :
    0 ≤ traceForm x x

theorem traceForm_self_eq_zero_iff [IsCommJordan J] [Module.Finite ℝ J]
    (hfr : ∀ (k : ℕ) (f : Fin k → J), (∑ i, f i * f i) = 0 → ∀ i, f i = 0) (x : J) :
    traceForm x x = 0 ↔ x = 0