{"id":"palomar/PALOMAR-2026-08-23-000005","url":"https://github.com/ehrlich-b/euclidean-jordan/tree/58fb886dceab0a3439c9ba3fca37f01073f2a0a4","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-23-000005-v1.json","repo":"https://github.com/ehrlich-b/euclidean-jordan","tags":["math.RA","math.OA","math.FA","msc:17C20","msc:17C27","msc:17C37","msc:17C65","msc:17A15","msc:46L70","jordan-algebras"],"score":0,"title":"ehrlich-b/euclidean-jordan","trust":"high","domain":"math.RA","source":"palomar","authors":["Bryan Ehrlich"],"reviews":0,"subject":"math.RA","summary":"A Euclidean Jordan algebra is a finite-dimensional real inner-product space carrying a commutative bilinear product with a unit, satisfying the Jordan identity (x*y)*(x*x) = x*(y*(x*x)) and the associativity of the inner product = . This is Faraut-Koranyi's definition (Analysis on Symmetric Cones, III.1). This development formalizes the classical structure theory of these algebras. Mathlib carries the Jordan identity as the typeclass IsCommJordan together with five operator-commutation lemmas, and nothing beyond that: no idempotent theory, no Peirce decomposition, no spectral theory. This…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-23","reactions":{},"formalized":true,"formalizes":[{"title":"Analysis on Symmetric Cones","identifier":"","relationship":"formalizes"},{"title":"Power-associative rings","identifier":"","relationship":"adapts"},{"title":"Geometry of State Spaces of Operator Algebras","identifier":"","relationship":"formalizes"}]}