Degenerations of Jordan algebras
Victor Bovdi, Ivan Kaygorodov, Yury Popov, Azamat Saydaliyev, Yury Volkov
math.RA
Oct 22, 2026 · v1
TL;DR
All degenerations and non-degenerations of the classified Jordan algebras were formally verified in Lean 4 with Mathlib, including Nullstellensatz certificates.
Abstract
We describe all degenerations of complex $4$-dimensional Jordan algebras and of complex $5$-dimensional nilpotent Jordan algebras. The proofs do not use other papers on degenerations, and all degenerations and non-degenerations were formally verified in the proof assistant Lean 4. The graph of primary degenerations of $4$-dimensional Jordan algebras has $73$ vertices and $160$ edges. The variety of $5$-dimensional nilpotent Jordan algebras is stratified into $63$ normal forms, five of which are one- or two-parameter families; together with two special members of a family this gives $65$ objects, and the graph of primary degenerations has $154$ edges. In particular, we describe all irreducible components of the corresponding varieties: the variety of $4$-dimensional Jordan algebras has $10$ irreducible components, and the variety of $5$-dimensional nilpotent Jordan algebras has dimension $22$ and $5$ irreducible components.
Problem
Classify all degenerations of complex 4-dimensional Jordan algebras and complex 5-dimensional nilpotent Jordan algebras, and determine the irreducible components of the corresponding varieties.
Approach
Each primary degeneration is exhibited by an explicit parametrized basis. Each primary non-degeneration is proved by an explicit invariant closed set. The emptiness conditions on Bruhat cells are checked with Nullstellensatz certificates found by Gröbner basis computations. All results were formally verified in Lean 4 with Mathlib, without relying on prior papers on degenerations.
Results
The graph of primary degenerations of 4-dimensional Jordan algebras has 73 vertices and 160 edges, and the variety has 10 irreducible components. The 5-dimensional nilpotent Jordan algebras give 65 objects with 154 primary degeneration edges, and the variety has dimension 22 and 5 irreducible components.
