Source and verification

This article explains family 090 of the October 6, 2026 OpenAI collection. Research conclusions are attributed to its manuscripts. The review covers statements, introductions, and selected proof mechanisms; it is not an independent verification of the complete proofs.

🏷️ Density, lattices, and pair energy

The triangular lattice of covolume one is

Covolume is the area of a fundamental parallelogram. The prefactor makes that area one and fixes the density scale for energy comparisons.

For a locally finite point set , let . The energy manuscripts consider centered density one, , and nonnegative potentials :

The sum counts ordered pairs. Centered density gives neither uniform bounds in every translated disk nor a positive minimum distance.

A function is completely monotone when for every nonnegative integer . Such functions are mixtures of decaying exponentials, connecting many repulsive energies to Gaussian kernels.

The atomic-certificate and universal-optimality manuscripts claim

under these assumptions. (OpenAI, 2026) (OpenAI, 2026b) Both sides may be infinite. For the lattice sum diverges when . A renormalized interaction in that range requires an additional definition; it cannot be obtained by subtracting unspecified infinities.

The Fourier-packing companion claims a sharp auxiliary function reproducing the classical planar circle-packing density. (OpenAI, 2026a) The Coulomb companion instead claims minimization of a renormalized field energy by the triangular lattice. (OpenAI, 2026c) Universal pair-energy optimality, a packing certificate, and Coulomb renormalization are distinct statements.

The universal-optimality manuscript also develops renormalized logarithmic and Riesz consequences. Their normalization is additional structure beyond the nonnegative pair sum. This article focuses on the common Gaussian mechanism and the explicitly defined Coulomb functional.

🏷️ The Gaussian auxiliary-function method

Use the Fourier convention

For each , the proposed certificate is a real radial Schwartz function satisfying

At nonzero points of , the first inequality is equality. At nonzero points of the dual lattice , the Fourier transform vanishes. Poisson summation therefore gives

For a finite configuration, Fourier positivity controls the quadratic sum of after frequency localization. In the density-one limit, low frequencies supply per point. Removing the diagonal costs . Domination by the Gaussian then gives the asserted energy bound. The manuscript treats the low-frequency limit under centered density, rather than inserting a uniform-density hypothesis. (OpenAI, 2026b) (OpenAI, 2026d)

The equality contacts account for the exact constant: the auxiliary function must touch the Gaussian at every nonzero lattice shell and vanish on every nonzero dual shell.

The atomic construction uses two finite blocks of size for , together with an infinite summable correction. Fourier duality handles the complementary range. Finite arithmetic controls the blocks, while analytic estimates control intervals, neighborhoods of contact zeros, and tails. These global sign conditions cannot be verified by a numerical grid alone.

Writing a completely monotone as a positive mixture of Gaussians transfers the inequalities. Nonnegativity permits Tonelli and Fatou arguments even when the final energy diverges. One need not construct a Schwartz auxiliary function for every possible mixture.

🏷️ The packing normalization

For disks of radius , admissible centers have pairwise distance at least one. The packing manuscript constructs

The linear-programming bound on center density is . Multiplying by disk area gives

This is the classical triangular-packing value. The contribution claimed here is the sharp Fourier certificate. The source builds it through shell interpolation, derivative control at zeros, finite inversion, and an infinite tail. Between contacts it uses polynomial positivity estimates; near contacts it exploits Taylor cancellation. (OpenAI, 2026a)

🏷️ Coulomb energy after removing self-interaction

The Coulomb paper considers fields satisfying, in distributions,

The background neutralizes density one. Near a point charge the energy diverges logarithmically. With a cutoff for a large square, renormalization takes

The functional is the limsup of this quantity divided by the square’s area as , with the source’s fixed-width cutoff convention. Under its centered counting bound, the manuscript claims , allowing infinite energy and excluding negative-infinite energy. (OpenAI, 2026c)

The proof uses Voronoi sectors and the planar average-side constraint. Local trial fields must match across boundaries. The source constructs one compatible comparison potential and retains a remainder . Treating each cell as an independent electrostatic problem would lose these interface conditions.

On finite tori, separation is established for the minimizers needed in the comparison; it is not assumed for every competitor. A square torus need not realize a triangular periodic configuration, so its lower energy bound is not an attainment assertion.

🏷️ Key steps and proof outlines

Interpolation fixes the equality data before signs are proved

