Symplectic Geometry

Motivation

Fixed-point bounds compare Hamiltonian dynamics with critical points of smooth functions. Degenerate fixed points are central to the unrestricted formulation tested here. The pinned manuscript supplies the research context.

Setting

The space is the complex projective quadric threefold, represented through its unit quadric and quotient tangent directions. Hamiltonian maps are endpoints of the specified smooth isotopies.

Formalization target

The selected goal is OAI.ArnoldCounterexample.main. Its central assertion is

$$\#\mathrm{Fix}(\varphi)=3<4\leq\mathrm{Crit}(Q^3).$$

The theorem states that the complex projective quadric Q = {[z] ∈ ℂP⁴ : ∑ⱼ₌₀⁴ zⱼ² = 0} admits a Hamiltonian bijection φ with exactly three fixed points, whereas every smooth real-valued function on Q has at least four critical points, including functions with degenerate critical points; equivalently, 3 < 4 ≤ the infimum of their critical-set cardinalities, with infinite cardinalities recorded as ∞. Here Hamiltonian means that φ is the endpoint of an isotopy starting at the identity whose forward maps, inverse maps, and Hamiltonian have globally smooth extensions on ℝ × ℂ⁵. For times in [0,1], the maps preserve the unit quadric, are inverse there, and commute with multiplication by unit complex scalars; the Hamiltonian is invariant under these scalars. They satisfy ω(∂ₜFₜ(z),v) = dHₜ(Fₜ(z))[v] for every horizontal v at Fₜ(z), where ω(u,v) = 2 Im ∑ⱼ conjugate(uⱼ)vⱼ and horizontality at z means both ∑ⱼ conjugate(zⱼ)vⱼ = 0 and ∑ⱼ zⱼvⱼ = 0. Smooth functions on Q are those with smooth local extensions after pullback to the unit quadric, and criticality means that every such extension has zero derivative in all horizontal directions. Moreover, φ has a degenerate fixed point: some unit representative z and nonzero horizontal vector v admit a smooth local lift G of φ with G(z) = z and DG(z)v − v = a iz for some real a. Thus the induced derivative on the quotient tangent has a genuine nonzero eigenvector with eigenvalue 1.

Significance and status

The goal includes the lower bound on all smooth critical sets and at least one degenerate fixed point. A rational cup-length computation is not a separate conclusion of this target. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

Counting fixed points is insufficient: the construction must satisfy the Hamiltonian lift conditions and give a genuine nonzero quotient-tangent eigenvector at a degenerate point.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

• OpenAI, Three fixed points on the symplectic quadric threefold, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

A symplectic form can be positive on complex lines without being invariant under the almost complex structure. The target asks whether some compatible form nevertheless exists in four dimensions. The pinned manuscript supplies the research context.

Setting

The manifold is smooth, compact, connected, Hausdorff and second countable, modeled on real four-space. The almost complex structure squares to minus the identity.

Formalization target

The selected goal is OAI.TamingCompatibility.taming_implies_compatibility. Its central assertion is

$$(\exists\alpha\text{ symplectic}:\ \alpha(v,Jv)>0\ \forall v\ne0)\ \Longrightarrow\ (\exists\eta\text{ symplectic}:\ \eta(v,Jv)>0\ \forall v\ne0,\ \eta(Ju,Jv)=\eta(u,v)\ \forall u,v).$$

The theorem states that, for a smooth manifold X modeled on four-dimensional Euclidean space ℝ⁴ (charted with smooth transition maps) that is Hausdorff, second countable, compact and connected, and for an almost complex structure J on X, if some symplectic two-form α tames J, then there exists a symplectic two-form η that is compatible with J. Here a two-form assigns to each point x a continuous alternating real bilinear form on the tangent space at x, and an almost complex structure J is a smooth field of continuous linear endomorphisms of the tangent spaces with J(Jv) = −v for every tangent vector v. A two-form is symplectic when it is smooth (its pullbacks along smooth maps from open subsets of ℝ⁴ are smooth), closed (the exterior derivative of each such pullback vanishes), and nondegenerate (a tangent vector v with α(v,w) = 0 for all w must be zero). The form α tames J when α(v, Jv) > 0 for every nonzero tangent vector v at every point. The form η is compatible with J when it tames J and is J-invariant, meaning η(Ju, Jv) = η(u, v) for all tangent vectors u and v at every point. This is a formal statement admitted without proof.

