we-solve (beta)

Math-2647 · mathematics · Geometry

Gromov width of symmetric polar products

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For every $n\geq2$ and origin-symmetric convex body $K\subset\mathbb{R}^n$ with polar \[ K^\circ=\{y:\langle x,y\rangle\leq1\text{ for all }x\in K\}, \] is the Gromov width of $\operatorname{int}(K\times K^\circ)$ in standard symplectic $\mathbb{R}^{2n}$ equal to $4$? Equivalently, can every open standard ball of capacity $c<4$ be smoothly symplectically embedded into that interior, while none of capacity $c>4$ can?

Short English statement

For every $n\geq2$ and origin-symmetric convex body $K\subset\mathbb{R}^n$, with $K^\circ=\{y:\langle x,y\rangle\leq1\text{ for all }x\in K\}$, does $\operatorname{int}(K\times K^\circ)\subset\mathbb{R}^{2n}$ with the standard symplectic structure have Gromov width $4$; equivalently, does every open standard ball of capacity $c<4$ admit a smooth symplectic embedding into it, and none of capacity $c>4$?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

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

OpenAI claim summary for Math-2647

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 087; 2026-09-22).

Gromov width of symmetric polar products

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 087; 2026-09-22), the asserted result is that the interior polar product of an origin-symmetric body in dimension at least two has Gromov width four, including ball embeddings of every smaller capacity.

Mathematical statement of the claimed result

Manuscript 1.
For every origin-symmetric convex body $K\subset\mathbb R^n$, $n\ge2$, let $K^{\circ}=\{p:q\cdot p\le1\ (q\in K)\}$ and $U_K=\operatorname{int}K\times\operatorname{int}K^{\circ}$ in standard symplectic space $(\mathbb R^{2n},\sum_jdq_j\wedge dp_j)$. The claim asserts \[ c_G(U_K)=4,\qquad \forall0<c<4:\quad\{(q,p):\pi(|q|^2+|p|^2)<c\}\hookrightarrow U_K \] by a smooth symplectic embedding. The Gromov width is the supremum of these ball capacities; the endpoints are not an assertion that capacity four is itself attained.

Outline of the argument

For manuscript 1 (family 087; 2026-09-22), a planar holomorphic coordinate gives a uniform slice estimate that can be realized inside a polar product. Smooth approximation extends the construction to nonsmooth convex bodies; volume preservation then yields the symmetric volume-product bound.

Formal verification

For manuscript 1 (family 087; 2026-09-22), OpenAI lists Lean statements for this assertion: the interior polar product of an origin-symmetric body in dimension at least two has Gromov width four, including ball embeddings of every smaller capacity.

The central assertion is within the documented formal scope; the additional applications retain their own scope limits.

The linked family Comparator checks are GeneralMahler.lean, MahlerConjecture.lean, SymmetricMahlerEquality.lean, SymmetricPolar.lean.

Their named declarations include OAI.GeneralMahler.general_mahler, OAI.SymmetricMahler.symmetric_mahler, OAI.SymmetricMahler.symmetric_mahler_equality, OAI.SymmetricPolar.symmetric_polar_main.

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 →