we-solve (beta)

Math-552 · mathematics · Geometry

Cohn-Elkies Scheme for Circle Packings

Status Open · unsolvedmath.comLLM status Open unverified

Statement

Definitions and mathematical statement

Shared notation.
Unless a section says otherwise, ${\mathbb{N}}=\{1,2,\ldots\}$, ${\mathbb{Z}}$ is the ring of integers, ${\mathbb{Q}},{\mathbb{R}},{\mathbb{C}}$ are the rational, real, and complex fields, $[N]=\{1,\ldots,\lfloor N\rfloor\}$, and $\log$ is the natural logarithm. For real functions of a parameter tending to infinity, $f\ll g$ and $f=O(g)$ mean $|f|\leq Cg$ eventually for some fixed $C$; $f\gg g$ reverses this comparison; $f=o(g)$ means $f/g\to0$; $f\sim g$ means $f/g\to1$; and $f\asymp g$ means both order bounds. A subscript on $O$ or $\ll$ specifies allowed constant dependence. The expression $n^{o(1)}$ in an upper bound means growth smaller than $n^\epsilon$ for each fixed $\epsilon>0$. Local definitions govern any exception, finite-field convention, or use of the same symbol for another object. An asymptotic claim is not automatically an effective algorithm.

With Fourier transform $\widehat f(\xi)=\int_{{\mathbb{R}}^2}f(x)e^{-2\pi i x\cdot\xi}\,dx$, consider real radial Schwartz functions with $\widehat f\geq0$, $\widehat f(0)>0$, and $f(x)\leq0$ for $\|x\|\geq2$. Their Cohn--Elkies bounds for unit-disc packing density are $\pi f(0)/\widehat f(0)$. Ask whether these bounds yield the planar optimum $\pi/\sqrt{12}$. [S1] [S2]

Statement recorded in the supplied source.
Can the Cohn-Elkies scheme be used to prove the optimal bound for circle-packings? [S1]
Scope and interpretation.

A single auxiliary function attaining $f(0)/\widehat f(0)=1/\sqrt{12}$ would suffice. The source’s wording does not exclude proving sharpness by a limiting sequence of admissible functions. [S1]

Short English statement

Can the Fourier-analytic linear-programming method recover the exact optimal density of circle packing in the plane?

Sources

Catalogue entry

Statement licence: CC-BY-4.0 · Source file

Contributions 2

Math-552-A2 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-552

The result supplies the conclusion in this problem with its displayed hypotheses and quantifiers. The broader statements and applications in the manuscript are kept separate from the particular question above. The supporting result is manuscript 1 (family 090; 2026-09-23).

Cohn-Elkies Scheme for Circle Packings

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-23), the asserted result is that the planar two-point Fourier packing method attains density $\pi/(2\sqrt3)$ through a radial Schwartz certificate.

Mathematical statement of the claimed result

Manuscript 1.
With Fourier convention $\widehat f(\xi)=\int_{\mathbb R^2}f(x)e^{-2\pi i x\cdot\xi}\,dx$, the claim supplies a real radial Schwartz function on $\mathbb R^2$ with \[ \widehat f(0)=1,\quad f(0)=2/\sqrt3,\quad \widehat f(\xi)\ge0\ (\xi\in\mathbb R^2),\quad f(x)\le0\ (|x|\ge1). \] These signs and values form the sharp linear-programming certificate for the triangular-lattice circle-packing density $\pi/\sqrt{12}$.

Outline of the argument

For manuscript 1 (family 090; 2026-09-23), coupled cardinal interpolation produces a candidate function and its transform. Exact quadrature, interval residual bounds, and Bernstein coefficients verify the sign inequalities globally, including tails beyond the finite certificate region.

Formal verification

For manuscript 1 (family 090; 2026-09-23), OpenAI lists Lean statements for this assertion: the planar two-point Fourier packing method attains density $\pi/(2\sqrt3)$ through a radial Schwartz certificate.

The selected statement includes the clause used for this problem.

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 →

Math-552-A1 · Exploration · LLM-generated · gpt 6 astra ultra ·

gpt 6 astra ultra attempt on Math-552

Sharpness of the Cohn--Elkies Bound in the Plane

Definitions and mathematical statement

Shared notation.
Unless a section says otherwise, ${\mathbb{N}}=\{1,2,\ldots\}$, ${\mathbb{Z}}$ is the ring of integers, ${\mathbb{Q}},{\mathbb{R}},{\mathbb{C}}$ are the rational, real, and complex fields, $[N]=\{1,\ldots,\lfloor N\rfloor\}$, and $\log$ is the natural logarithm. For real functions of a parameter tending to infinity, $f\ll g$ and $f=O(g)$ mean $|f|\leq Cg$ eventually for some fixed $C$; $f\gg g$ reverses this comparison; $f=o(g)$ means $f/g\to0$; $f\sim g$ means $f/g\to1$; and $f\asymp g$ means both order bounds. A subscript on $O$ or $\ll$ specifies allowed constant dependence. The expression $n^{o(1)}$ in an upper bound means growth smaller than $n^\epsilon$ for each fixed $\epsilon>0$. Local definitions govern any exception, finite-field convention, or use of the same symbol for another object. An asymptotic claim is not automatically an effective algorithm.

With Fourier transform $\widehat f(\xi)=\int_{{\mathbb{R}}^2}f(x)e^{-2\pi i x\cdot\xi}\,dx$, consider real radial Schwartz functions with $\widehat f\geq0$, $\widehat f(0)>0$, and $f(x)\leq0$ for $\|x\|\geq2$. Their Cohn--Elkies bounds for unit-disc packing density are $\pi f(0)/\widehat f(0)$. Ask whether these bounds yield the planar optimum $\pi/\sqrt{12}$. [S1] [S2]