Significance and status

The conclusion supplies a possibly different symplectic form. It does not assert that the original taming form is compatible or prescribe its cohomology class. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

A pointwise compatibility adjustment need not preserve closedness. The conclusion requires both global symplectic structure and positivity.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

• OpenAI, Taming implies compatibility on four-manifolds, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

A symplectic embedding preserves the standard symplectic form $\omega_0=\sum_j dx_j\wedge dy_j$ on $\mathbb C^n$, and in particular preserves volume. Gromov's nonsqueezing and two-ball theorems showed that symplectic embeddings obey constraints invisible to volume (Gromov 1985). The ball-packing problem asks exactly when finitely many balls can be embedded disjointly and symplectically into a given ball, and so measures how far symplectic rigidity goes beyond volume.

In real dimension four the answer involves infinitely many obstructions coming from pseudoholomorphic curves and algebraic geometry (McDuff–Polterovich 1994; Biran 1997). In higher dimensions Siegel and Yao conjectured that only two obstructions survive: volume and Gromov's two-ball obstruction (Conjecture A of Siegel–Yao 2025).

This mission asks for a machine-checked proof of Theorem 1.1 of an OpenAI preprint dated September 23, 2026 (source), which claims Conjecture A in every real dimension $2n\ge6$. The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.

Background

• 1985 — Gromov introduces pseudoholomorphic curves and proves the two-ball obstruction $R_1+R_2\le R$ (Invent. Math. 1985).
• 1994 — McDuff and Polterovich connect packing to blowups and algebraic geometry (Invent. Math. 1994).
• 1995 — Traynor gives explicit packing constructions (J. Differential Geom. 1995).
• 1997–2001 — Biran proves packing stability in dimension four (GAFA 1997; GAFA 2001).
• 2005 — Schlenk's monograph develops folding and planar constructions (de Gruyter 2005).
• 2011–2016 — Buse and Hind extend equal-ball stability to higher dimensions (Geom. Topol. 2011; Compos. Math. 2013); Buse, Hind and Opshtein prove unequal-ball stability in dimension four for small capacities (Trans. AMS 2016).
• 2025 — Siegel and Yao formulate Conjecture A for higher-dimensional packings.
• 2026 — The OpenAI preprint claims Conjecture A for all $n\ge3$ (Theorem 1.1, p. 2).

Setting

For $R>0$ write

$$B^{2n}(R)=\Bigl\{z\in\mathbb C^n:\ \pi\sum_{j=1}^n|z_j|^2\le R\Bigr\},$$

so $R$ is the capacity, the Euclidean radius is $\sqrt{R/\pi}$, and $\mathrm{vol}\,B^{2n}(R)=R^n/n!$. An embedding of a closed ball into the open ball $\operatorname{int}B^{2n}(R)$ means a smooth map defined on an open neighbourhood of the closed ball, which is a topological embedding there, pulls $\omega_0$ back to $\omega_0$, and sends the closed ball into the open target. A packing of $B^{2n}(R_1),\dots,B^{2n}(R_k)$ is a family of such embeddings whose images of the closed balls are pairwise disjoint.

Formalization targets

Milestone: necessity in Theorem 1.1 (p. 4)

If $n\ge3$, $k\ge1$, $R,R_i>0$ and a packing exists, then

$$\sum_{i=1}^kR_i^n<R^n\qquad\text{and}\qquad R_i+R_j<R\ \ (i\ne j).$$

The images lie in some $\operatorname{int}B^{2n}(\sigma)$ with $\sigma<R$ by compactness, so the volume bound and Gromov's two-ball obstruction give the strict inequalities.

Goal: Theorem 1.1 (p. 2)

For integers $n\ge3$, $k\ge1$ and positive reals $R,R_1,\dots,R_k$, a symplectic embedding $\bigsqcup_iB^{2n}(R_i)\hookrightarrow\operatorname{int}B^{2n}(R)$ exists if and only if the two inequalities above hold.

Significance

The result itself. In every real dimension at least six, the volume and two-ball obstructions are the only obstructions to packing balls of arbitrary capacities into a ball. This contrasts with dimension four, where infinitely many further obstructions are essential, and it goes beyond packing-stability results, which concern many small balls. The theorem settles Siegel and Yao's Conjecture A.

