Papers With

← All papers
First page of Equality of the Jellium and the Uniform Electron Gas Energies

Equality of the Jellium and the Uniform Electron Gas Energies

Mihály A. Csirik

math-ph Oct 14, 2026 · v1 cond-mat.quant-gas cond-mat.stat-mech
formalization mathlib physics analysis
Read PDF arXiv abstract Code
TL;DR
The lower and upper comparison proofs and the neutralization construction are formalized in Lean 4 with Mathlib, produced with AI assistance and released in a public repository.
Abstract
Jellium, a system of electrons in a uniform neutralizing background, and the uniform electron gas (UEG), a system of electrons with constant density and no background, are two standard models of the electron gas. We prove that the ground-state energy per unit volume of Jellium, as defined by Lieb and Narnhofer, coincides with the UEG energy defined by Lewin, Lieb and Seiringer, i.e. \[ e^\hbar_{\rm Jel}(ρ_0)=e^\hbar_{\rm UEG}(ρ_0). \] This equality was previously established in the classical case by Lewin, Lieb and Seiringer and independently by Cotar and Petrache.
Problem

Jellium (electrons in a uniform neutralizing background) and the uniform electron gas (constant density, no background) are two standard models of the electron gas. Their ground-state energies per unit volume had been shown equal only in the classical case. In the quantum case only a one-sided inequality was known, for a grand-canonical version of Jellium.

Approach

Two inequalities are proved separately, each compared against the canonical, neutral Dirichlet Jellium energy. One direction starts from minimizers of the Levy–Lieb functional. The other uses localization arguments, the Lieb–Oxford inequality and a neutralization construction. The comparisons of Sections 4.2–4.3 and the Appendix B construction were checked in Lean 4 with Mathlib, with AI help.

Results

For every spin multiplicity q, every density ρ0>0 and every ħ>0, the Jellium energy of Lieb–Narnhofer equals the UEG energy of Lewin–Lieb–Seiringer. As a consequence, known UEG properties transfer to Jellium, including its high-density Thomas–Fermi/Dirac asymptotics.