The frame Peirce decomposition

The statement

Given a Jordan frame, its Peirce blocks form an internal direct sum of the Euclidean Jordan algebra. The blocks are indexed by unordered pairs of frame indices, so each block is counted once. In finite dimension, every diagonal block is one-dimensional.

J = ⨁ᵢ≤ⱼ Vᵢⱼ, and dimℝ Vᵢᵢ = 1.

The diagonal block Vᵢᵢ is the 1-eigenspace of multiplication by the frame element pᵢ. For i ≠ j, Vᵢⱼ is the joint ½-eigenspace for multiplication by pᵢ and pⱼ. DirectSum.IsInternal asserts both independence and spanning.

Hypotheses

• J is a real inner-product space with a commutative bilinear unital product satisfying the Jordan identity and associativity against the inner product.
• A frame F : JordanFrame J n is supplied as data: its members are pairwise orthogonal primitive idempotents summing to the unit.
• The direct-sum theorem has no finite-dimensionality hypothesis. Primitivity remains a formal input because it’s carried by JordanFrame.
• The diagonal-dimension theorem additionally assumes FiniteDimensional ℝ J and uses primitivity.

The inner product can be any positive definite associative one; it isn’t required to be the trace form.

What’s not proved

The entry doesn’t produce a frame, prove conjugacy of frames, or identify its cardinality with the rank of J. The multiplication table between blocks isn’t registered in these two declarations.

It doesn’t prove a matrix coordinatization, classify simple Jordan algebras, or construct an octonionic Jordan algebra. A decomposition for a complete orthogonal idempotent family without primitivity isn’t the formal statement here.

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

variable {n : ℕ}

theorem frameBlock_isInternal (F : JordanFrame J n) : DirectSum.IsInternal (frameBlock F)

theorem finrank_frameBlock_diag [FiniteDimensional ℝ J] (F : JordanFrame J n) (i : Fin n) :
    Module.finrank ℝ ↥(frameBlock F s(i, i)) = 1