Formalizing it. The necessity direction needs Gromov's two-ball theorem, which rests on pseudoholomorphic curve theory and has no formalization. The sufficiency direction uses Hamiltonian flows, Moser isotopies, toric domains, Kähler forms on projective degenerations and normal-cone transfer. A formal proof would require substantial new symplectic and algebro-geometric infrastructure, all of it reusable.

Difficulty

Sufficiency is the hard direction. The volume inequality is an integral condition, but a packing needs pointwise room; in the preprint's toric models over a surface with a handle, the unused-area profile $P$ has positive integral but need not be positive at every moment, and a Hamiltonian comparison theorem (Lemma 2.1, p. 5) is needed to rearrange it into disjoint ball layers (Lemma 3.3, p. 12). The models must then be transferred symplectically into the target ball using Kähler degenerations; three geometric cases arise (all capacities below $R/2$, Proposition 5.2, p. 25; one large capacity in dimension $\ge8$, Proposition 5.3, p. 26; one large capacity in dimension six, Proposition 6.7, p. 39). For necessity the obvious volume argument gives only non-strict inequalities; strictness comes from compactness of the images, and the pairwise bound is genuinely symplectic.

Formalization scope

• Phase space is Fin n → ℂ with capacity $\pi\sum_j|z_j|^2$ and $\omega_0(u,v)=\sum_j(\mathrm{Re}\,u_j\,\mathrm{Im}\,v_j-\mathrm{Im}\,u_j\,\mathrm{Re}\,v_j)$.
• SymplecticOn U f: $U$ open, $f$ is $C^\infty$ on $U$, $f|_U$ is a topological embedding, and fderiv preserves $\omega_0$ at every point of $U$.
• HasPacking n k R r: each closed ball $B^{2n}(r_i)$ lies in an open $U_i$ on which $f_i$ is symplectic, $f_i$ maps the closed ball into the open ball of capacity $R$, and images of distinct closed balls are disjoint.
• PackingInequalities uses strict inequalities and quantifies over ordered pairs $i\ne j$; the goal assumes $n\ge3$, $k\ge1$, $R>0$, $r_i>0$, matching the source exactly.
• Neither side is vacuous: for one ball the pairwise condition is empty and the statement reduces to $r_1<R$.

Selected references

• OpenAI, Symplectic Ball Packings in Higher Dimensions, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Symplectic-Ball-Packings-in-Higher-Dimensions-September-23-2026/paper.pdf
• K. Siegel, Y. Yao, On symplectic packing problems in higher dimensions, Math. Ann. 392 (2025), 5361–5392. https://doi.org/10.1007/s00208-025-03221-7
• M. Gromov, Pseudo holomorphic curves in symplectic manifolds, Invent. Math. 82 (1985), 307–347. https://doi.org/10.1007/BF01388806
• D. McDuff, L. Polterovich, Symplectic packings and algebraic geometry, Invent. Math. 115 (1994), 405–429. https://doi.org/10.1007/BF01231766
• P. Biran, Symplectic packing in dimension 4, Geom. Funct. Anal. 7 (1997), 420–437. https://doi.org/10.1007/s000390050014
• O. Buse, R. Hind, Ellipsoid embeddings and symplectic packing stability, Compos. Math. 149 (2013), 889–902. https://doi.org/10.1112/S0010437X12000826
• O. Buse, R. Hind, E. Opshtein, Packing stability for symplectic 4-manifolds, Trans. Amer. Math. Soc. 368 (2016), 8209–8222. https://doi.org/10.1090/tran/6802
• L. Traynor, Symplectic packing constructions, J. Differential Geom. 41 (1995), 735–751. https://doi.org/10.4310/jdg/1214456483
• F. Schlenk, Embedding Problems in Symplectic Geometry, de Gruyter (2005). https://doi.org/10.1515/9783110199697

Motivation

