The results

Nine Palomar entries across three developments. Each page records the precise statement, the hypotheses, and the limits of the result.

Palomar entries

Entry links and registered source revisions.
Result	Palomar entry	Repository	Commit	Theorem names
Wigner's theorem over the reals	PALOMAR-2026-08-21-000001	ehrlich-b/sequential-products-lean	3c0e870eb2ac	`WignerReal.exists_isometry_of_transProbPreserving`
Albert's power-associativity theorem	PALOMAR-2026-08-21-000009	ehrlich-b/sequential-products-lean	9c6d92f5fc22	`AlbertPowerAssoc.jpow_mul_jpow`
Classification of sequential products	PALOMAR-2026-08-22-000006	ehrlich-b/sequential-products-lean	9c6d92f5fc22	`TwistNormalForm.real_classification` `TwistNormalForm.complex_classification`
Koecher / Alfsen–Shultz	PALOMAR-2026-08-23-000005	ehrlich-b/euclidean-jordan	58fb886dceab	`KoecherAlfsenShultz.orderIso_preservesJordan`
The Jordan spectral theorem	PALOMAR-2026-08-23-000006	ehrlich-b/euclidean-jordan	58fb886dceab	`JordanSpectral.spectral_resolution_bilinear`
The Jordan trace form	PALOMAR-2026-08-29-000001	ehrlich-b/euclidean-jordan	a0077822f037	`JordanTraceForm.traceForm_comm` `JordanTraceForm.traceForm_assoc` `JordanTraceForm.traceForm_self_nonneg` `JordanTraceForm.traceForm_self_eq_zero_iff`
The frame Peirce decomposition	PALOMAR-2026-08-29-000008	ehrlich-b/euclidean-jordan	a83407e4dbf7	`JordanFramePeirce.frameBlock_isInternal` `JordanFramePeirce.finrank_frameBlock_diag`
Hurwitz's theorem: dimension	PALOMAR-2026-08-29-000015	ehrlich-b/composition-algebras	e37e22b0571a	`HurwitzDimension.finrank_eq_one_or_two_or_four_or_eight`
Hurwitz's theorem: classification	PALOMAR-2026-08-29-000018	ehrlich-b/composition-algebras	98d4437ce1bf	`HurwitzClassification.hurwitz_classification`