we-solve (beta)

Math-2316 · mathematics · Geometry

Linear-Programming Sharpness and Universal Lattice Optimality

Status Partially solved · unsolvedmath.comLLM status Open unverified

Statement

Definitions and mathematical statement

Shared notation.
$\mathbb N$, $\mathbb Z$, $\mathbb Q$, $\mathbb R$, and $\mathbb C$ denote the natural numbers, integers, rationals, reals, and complex numbers, respectively. All additional parameters and hypotheses are specified in the question.
Statement recorded in the supplied source.
Does the linear-programming auxiliary-function method prove universal optimality for a finite spherical configuration exactly when the linear-programming bound for spherical codes is sharp for that configuration; and does its Euclidean analogue prove universal optimality for the hexagonal lattice, the $E_8$ root lattice, and the Leech lattice?

Formulation references: [S1], [S2].

Short English statement

Does the linear-programming auxiliary-function method prove universal optimality for a finite spherical configuration exactly when the linear-programming bound for spherical codes is sharp for that configuration; and does its Euclidean analogue prove universal optimality for the hexagonal lattice, the $E_8$ root lattice, and the Leech lattice?

Sources

Catalogue entry

Statement licence: CC-BY-SA-4.0 · Source file

Contributions 1

Math-2316-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2316

Sharp Gaussian Fourier minorants supply the planar triangular-lattice part. The proposed relation between spherical code sharpness and universal optimality for all finite spherical configurations is a different clause and is not proved by the planar construction.

Linear-Programming Sharpness and Universal Lattice Optimality

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 090; 2026-09-26), the asserted result is that the triangular lattice minimizes the lower per-particle energy for all nonnegative completely monotone squared-distance potentials among centered-density-one planar configurations; In manuscript 2 (family 090; 2026-09-23), the asserted result is that the triangular lattice minimizes that full class of planar pair energies and also the stated logarithmic and Riesz renormalized energies, including corresponding jellium minima.

Mathematical statement of the claimed result

Manuscript 1.
Let $b=\sqrt3/2$ and $A=b^{-1/2}\{m(1,0)+n(1/2,b):m,n\in\mathbb Z\}$, the density-one triangular lattice. A locally finite planar configuration $\mathcal C$ has centered-disk density one if $N_R=|\mathcal C\cap B_R|$ satisfies $N_R/(\pi R^2)\to1$. For smooth $g:(0,\infty)\to[0,\infty)$ with $(-1)^jg^{(j)}(t)\ge0$ for every $j\ge0,t>0$, set \[ E_g(\mathcal C)=\liminf_{R\to\infty}\frac1{N_R} \sum_{\substack{x,y\in\mathcal C\cap B_R\\x\ne y}}g(|x-y|^2). \] The asserted universal comparison is \[ E_g(\mathcal C)\ge E_g(A)=\sum_{a\in A\setminus\{0\}}g(|a|^2). \] Pairs are ordered, and the inequality is interpreted in the extended nonnegative reals; periodicity or uniform local counting bounds are not required.
Manuscript 2.
Let $A=\sqrt{2/\sqrt3}[\mathbb Z(1,0)+\mathbb Z(1/2,\sqrt3/2)]$. A locally finite planar configuration $\mathcal C$ has centered-disk density one when $|\mathcal C\cap B_R|/(\pi R^2)\to1$. For every smooth completely monotone $g:(0,\infty)\to[0,\infty)$, meaning $(-1)^rg^{(r)}\ge0$ for all integers $r\ge0$, define the ordered-pair energy per point \[ E_g(\mathcal C)=\liminf_{R\to\infty}\frac1{|\mathcal C\cap B_R|} \sum_{\substack{x,y\in\mathcal C\cap B_R\\x\ne y}}g(|x-y|^2). \] The claimed universal inequality, including infinite values, is \[ E_g(\mathcal C)\ge\sum_{a\in A\setminus\{0\}}g(|a|^2)=E_g(A). \] Its cited renormalized-energy extension allows $0\le s<2$. Set $g_0(X)=-\log|X|$, $g_s(X)=|X|^{-s}$ for $s>0$, $k=0$ at $s=0$ and $k=1$ otherwise, $w_s=1$ at $s=0$ and $w_s=|y|^{s-1}$ otherwise, and $\kappa_0=2\pi$, $\kappa_s=4\pi$ for $s>0$. Admissible gradient fields obey \[ -\operatorname{div}(w_sE)=\kappa_s(\sum_{p\in\mathcal C}\delta_{(p,0)}-\delta_{\mathbb R^2}) \] in $\mathbb R^{2+k}$, with $w_sE$ locally integrable and $E$ locally in $L^t$ for some $1<t<2$ at $s=0$, or $1<t<\min(2,2/s,3/(s+1))$ at $s>0$. For $f_{\eta}=(g_s-g_s(\eta))_+$ and $E_{\eta}=E-\sum_p\nabla f_{\eta}(\cdot-(p,0))$, use the normalization \[ W_s(\mathcal C)=\inf_E\lim_{\eta\downarrow0}\limsup_{R\to\infty} \left[\frac1{R^2}\int_{[-R/2,R/2]^2\times\mathbb R^k}w_s|E_{\eta}|^2 -\kappa_sg_s(\eta)\right]. \] The periodic version $W_{s,L}$ uses the mean-zero periodic potential and replaces $R^{-2}$ by reciprocal torus area. For every integer $n\ge1$, $N=n^2$, and every $N$ distinct points on $\mathbb R^2/(nA)$, the claim is \[ W_{s,nA}(a_1,\ldots,a_N)\ge W_{s,nA}(A/(nA)),\qquad W_s(\mathcal C)\ge W_s(A),\qquad e_{\rm Jel}^{(s)}=\kappa_s^{-1}W_s(A). \] Here $e_{\rm Jel}^{(s)}$ denotes the thermodynamic minimum per unit area of the ordered-pair $g_s$ interaction with a uniform density-one neutralizing background, including both particle--background and background--background terms.

Outline of the argument

For manuscript 1 (family 090; 2026-09-26), sharp Gaussian minorants are obtained by solving finite atomic interpolation systems and controlling the infinite correction. Fourier positivity transfers each Gaussian bound to general configurations, and positive Laplace mixtures include singular potentials and infinite energies.

For manuscript 2 (family 090; 2026-09-23), cardinal spectral interpolation is certified using positive quadrature and rigorous finite parameter bounds. Sharp Gaussian Fourier comparisons are mixed to treat general potentials, while heat-kernel comparison passes to renormalized and jellium energies.

Formal verification

For manuscript 1 (family 090; 2026-09-26), OpenAI lists Lean statements for this assertion: the triangular lattice minimizes the lower per-particle energy for all nonnegative completely monotone squared-distance potentials among centered-density-one planar configurations.

This coverage does not establish a formal proof of the complete problem as stated here.

No Lean formalization is listed at this snapshot for manuscript 2 (family 090; 2026-09-23).

The linked family Comparator checks are AtomicGaussian.lean, PlanarPacking.lean, TriangularEnergy.lean, TriangularGaussian.lean.

Their named declarations include OAI.AtomicTriangular.sharp_gaussian_minorants_atomic, OAI.AtomicTriangular.sharp_gaussian_minorants_with_construction, OAI.AtomicTriangular.universal_energy_minimum, OAI.sharp_fourier_certificate.

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources

Go to contribution →