{"id":"palomar/PALOMAR-2026-08-21-000001","url":"https://github.com/ehrlich-b/sequential-products-lean/tree/3c0e870eb2acb1320b62e62c791c9365f7e5260b","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-21-000001-v1.json","repo":"https://github.com/ehrlich-b/sequential-products-lean","tags":["math.OA","math.RA","quant-ph","msc:17C65","msc:81P16","msc:46L70","msc:81P10","msc:15B57","msc:17C90","operator-algebras"],"score":0,"title":"ehrlich-b/sequential-products-lean","trust":"high","domain":"math.OA","source":"palomar","authors":["Bryan Ehrlich"],"reviews":0,"subject":"math.OA","summary":"A sequential product on the effects of an order-unit space is a binary operation a & b, read \"first test a, then test b with the state updated by the first test\", satisfying the seven axioms S1-S7 of van de Wetering (arXiv:1803.11139, Definition 2). This development registers two classification theorems for such products on the Hermitian matrix algebras. On H_N(R), the Hermitian N x N real matrices with N >= 1, every sequential product is the Lueders product sqrt(a) b sqrt(a): there is no free parameter. On H_N(C) with N >= 3, every sequential product has the twist normal form a^(1/2+it) b…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-21","reactions":{},"formalized":true,"formalizes":[{"title":"Sequential Products on Euclidean Jordan Algebras: Classification in Rank at Least Three and the Complex Qubit","identifier":"","relationship":"formalizes"},{"title":"On Jordan algebras of linear transformations","identifier":"","relationship":"formalizes"},{"title":"Wigner's theorem on symmetries of quantum mechanical systems, real case","identifier":"","relationship":"formalizes"}]}