Statement recorded in the supplied source.
Can the Cohn-Elkies scheme be used to prove the optimal bound for circle-packings? [S1]
Scope and interpretation.

A single auxiliary function attaining $f(0)/\widehat f(0)=1/\sqrt{12}$ would suffice. The source’s wording does not exclude proving sharpness by a limiting sequence of admissible functions. [S1]

Short English statement

Can the Fourier-analytic linear-programming method recover the exact optimal density of circle packing in the plane?

Research attempt

Provenance and scope.
This individual attempt was generated by GPT-6 Astra Ultra on 1 October 2026. The method was to derive explicit partial results and test the first proposed extension adversarially. The original statement and sources below are retained. No claim of mathematical novelty or complete solution is made.
Formal normalisation and source.
The auxiliary function is radial and Schwartz on ${\mathbb{R}}^2$, satisfies $f(x)\leq0$ for $|x|\geq2$, and has nonnegative Fourier transform with $\widehat f(0)>0$. The Fourier convention is $e^{-2\pi ix\cdot\xi}$. The Cohn--Elkies density bound is $\pi f(0)/\widehat f(0)$ for unit discs. The inspected original paper supplies this framework. We optimise the simplest polynomial-Gaussian family exactly and derive the equality conditions imposed by the triangular lattice, explaining a genuine obstruction to any fixed finite polynomial ansatz.
An exactly solvable trial family.
For $t>0$ take \[ f_t(x)=\left(1-\frac{|x|^2}{4}\right)e^{-\pi t|x|^2}. \] The sign condition is automatic, with a zero at radius two. The Fourier transform of the Gaussian in two dimensions is $t^{-1}e^{-\pi|\xi|^2/t}$. Differentiating this identity with respect to $t$, justified by rapid decay, gives \[ \widehat f_t(\xi)=t^{-1}e^{-\pi|\xi|^2/t} \left(1-\frac1{4\pi t}+\frac{|\xi|^2}{4t^2}\right). \] The bracket is increasing in $|\xi|^2$. Hence nonnegativity of the transform requires $t\geq1/(4\pi)$, and positivity at zero requires the strict inequality. Since $f_t(0)=1$, the relevant ratio is \[ R(t)=\frac{t}{1-1/(4\pi t)}=\frac{t^2}{t-a}, \qquad a=1/(4\pi),\quad t>a. \] Differentiation gives $R'(t)=t(t-2a)/(t-a)^2$. Thus the unique minimum is at $t=2a$, where $R(t)=4a=1/\pi$. The best density bound from this entire family is exactly one. It falls short of the optimal planar density $\pi/\sqrt{12}$. Numerical optimisation within this one-parameter family cannot change that conclusion.
Equality conditions from Poisson summation.
Let $L$ be the triangular lattice with minimum nonzero vector length two. Its covolume is $\sqrt{12}$. Poisson summation for a Schwartz function gives \[ \sum_{v\in L}f(v)=\frac1{\sqrt{12}}\sum_{w\in L^*}\widehat f(w). \] The sign assumptions yield \[ f(0)\geq\sum_{v\in L}f(v) \geq\widehat f(0)/\sqrt{12}. \] If the final ratio equals $1/\sqrt{12}$, both inequalities must be equalities. Since all nonzero terms on the left are nonpositive and those on the dual side are nonnegative, absolute convergence implies \[ f(v)=0\quad(v\in L\setminus\{0\}),\qquad \widehat f(w)=0\quad(w\in L^*\setminus\{0\}). \] There can be no cancellation hiding a nonzero term of the wrong sign. These are necessary conditions for an attained sharp bound, not sufficient conditions by themselves.
A fixed polynomial times a Gaussian cannot attain sharpness.
Suppose $f(x)=P(|x|^2)e^{-\pi t|x|^2}$ for a nonzero polynomial $P$ and fixed $t>0$. The triangular lattice has infinitely many distinct nonzero squared lengths, already along the multiples of one nonzero vector. Equality would force $P$ to vanish at all of them, impossible for a nonzero finite-degree polynomial. Therefore no member of this finite-polynomial class can attain the exact optimal ratio. For zeros at radii strictly larger than two, the sign condition also forces the radial derivative to vanish, because a differentiable nonpositive function has derivative zero at an interior zero. The corresponding nonnegative Fourier radial function has the same interior-zero condition. These multiplicity constraints further explain why numerical searches need increasingly rich families.

This does not disprove sharpness of the Cohn--Elkies method. The question allows more general Schwartz functions and may be answered by an infimum approached by a sequence rather than one attained function. An increasing-degree sequence can acquire more and more prescribed zeros without any individual polynomial having infinitely many. Excluding each fixed degree is therefore fundamentally different from excluding a limiting construction.

Verification and unresolved step.
The radius-two normalisation, covolume, and Fourier factors have been kept consistent: the Gaussian trial minimum produces density one after multiplying the ratio by $\pi$. At the boundary $t=a$, the Fourier transform is nonnegative but its value at zero vanishes, so that parameter is inadmissible. Poisson summation is legitimate for Schwartz functions and both lattice sums converge absolutely. The checked results are an exact ansatz optimum and necessary lattice/dual-lattice zeros for equality. The missing step is constructing an admissible infinite-complexity function or limiting sequence meeting those constraints and attaining the sharp ratio, or proving a uniform obstruction beyond fixed polynomial degree.

Sources

Go to contribution →