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

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

- [An atomic certificate for triangular-lattice universal optimality](../../preprints/An-atomic-certificate-for-triangular-lattice-universal-optimality-September-26-2026/paper.pdf)
- [A sharp Fourier certificate for planar circle packing](../../preprints/A-sharp-Fourier-certificate-for-planar-circle-packing-September-23-2026/paper.pdf)

## 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](../ComparatorChallenges/AtomicGaussian.lean) |
| Universal energy minimality of the triangular lattice | [TriangularEnergy.lean](../ComparatorChallenges/TriangularEnergy.lean) |
| Gaussian Fourier minorants with their construction | [TriangularGaussian.lean](../ComparatorChallenges/TriangularGaussian.lean) |
| Sharp Fourier certificate for planar circle packing | [PlanarPacking.lean](../ComparatorChallenges/PlanarPacking.lean) |