Machine-checked, not peer-reviewed; no priority claim.
Mathematics.
With proofs you can check.
I’m Bryan Ehrlich. This is a collection of machine-checked results in Jordan algebras, sequential products, and composition algebras, formalized in Lean.
Read the mathematics first, then the precise statement and the proof. The hypotheses and limits sit beside each result.
The results
Sequential products & rigidity
3 entries- 01Wigner's theorem over the realsA map on real rays preserving transition probabilities comes from an isometry.
- 02Albert's power-associativity theoremDifferent bracketings of powers of a single element agree.
- 03Classification of sequential productsThe real Lüders formula and the unique complex twist normal form.
Euclidean Jordan algebras
4 entries- 04Koecher / Alfsen–ShultzA linear bijection fixing the unit and preserving the positive cone is a Jordan automorphism.
- 05The Jordan spectral theoremA single element resolves into a real combination of orthogonal idempotents.
- 06The Jordan trace formThe form τ(x, y) = tr(Lₓ∘ᵧ) comes from the multiplication itself.
- 07The frame Peirce decompositionThe joint eigenspaces of a Jordan frame are independent and span the algebra.
Composition algebras
2 entriesReading a formal result
Lean checks that a proof follows from its stated hypotheses. It doesn't settle whether the statement captures the intended mathematics.
Each page gives the statement, its assumptions, its limits, and links to the source at the registered commit. The repositories include axiom audits; the challenge files state the problems, and the solution files prove them. The registry index lists entry IDs and source revisions.
In progress
- Cone teleportationIn progress
- Cayley–DicksonIn progress
These topics aren't presented as results here.