The Jordan spectral theorem

The statement

Every element of a finite-dimensional unital formally real Jordan algebra is a real linear combination of a finite family of idempotents. The idempotents are pairwise orthogonal under the Jordan product and sum to the unit. This is a spectral resolution of a single element.

x = ∑ᵢ λᵢ qᵢ, with qᵢ ∘ qᵢ = qᵢ, qᵢ ∘ qⱼ = 0 for i ≠ j, and ∑ᵢ qᵢ = e.

Orthogonality here refers to the product. The theorem doesn’t ask the product to be associative against the carrier’s inner product.

Hypotheses

• J is a finite-dimensional real inner-product space.
• m is a bundled real-bilinear product, assumed commutative and satisfying the Jordan identity.
• Formal reality is explicit: a vanishing finite sum of squares has zero arguments. The element e is a unit for m.
• No compatibility between m and the given inner product is assumed.

Finite-dimensionality matters. Real polynomials satisfy the other algebraic hypotheses, but their only idempotents are 0 and 1, so the polynomial X has no such resolution.

What’s not proved

The theorem doesn’t assert uniqueness, distinct coefficients, nonzero or primitive idempotents, or a fixed size of the family. The empty family is permitted on a trivial carrier.

It doesn’t assert that these idempotents belong to the subalgebra generated by x, build a functional calculus, or classify the algebra.

variable {J : Type*} [NormedAddCommGroup J] [InnerProductSpace ℝ J]

theorem spectral_resolution_bilinear [FiniteDimensional ℝ J] (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) (x : J) :
    ∃ (n : ℕ) (q : Fin n → J) (lam : Fin n → ℝ),
      (∀ i, m (q i) (q i) = q i) ∧
      (∀ i j, i ≠ j → m (q i) (q j) = 0) ∧
      (∑ i, q i) = e ∧
      x = ∑ i, lam i • q i