Triangular-lattice optimality, long-range Riesz and Coulomb energies, and spherical logarithmic energy

4 papersLean

Proves that the triangular lattice minimizes the lower limit of energy per particle for every nonnegative completely monotone potential of squared distance among locally finite planar configurations of centered-disk density one. It also minimizes unit-background renormalized Riesz energies for \(0\lt s\lt 2\) and Coulomb energy, resolving Sandier–Serfaty and the two-dimensional Brauchart–Hardin–Saff conjecture on the linear term of optimal spherical logarithmic energy.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 4

An atomic certificate for triangular-lattice universal optimality

OpenAI · September 26, 2026

We prove that the density-one triangular lattice minimizes the lower energy per particle for every nonnegative completely monotone function of squared distance, among all locally finite planar configurations of centered disk density one. The comparison includes infinite energies. The proof constructs sharp Gaussian Fourier minorants using an atomic interpolation certificate.

Read PDF Download Source

Cite

@misc{OAI:An-atomic-certificate-for-triangular-lattice-universal-optimality-September-26-2026,
  author = {{OpenAI}},
  title = {{An atomic certificate for triangular-lattice universal optimality}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/An-atomic-certificate-for-triangular-lattice-universal-optimality-September-26-2026/paper.pdf}{OAI:An-atomic-certificate-for-triangular-lattice-universal-optimality-September-26-2026}},
  year = {2026}
}

Universal optimality of the triangular lattice

OpenAI · September 23, 2026

We prove universal energy minimality for the triangular lattice in the plane. Among locally finite configurations of centered density one, it minimizes the lower limit of centered-ball energy averages for every nonnegative completely monotone function of squared distance, including when the energy is infinite. We also prove triangular minimality for planar logarithmic and Riesz renormalized energies, with \(0\lt s\lt 2\) in the Riesz case, and the corresponding jellium minima. The proof uses sharp Gaussian Fourier bounds, positive mixtures, and heat-kernel comparison.

Read PDF Download Source

Cite

@misc{OAI:Universal-optimality-of-the-triangular-lattice-September-23-2026,
  author = {{OpenAI}},
  title = {{Universal optimality of the triangular lattice}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Universal-optimality-of-the-triangular-lattice-September-23-2026/paper.pdf}{OAI:Universal-optimality-of-the-triangular-lattice-September-23-2026}},
  year = {2026}
}

A sharp Fourier certificate for planar circle packing

OpenAI · September 23, 2026

We resolve the planar Cohn–Elkies sharpness conjecture: the two-point Fourier bound attains the optimal circle-packing density \(\pi/(2\sqrt3)\). We construct a radial Schwartz certificate and prove its global sign conditions using rigorous interval arithmetic and analytic estimates. The same certificate recovers the classical uniqueness of the triangular packing among periodic equality cases.

Read PDF Download Source

Cite

@misc{OAI:A-sharp-Fourier-certificate-for-planar-circle-packing-September-23-2026,
  author = {{OpenAI}},
  title = {{A sharp Fourier certificate for planar circle packing}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-sharp-Fourier-certificate-for-planar-circle-packing-September-23-2026/paper.pdf}{OAI:A-sharp-Fourier-certificate-for-planar-circle-packing-September-23-2026}},
  year = {2026}
}

Triangular minimality for planar Coulomb renormalized energy

OpenAI · September 23, 2026

We prove the Sandier–Serfaty conjecture: the triangular lattice of covolume one minimizes planar Coulomb renormalized energy over all admissible curl-free fields with a unit uniform background. Combined with Bétermin and Sandier's asymptotic formula, this also proves the Brauchart–Hardin–Saff conjecture for the linear term of optimal ordered-pair logarithmic energy on the unit two-sphere. The proof uses a direct Voronoi-cell comparison with rigorous interval arithmetic.

Read PDF Download Source

Cite

@misc{OAI:Triangular-minimality-for-planar-Coulomb-renormalized-energy-September-23-2026,
  author = {{OpenAI}},
  title = {{Triangular minimality for planar Coulomb renormalized energy}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Triangular-minimality-for-planar-Coulomb-renormalized-energy-September-23-2026/paper.pdf}{OAI:Triangular-minimality-for-planar-Coulomb-renormalized-energy-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalization proves that the density-one triangular lattice minimizes lower energy per particle among all locally finite planar configurations of centered-disk density one, for every nonnegative completely monotone function of squared distance. Infinite energies are allowed in the comparison.

It also constructs sharp radial Schwartz minorants for every Gaussian potential: each minorant lies below the Gaussian, has nonnegative real Fourier transform, agrees with the Gaussian at nonzero triangular-lattice points, and vanishes on nonzero dual-lattice points after Fourier transformation. For the stated parameter range, the formalization includes the explicit atomic interpolation construction.

The planar Cohn–Elkies sharpness conjecture asks whether the two-point Fourier method attains the optimal circle-packing density. The formalization constructs a radial Schwartz function \(f\) on \(\mathbb R^2\) with \(\widehat f(0)=1\), \(f(0)=2/\sqrt3\), \(\widehat f\) real and nonnegative everywhere, and \(f(x)\le0\) whenever \(\|x\|\ge1\). These are the sharp Fourier certificate conditions yielding density \(\pi/(2\sqrt3)\). The separate uniqueness statement for periodic equality cases is outside this selected theorem.

Comparator links

Result	Comparator statement
Sharp Gaussian minorants from an atomic certificate	AtomicGaussian.lean
Universal energy minimality of the triangular lattice	TriangularEnergy.lean
Gaussian Fourier minorants with their construction	TriangularGaussian.lean
Sharp Fourier certificate for planar circle packing	PlanarPacking.lean

Scope note on GitHub →