Place a convex body $K\subset\mathbb R^n$ in the position coordinates and its polar $K^\circ$ in the momentum coordinates of the standard symplectic space $(\mathbb R^n_q\times\mathbb R^n_p,\omega_0)$. The resulting Lagrangian product $K\times K^\circ$ links two problems. Its volume is the Mahler volume product $|K||K^\circ|$, and its symplectic capacities measure how large a round ball can be squeezed into it by a symplectic map. Since symplectic maps preserve volume, a ball of capacity $c$ inside $\operatorname{int}K\times\operatorname{int}K^\circ$ forces $|K||K^\circ|\ge c^n/n!$. Artstein-Avidan, Karasev and Ostrover showed that the Hofer–Zehnder capacity of $K\times K^\circ$ equals $4$ for every origin-symmetric $K$ and connected Viterbo's volume–capacity conjecture to Mahler's conjecture (Duke 2014). Whether actual balls of capacity close to $4$ fit, i.e. whether the Gromov width also equals $4$, was open.

This mission asks for a formal proof that it does, as claimed in an OpenAI preprint dated September 22, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Timeline

• 1939 — Mahler formulates the symmetric volume-product problem (Časopis 1939).
• 1985 — Gromov's nonsqueezing theorem shows that ball embeddings detect symplectic rigidity beyond volume (Invent. Math. 1985).
• 1987 — Bourgain–Milman reverse Santaló inequality (Invent. Math. 1987); Reisner's sharp inequality for unconditional bodies (J. LMS 1987).
• 1994 — Hofer and Zehnder introduce their capacity (book, 1994).
• 2000 — Viterbo proposes the volume–capacity inequality for convex domains (JAMS 2000).
• 2013 — Latschev, McDuff and Schlenk compute Gromov widths of four-dimensional tori with area-preserving constructions (G&T 2013).
• 2014 — Artstein-Avidan, Karasev and Ostrover prove $c_{HZ}(K\times K^\circ)=4$ for symmetric $K$ (Duke 2014).
• 2019–2021 — Ramos and Sepe identify the cube–cross-polytope product with a ball of capacity $4$ (J. Symplectic Geom. 2019); Karasev treats $\ell_p$ balls (Israel J. Math. 2021).
• 2020 — Iriyeh and Shibata prove the three-dimensional symmetric Mahler conjecture (Duke 2020).
• 2024–2026 — Haim-Kislev and Ostrover disprove the general Viterbo conjecture with a non-symmetric four-dimensional example (Annals 2026); Vicente studies functional-dual products and records the width question (arXiv:2505.07572).
• September 2026 — The OpenAI preprint claims Gromov width $4$ for every symmetric polar product, $n\ge2$ (Theorem 1.1, p. 1).

Setting

An origin-symmetric convex body $K\subset\mathbb R^n$ is compact, convex, has nonempty interior, and satisfies $x\in K\iff -x\in K$. Its polar is $K^\circ=\{p:\langle q,p\rangle\le1\ \forall q\in K\}$. On $\mathbb R^n\times\mathbb R^n$ put $\omega_0((q,p),(q',p'))=\langle q,p'\rangle-\langle q',p\rangle$, and let

$$U_K=\operatorname{int}K\times\operatorname{int}K^\circ,\qquad B^{2n}(c)=\{(q,p):\pi(|q|^2+|p|^2)<c\}.$$

A symplectic embedding of an open set $U$ into $V$ is a $C^\infty$ map on $U$ that is a topological embedding, maps $U$ into $V$, and whose derivative preserves $\omega_0$ at every point. The Gromov width $c_G(V)$ is the supremum of capacities $c>0$ for which $B^{2n}(c)$ embeds symplectically into $V$.

Formalization targets

Milestone: the symmetric Mahler inequality (Corollary 5.3, p. 16)

For every $n\ge1$ and origin-symmetric convex body $K\subset\mathbb R^n$, $\ |K|\,|K^\circ|\ge 4^n/n!$.

Goal: Theorem 1.1 (p. 1)

For every $n\ge2$ and every origin-symmetric convex body $K\subset\mathbb R^n$,

$$c_G(U_K)=4,$$

and for every $0<c<4$ there is a symplectic embedding $B^{2n}(c)\hookrightarrow U_K$. No embedding at capacity exactly $4$ is asserted.

Significance

The result itself. It answers the symmetric-polar-product width question with no smoothness, strict convexity or unconditionality assumptions, and through volume preservation it implies the symmetric Mahler inequality in every dimension (Corollary 5.3). For $n\ge3$ it also transports finite ball packings satisfying strict volume and pairwise-capacity conditions into $U_K$ (Corollary 5.5, p. 17). It is specific to symmetric polar products: the general Viterbo conjecture is false.

