Open Research Index

Stability of Matter in Lean: Lieb–Thirring, Ionization, the Thermodynamic Limit and Thomas–Fermi Theory

Scott Armstrong, Amélie Loher

Palomar Registrypalomar/PALOMAR-2026-10-08-000006Oct 8, 2026math-phscore 0

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…

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-10-08-000006
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-08-000006/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-08-000006/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'