A sharp Gaussian auxiliary function must satisfy two families of conditions: contact with the Gaussian on primal lattice shells and zeros of its Fourier transform on dual shells. At interior contact radii, derivatives must also match if a global one-sided inequality is to hold. The source therefore solves a coupled interpolation problem for values and first derivatives, called jets.

Cardinal basis functions are built so prescribed jets can be adjusted independently before Fourier transformation couples them again. Apparent quotients at interpolation nodes are interpreted through exact entire identities, for example

The integral supplies the removable value at and makes differentiation and Fourier transformation legitimate. The analogous second-order identity handles value-and-slope subtraction. This analytic treatment avoids assigning inconsistent limiting values at contact nodes. (OpenAI, 2026d)

Finite blocks and an infinite correction have different roles

The finite matrices determine a reference coefficient list and bound the main interpolation operator. The omitted coefficients live in a weighted summable sequence space. Block inversion and tail bounds then solve the exact infinite interpolation equations near the finite reference list. A numerically small residual is only an input to this correction argument; it is not exact interpolation on its own.

Positive quadrature rules estimate the finite moments. Analytic bounds on complex disks control Taylor remainders, and polynomial exactness plus positivity converts those remainders into rigorous quadrature errors. The arithmetic verification encloses constants and matrix entries with outward bounds. The atomic-certificate companion packages the same overall obligations through two finite blocks and a summable correction. (OpenAI, 2026b)

The signs are then checked on three kinds of region. Near a contact node, subtract the prescribed value and slope and estimate the remaining Taylor quotient. On a compact gap between nodes, use polynomial positivity bounds. Far out, use analytic tail estimates. These three regions cover every radius; a finite grid of sampled positive values would not replace any one of them.

Fourier positivity gives an energy inequality through a comparison measure

For finite signed measures , set . Fourier inversion gives

If , then , so . Choose as the point measure in a large region and as a suitable area comparison measure. The cross term captures the low-frequency density contribution. The manuscript estimates boundary effects under centered density rather than assuming uniform local density. Remove the diagonal , compare to the Gaussian off the diagonal, and pass to the lower limit.

Poisson summation at the triangular lattice identifies the sharp constant because every nonzero primal and dual interpolation condition is exact. Positive Gaussian mixtures then transfer the result to completely monotone interactions. Tonelli applies to the nonnegative mixture, and Fatou handles lower limits without requiring the final energy to be finite.

Packing uses a distinct normalization identity

For packing, the desired sign is beyond the minimum distance, rather than domination by a Gaussian. The companion again solves coupled Fourier interpolation and proves global signs. It then differentiates a dilated Poisson identity. Contact derivatives vanish except on the first shell, so the derivative identity fixes the relation between the values at zero and the first-shell data. A final dilation places the first contact at distance one. This gives the exact ratio used in the density bound. (OpenAI, 2026a)

Coulomb calibration must be globally compatible

The Coulomb source first proves existence and separation for finite-torus minimizers; arbitrary competitors need not be separated. It builds a triangular-cell calibration from the periodic Green function and decomposes general Voronoi cells into sectors. The local comparison potentials must match across shared edges. A single compatible potential then leaves the nonnegative remainder

Finite scalar inequalities and controlled infinite-mode tails bound the remaining sector terms. The planar average-side constraint combines them into the triangular lower bound. Approximation and boundary estimates transfer the torus result to the whole-plane renormalized functional. This argument concerns a specified field energy with subtracted self-interaction, so it cannot be replaced by applying the nonnegative pair-energy theorem to an undefined logarithmic sum. (OpenAI, 2026c)

See Also

Covering densities compares lattices and unrestricted arrangements in a different optimization problem. Mahler volume products gives another sharp constant whose analytic construction must preserve all equality conditions.

🏷️ Manuscripts and verification scope

The family scope page describes selected formalization coverage. The scope covers the atomic manuscript’s Gaussian and universal-optimality statements and the sharp packing certificate. It does not cover the other manuscript’s renormalized consequences or the Coulomb theorem. No Lean build, axiom audit, or manuscript-to-formal-statement equivalence check was performed for these notes.

OpenAI collection provides prerequisites and the reading sequence; coverage register records completed and pending families.

🐻  OpenAI 2026a. A sharp Fourier certificate for planar circle packing.
🐻  OpenAI 2026b. An atomic certificate for triangular-lattice universal optimality.
🐻  OpenAI 2026c. Triangular minimality for planar Coulomb renormalized energy.
🐻  OpenAI 2026d. Universal optimality of the triangular lattice.