Formalizing it. Mathlib has smooth manifolds and differential forms but no symplectic capacities, nonsqueezing, or Moser's deformation method. A formal proof would need these, together with a conformal map of the disk with explicit boundary estimates. These components are reusable across symplectic geometry. No machine-checked computation of a Gromov width of a non-trivial domain is known.

Difficulty

The upper bound $c_G\le4$ follows from Gromov nonsqueezing and a supporting-cylinder argument (or from the Hofer–Zehnder computation). The lower bound is the hard direction: knowing $c_{HZ}=4$ does not produce any ball, and explicit embeddings were previously known only for special families ($\ell_p$ balls, the cube). The preprint's route (Sections 2–4) needs balls of capacity close to $\pi k$ from holomorphic maps vanishing to order $k$, and a momentum scale $S_k=(1+o(1))\pi k/4$ that is uniform up to the tips of a conformal lens, where slice heights approach $\pm1$ as $k$ grows; a non-uniform estimate does not suffice.

Formalization scope

• Position and momentum spaces are EuclideanSpace ℝ (Fin n); phase space is their product. polar uses the real inner product; polarProduct K is interior K ×ˢ interior (polar K).
• capacityBall n c is the open ball $\pi(|q|^2+|p|^2)<c$, so a ball of radius $r$ has capacity $\pi r^2$.
• HasSymplecticEmbedding U V: some e with ContDiffOn ℝ ∞ e U, IsEmbedding on the subtype U, MapsTo e U V, and $\omega_0(De\,v,De\,w)=\omega_0(v,w)$ for all $z\in U$.
• gromovWidth is an sSup in ℝ≥0∞ of the admissible capacities, so an unbounded set would give ⊤; the goal asserts the value 4 and separately every capacity below $4$.
• The hypothesis is $n\ge2$, as in the source; the milestone allows $n\ge1$.

Welcome contributions: a Lean notion of symplectic embedding between open subsets of $\mathbb R^{2n}$, Gromov nonsqueezing (as an axiom-free target in its own right), and volume preservation for symplectic maps.

Selected references

• OpenAI, Symplectic Balls in Symmetric Polar Products, OpenAI Math Release preprint, September 22, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Symplectic-Balls-in-Symmetric-Polar-Products-September-22-2026/paper.pdf
• OpenAI, The symmetric Mahler conjecture and its equality cases, OpenAI Math Release preprint, September 22, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-symmetric-Mahler-conjecture-and-its-equality-cases-September-22-2026/paper.pdf
• S. Artstein-Avidan, R. Karasev, Y. Ostrover, From symplectic measurements to the Mahler conjecture, Duke Math. J. (2014). https://doi.org/10.1215/00127094-2794999
• M. Gromov, Pseudo holomorphic curves in symplectic manifolds, Invent. Math. (1985). https://doi.org/10.1007/BF01388806
• C. Viterbo, Metric and isoperimetric problems in symplectic geometry, J. Amer. Math. Soc. (2000). https://doi.org/10.1090/S0894-0347-00-00328-3
• H. Hofer, E. Zehnder, Symplectic Invariants and Hamiltonian Dynamics, Birkhäuser (1994). https://doi.org/10.1007/978-3-0348-8540-9
• P. Haim-Kislev, Y. Ostrover, A counterexample to Viterbo's conjecture, Ann. of Math. (2026). https://doi.org/10.4007/annals.2026.203.2.5
• R. Karasev, Mahler's conjecture for some hyperplane sections, Israel J. Math. (2021). https://doi.org/10.1007/s11856-021-2114-4
• V. G. B. Ramos, D. Sepe, On the rigidity of Lagrangian products, J. Symplectic Geom. (2019). https://doi.org/10.4310/JSG.2019.v17.n5.a7
• J. Latschev, D. McDuff, F. Schlenk, The Gromov width of 4-dimensional tori, Geom. Topol. (2013). https://doi.org/10.2140/gt.2013.17.2813
• J. Moser, On the volume elements on a manifold, Trans. Amer. Math. Soc. (1965). https://doi.org/10.1090/S0002-9947-1965-0182927-5
• K. Mahler, Ein Übertragungsprinzip für konvexe Körper, Časopis Pěst. Mat. Fys. (1939). https://doi.org/10.21136/CPMF.1939.109441

