{"id":"palomar/PALOMAR-2026-10-08-000006","url":"https://github.com/scottnarmstrong/LiebThirring/tree/8bf4656f07f5aaa227b0b850d77b16976915bbd4","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-08-000006-v1.json","repo":"https://github.com/scottnarmstrong/LiebThirring","tags":["math-ph","math.AP","msc:81V70","msc:81Q10","msc:35Q40","mathematical-physics","stability-of-matter","lean-formalization"],"score":0,"title":"Stability of Matter in Lean: Lieb–Thirring, Ionization, the Thermodynamic Limit and Thomas–Fermi Theory","trust":"high","domain":"math-ph","source":"palomar","authors":["Scott Armstrong","Amélie Loher"],"reviews":0,"subject":"math-ph","summary":"A Lean 4 and Mathlib formalization of the stability of non-relativistic Coulomb matter in three dimensions. For normalized antisymmetric L2 electron states with q >= 1 spin states and static nuclei with charges between zero and Z, it proves a lower energy bound -C(q,Z)(N+M), uniformly in particle counts and nuclear positions. The main estimate is an additive inequality between nonnegative extended energies, valid even for infinite kinetic energy and nuclear collisions. A real quadratic-form theorem proves Coulomb finiteness and the lower bound for states with finite kinetic energy and…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-08","reactions":{},"formalized":true,"formalizes":[{"title":"The Lieb-Thirring inequalities: Recent results and open problems","identifier":"arxiv:2007.09326","relationship":"adapts"},{"title":"Methods of Modern Mathematical Physics: Uncertainty and Exclusion Principles in Quantum Mechanics","identifier":"arxiv:1805.03063","relationship":"adapts"},{"title":"Balanced distribution-energy inequalities and related entropy bounds","identifier":"doi:10.1215/00127094-1444305","relationship":"adapts"},{"title":"Bound on the maximum negative ionization of atoms and molecules","identifier":"doi:10.1103/PhysRevA.29.3018","relationship":"adapts"},{"title":"The constitution of matter: Existence of thermodynamics for systems composed of electrons and nuclei","identifier":"doi:10.1016/0001-8708(72)90023-0","relationship":"adapts"}]}