{"id":"palomar/PALOMAR-2026-08-29-000001","url":"https://github.com/ehrlich-b/euclidean-jordan/tree/a0077822f037d5de7bdcbf3f9f498cc00f361a4a","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-29-000001-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":"The Jordan trace form tau(x,y) = tr(L_{x*y}), constructed from the multiplication rather than assumed: symmetric, associative, and positive definite. Symmetry and associativity need neither finite dimensionality nor formal reality; positive definiteness needs both, and runs through the spectral theorem. The carrier is not assumed unital, so this supplies the Euclidean form itself and does not by itself establish a unital Euclidean Jordan algebra. Sits directly on Mathlib's IsCommJordan. Coordinatization is absent. Machine checked, not peer reviewed, no priority claim.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-29","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"}]}