Motivation

A global surface of section reduces a flow on a closed 3-manifold to an area-preserving map of a surface. It is a compact embedded surface whose boundary consists of periodic orbits, whose interior is transverse to the flow, and which every other trajectory hits infinitely often in forward and backward time. Poincaré introduced the idea for the restricted three-body problem. Once a section is a disk, results on area-preserving disk maps (Brouwer, Franks) give periodic orbits and other structure for the whole flow.

For Hamiltonian flows on star-shaped energy surfaces in $\mathbb{R}^4$, equivalently Reeb flows on the tight 3-sphere, it is natural to ask which periodic orbits bound such a disk. Hryniewicz's criterion answers this for dynamically convex flows, with no genericity assumption. The answer is purely topological: a periodic orbit bounds a disk-like global section exactly when it is unknotted with self-linking number $-1$. The criterion is used in celestial mechanics: Joung and van Koert apply it to validated periodic orbits of the restricted three-body problem (arXiv:2407.19159).

Timeline.

• 1998. Hofer, Wysocki and Zehnder prove that every dynamically convex contact form on $S^3$ has some periodic orbit $P_0$, with Conley–Zehnder index $3$, that bounds a disk-like global section. That disk is a page of an open book adapted to the flow. Strictly convex energy surfaces in $\mathbb{R}^4$ are dynamically convex (Ann. of Math. 148).
• 2008/2012. Hryniewicz proves the "unknotted, self-linking $-1$" characterization in the non-degenerate case (arXiv:0812.4076).
• 2010/2011. Hryniewicz and Salomão treat non-degenerate tight contact forms on $S^3$. Two extra conditions appear there: $\mu_{CZ}\ge 3$, and linking with every orbit of index $2$ (arXiv:1006.0049).
• 2011/2014. Hryniewicz removes non-degeneracy for dynamically convex forms (arXiv:1105.2077, Theorem 1.7). In the same paper, Theorem 1.8 shows that any orbit coming from a fixed point of the first-return map of a disk-like section is again such a binding.
• 2012. Albers, Fish, Frauenfelder, Hofer and van Koert use this circle of ideas to get disk-like sections in the planar circular restricted three-body problem (arXiv:1103.3881).

Setting

Use coordinates $x=(q_1,p_1,q_2,p_2)$ on $\mathbb{R}^4$, the Liouville form $\lambda_0=\tfrac12\sum_j (q_j\,dp_j-p_j\,dq_j)$ and the symplectic form $\omega_0=d\lambda_0=\sum_j dq_j\wedge dp_j$.

Let $H:\mathbb{R}^4\to\mathbb{R}$ be smooth and set $S=H^{-1}(1)$. Assume that every ray from the origin meets $S$ exactly once, and that it crosses $S$ transversally:

$$dH(x)\,x>0\qquad(x\in S).$$

Then $S$ is a strictly star-shaped hypersurface diffeomorphic to $S^3$. Every contact form on $S^3$ that matters below arises this way, up to diffeomorphism (see Formalization scope).

The Hamiltonian vector field $X_H$ is defined by $\iota_{X_H}\omega_0=-dH$. With this sign, $\lambda_0(X_H)=\tfrac12\,dH(x)\,x>0$ on $S$. So $X_H|_S$ is a positive multiple of the Reeb vector field of the contact form $\lambda_0|_S$, and its orbits are the Reeb orbits reparametrized. A periodic orbit $P=(x,T)$ is a solution with $x(T)=x(0)$ and $T>0$. It is prime when $T$ is its least positive period. The contact structure is $\xi=\ker\lambda_0|_S$.

• Conley–Zehnder index. Fix the global frame of $\xi$ given by the quaternionic rotations of $\nabla H$. Along $P$, the linearized flow restricted to $\xi$ is a path $\varphi:[0,1]\to Sp(1)$ with $\varphi(0)=I$. The winding interval $I(\varphi)$ collects the total rotations of all nonzero vectors, measured in turns. Then $\mu_{CZ}(P)$ is the lower semicontinuous index of Hryniewicz's §2.1.1. In particular,

$$\mu_{CZ}(P)\ge 3 \iff \min I(\varphi)>1,$$

that is, every nonzero transverse vector turns by more than one full turn.

• Dynamical convexity. The flow is dynamically convex if $\mu_{CZ}(P)\ge 3$ for every periodic orbit $P$ in $S$, prime or multiply covered.
• Disk-like global surface of section. A smoothly embedded closed disk $D\subset S$ such that $\partial D=x(\mathbb{R})$ for a periodic orbit $P$, $X_H$ is transverse to $D\setminus\partial D$, and every trajectory not contained in $\partial D$ meets $D$ at arbitrarily large positive and negative times. Then $P$ bounds $D$.
• Unknotted. $P$ is unknotted if $x(\mathbb{R})$ is the boundary of some smoothly embedded closed disk in $S$.
• Self-linking number. Push $x$ off itself along the global frame of $\xi$ to a disjoint loop $x'$. Then

$$\operatorname{sl}(P)=\operatorname{lk}(x,x')\in\mathbb{Z},$$

the linking number in $S\cong S^3$, with $S$ oriented as the boundary of the star-shaped domain it bounds. This agrees with Hryniewicz's Definition 1.5, which uses a section of $\xi$ over a spanning disk.

Formalization targets

Goal: Hryniewicz's criterion (Theorem 1.7, first sentence)

For every dynamically convex strictly star-shaped $S$ and every prime periodic orbit $\bar P$:

$$\bar P \text{ bounds a disk-like global surface of section} \iff \bar P \text{ is unknotted and } \operatorname{sl}(\bar P)=-1.$$

The statement fixes no constants and no non-degeneracy, and it covers every dynamically convex star-shaped surface.

Stronger: adapted open book (Theorem 1.7, second sentence)

If $\bar P$ is unknotted with $\operatorname{sl}(\bar P)=-1$, then $S\setminus \bar x(\mathbb{R})$ fibres smoothly over $\mathbb{R}/\mathbb{Z}$. Every fibre is the interior of a disk-like global surface of section whose oriented boundary is $\bar P$.

Further: new bindings from fixed points (Theorem 1.8)

Let $D_0$ be any disk-like global section. Every periodic orbit through a fixed point of the first-return map of $D_0\setminus\partial D_0$ is unknotted, has self-linking number $-1$, and so bounds the page of an adapted open book.

Significance

The result. The criterion turns a dynamical question into a topological check. It does not depend on whether the orbit is degenerate, and degenerate orbits are what one meets at bifurcations and on symmetric levels. Every periodic orbit in a strictly convex energy surface that is unknotted with $\operatorname{sl}=-1$ is a binding, so the flow is organised by many open books at once. Theorem 1.8 makes this concrete: the Hamiltonian flow twists around two different bindings, $\partial D_0$ and $\partial D_1$. In applications, numerically validated orbits become analytic global sections without a separate non-degeneracy check (Joung–van Koert, Theorems 1.2 and 1.5).

Formalizing it. The theorem is proved, in a 50-page paper that relies on Hofer–Wysocki–Zehnder's theory of pseudo-holomorphic curves in symplectizations. It has no machine-checked proof. Mathlib has no Conley–Zehnder index, no self-linking number, no linking number of curves in $S^3$, and no global surfaces of section. A Lean statement fixes every sign and orientation convention involved: the sign of $X_H$, the orientation of $S$, which push-off defines $\operatorname{sl}$, and the index of degenerate orbits. Each of these is easy to get wrong in prose. Formal proofs of the parts that use no holomorphic curves are valuable on their own: the necessity direction, the description of the index by winding intervals, and the explicit ellipsoid examples.

Difficulty

The obvious route is to approximate the contact form by non-degenerate forms $\lambda_k\to\lambda$ that keep $\bar P$ as an orbit, and then apply the non-degenerate theorems. This fails. The $\lambda_k$ need not be dynamically convex. They can have orbits of very high action with $\mu_{CZ}=2$ that are not linked with $\bar P$, so the Hryniewicz–Salomão criterion does not apply to $\lambda_k$ (Hryniewicz, p. 4). The families of planes that would give the pages for $\lambda_k$ have to be controlled directly as $k\to\infty$, and this is not a formal limit argument.

A second obstruction is genuinely global. A disk spanning $\bar P$ and transverse to the flow in its interior is easy to produce when $\operatorname{sl}(\bar P)=-1$. Showing that every trajectory returns to it is the whole content of the theorem, and no local or perturbative argument gives it.

For the formalization, nothing in the proof of sufficiency avoids finite-energy pseudo-holomorphic planes: Fredholm theory, asymptotic analysis, bubbling-off and compactness all enter. None of this exists in Lean.

Formalization scope

• Ambient space. $\mathbb{R}^4$ is Fin 4 → ℝ with coordinates ordered $(q_1,p_1,q_2,p_2)$. $\lambda_0$, $\omega_0$ and $X_H$ are defined explicitly, with the sign conventions above.
• Energy surfaces. Star-shaped surfaces are smooth (ContDiff ℝ ⊤) functions $H$ with the ray condition and $dH(x)x>0$ on $H^{-1}(1)$. The Reeb flow of a general dynamically convex form on $S^3$ reduces to this case, up to diffeomorphism and positive time change: such a form is tight (Hofer–Wysocki–Zehnder), and every tight form on $S^3$ comes from a star-shaped hypersurface (Eliashberg 1992). That reduction is not part of the targets. Hryniewicz makes the same reduction (§3, first paragraph).
• Flow. The flow is the flow of $X_H$, not of the Reeb field. All notions in the targets are invariant under positive time change. Periodic orbits are solutions of $\dot x=X_H(x)$ on all of $\mathbb{R}$. "Prime" means the recorded period is least.
• Index. $\mu_{CZ}\ge 3$ is encoded by the winding-interval condition in the global quaternionic frame, with degenerate orbits included. Multiply covered orbits are included in dynamical convexity.
• Disks. Disks are smooth embeddings of the closed unit disk (injective, with injective differential up to the boundary). The return condition demands hits at arbitrarily large positive and negative times.
• Ruling out vacuous encodings. A version without the two-sided return condition, with a dynamical-convexity predicate that no surface satisfies, or with $\operatorname{sl}$ that is not a linking number of the push-off, proves a different theorem. The ellipsoid milestone below is a non-vacuity check on the definitions.
• Infrastructure. A complete development needs the following.
  • Reusable beyond this mission: the Conley–Zehnder index of paths in $Sp(1)$, the linking number of disjoint loops in $S^3$ (or in $\mathbb{R}^3$ after stereographic projection), and global flows of vector fields on compact level sets.
  • Specific to this proof: contact topology of spanning disks (characteristic foliations, elimination of singularities), and finite-energy planes in $\mathbb{R}\times S^3$ with their Fredholm, asymptotic and compactness theory.
• Contributions welcome. The definition layer, the index and linking-number libraries, the ellipsoid examples, Lemma 2.1, the necessity direction, Lemma 3.12, and any sub-step of the holomorphic-curve argument stated as an independent lemma.

Selected references

• H. Hofer, K. Wysocki, E. Zehnder, The dynamics on three-dimensional strictly convex energy surfaces, Ann. of Math. 148 (1998), 197–289. https://doi.org/10.2307/120994
• U. L. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. Amer. Math. Soc. 364 (2012), 1859–1931. https://arxiv.org/abs/0812.4076
• U. L. Hryniewicz, P. A. S. Salomão, On the existence of disk-like global sections for Reeb flows on the tight 3-sphere, Duke Math. J. 160 (2011), 415–465. https://arxiv.org/abs/1006.0049
• U. L. Hryniewicz, Systems of global surfaces of section for dynamically convex Reeb flows on the 3-sphere, J. Symplectic Geom. 12 (2014), 791–862. https://arxiv.org/abs/1105.2077
• U. L. Hryniewicz, P. A. S. Salomão, Global surfaces of section for Reeb flows in dimension three and beyond, Proc. ICM 2018 (extended version). https://arxiv.org/abs/1712.01925
• P. Albers, J. W. Fish, U. Frauenfelder, H. Hofer, O. van Koert, Global surfaces of section in the planar restricted 3-body problem, Arch. Ration. Mech. Anal. 204 (2012), 273–284. https://arxiv.org/abs/1103.3881
• C. Joung, O. van Koert, Computational symplectic topology and symmetric orbits in the restricted three-body problem, Nonlinearity 38 (2025), 025015. https://arxiv.org/abs/2407.19159
• Y. Eliashberg, Contact 3-manifolds twenty years since J. Martinet's work, Ann. Inst. Fourier 42 (1992), 165–192. https://doi.org/10.5802/aif.1288