Symplectic Geometry

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

Motivation

A contact structure on a manifold of odd dimension $2k+1$ is a field of hyperplanes $\xi=\ker\alpha$ that is as far from integrable as possible. Contact structures are the odd-dimensional counterpart of symplectic forms. They arise on every star-shaped energy level of a Hamiltonian system, on unit cotangent bundles (geodesic flows), and on links of singularities. They are the setting of Reeb dynamics and of the Weinstein conjecture.

Gray's stability theorem says that on a closed manifold contact structures have no local moduli. If $\xi_t$, $t\in[0,1]$, is a smooth family of contact structures, there is an isotopy $\psi_t$ with $T\psi_t(\xi_0)=\xi_t$. A contact structure can therefore be deformed only within its isotopy class, and every classification of contact structures (tight versus overtwisted, Eliashberg's classification on $S^3$) is a classification up to isotopy because of it.

Timeline.

• 1959. Gray proves stability with deformation theory in the style of Kodaira–Spencer (Ann. of Math. 69).
• 1965. Moser proves the analogous stability for volume forms by integrating a time-dependent vector field, now called the Moser trick (Trans. AMS 120).
• Later. The Moser trick becomes the standard proof of Gray's theorem. Geiges' survey gives a short complete proof (arXiv:math/0307242, Theorem 2.20), which is the source of this mission. Its remarks record the limits of the statement: contact forms are not stable (Remark 2.21(1)), and on the open manifold $S^1\times\mathbb{R}^2$ stability fails (Remark 2.21(2), after Eliashberg).

Setting

The closed manifold is a compact submanifold of Euclidean space. Let $F:\mathbb{R}^n\to\mathbb{R}^c$ be smooth, let $M=F^{-1}(0)$ be compact, and assume $DF(y)$ is surjective for every $y\in M$. Then $M$ is a closed smooth manifold of dimension $n-c$ with tangent spaces

$$T_yM=\ker DF(y).$$

A one-form is a smooth map $\alpha:\mathbb{R}^n\to(\mathbb{R}^n)^*$, restricted to $TM$. Its exterior derivative is

$$d\alpha_y(u,v)=D\alpha_y(u)(v)-D\alpha_y(v)(u).$$

• Contact form. $\alpha$ is a contact form on $M$ if at every $y\in M$ the covector $\alpha_y$ is nonzero on $T_yM$ and $d\alpha_y$ is non-degenerate on the hyperplane

$$\xi_y=T_yM\cap\ker\alpha_y.$$

This is the condition $\alpha\wedge(d\alpha)^k\neq0$ in the form of Geiges' Remark 2.3. It forces $\dim M$ to be odd. The contact structure is $\xi=\ker\alpha$. Contact structures are cooriented throughout, as in Geiges' standing assumption (§2).

• Smooth family. A family $\alpha_t$ is smooth if $(t,y)\mapsto\alpha_t(y)$ is smooth. It is a family of contact forms if each $\alpha_t$, $t\in[0,1]$, is a contact form on $M$.
• Isotopy. An isotopy of $M$ is a smooth map $(t,y)\mapsto\psi_t(y)$ with $\psi_0=\mathrm{id}$ on $M$, such that each $\psi_t$, $t\in[0,1]$, maps $M$ bijectively onto $M$ with injective differential on $TM$, i.e. is a diffeomorphism of $M$.
• Pull-back. $(\psi_t^*\alpha)_y(v)=\alpha_{\psi_t(y)}(D\psi_t(y)\,v)$.

Formalization targets

Goal: Gray stability (Theorem 2.20)

For every smooth family of contact forms $\alpha_t$, $t\in[0,1]$, on $M$ there is an isotopy $\psi_t$ of $M$ with

$$T\psi_t(\xi_0)=\xi_t\qquad(t\in[0,1]),\qquad\xi_t=\ker\alpha_t,$$

stated pointwise: for $v\in T_yM$, $\alpha_0(v)=0$ iff $\alpha_t(D\psi_t(y)v)=0$.

The goal concerns the contact structures. It fixes no normalization of the forms and no dimension.

Stronger: conformal form

The same isotopy can be chosen with smooth functions $\lambda_t>0$ such that

$$\psi_t^*\alpha_t=\lambda_t\,\alpha_0\quad\text{on }TM.$$

Stronger: stationary points (Remark 2.21(3))

Moreover, every point $p\in M$ at which $\dot\alpha_t$ vanishes on $T_pM$ for all $t$ stays fixed: $\psi_t(p)=p$.

Significance

The result. Gray stability is the basic rigidity statement of contact topology.

• It reduces the classification of contact structures to isotopy classes, so invariants of a contact manifold are constant along deformations.
• It is the first step of many local normal forms: Darboux's theorem and the neighbourhood theorems for Legendrian and transverse submanifolds are proved by applying it, or its proof, near a submanifold (Geiges §2.4–2.5).
• In Hamiltonian dynamics it identifies the contact structures of a continuous family of star-shaped energy levels. Topological invariants of transverse periodic orbits, such as the self-linking number, are then constant along the family.

Formalizing it. The theorem is classical and has a short proof on paper. Mathlib, at the revision used here, has no differential forms on manifolds, no Lie derivative, no global flows of time-dependent vector fields on compact submanifolds, and no contact structures. The mission builds these concretely on submanifolds of $\mathbb{R}^n$:

• one-forms, their exterior derivative and pull-back;
• the derivative of a pulled-back family along a flow (Lemma 2.19);
• the pointwise linear algebra of a contact form: the Reeb vector, and the unique solution of the Moser equation;
• global flows of smooth time-dependent vector fields tangent to a compact submanifold.

All of these are reusable for Moser's theorem on volume and symplectic forms and for the Darboux and neighbourhood theorems.

Difficulty

The proof is soft, but two steps are not formal.

1. Solving for the vector field. Writing $\psi_t$ as the flow of $X_t$, the equation $\psi_t^*\alpha_t=\lambda_t\alpha_0$ becomes

$$\dot\alpha_t+i_{X_t}d\alpha_t=\mu_t\alpha_t,\qquad X_t\in\xi_t.$$

It has a unique solution at each point, but only because $d\alpha_t$ is non-degenerate on $\xi_t$ and the Reeb vector spans the kernel of $d\alpha_t|_{TM}$. The solution must also depend smoothly on $(t,y)$ and be tangent to $M$; the ambient form $\alpha_t$ is in general not contact off $M$. 2. Integrating it. The isotopy is the flow of $X_t$, which must exist for all $t\in[0,1]$ and stay on $M$. Compactness of $M$ enters exactly here. On open manifolds the statement is false (Remark 2.21(2)).

The tempting shortcut of asking for $\psi_t^*\alpha_t=\alpha_0$ does not work. Contact forms themselves are not stable, as the Hopf family on $S^3$ shows (Remark 2.21(1)), and the conformal factor $\lambda_t$ cannot be dropped.

Formalization scope

• Representation.
  • $\mathbb{R}^n$ is Fin n → ℝ; $M$ is a compact regular level set $F^{-1}(0)$ of a smooth $F:\mathbb{R}^n\to\mathbb{R}^c$.
  • One-forms are maps $\mathbb{R}^n\to(\mathbb{R}^n\to_L\mathbb{R})$, smooth families are jointly smooth in $(t,y)$ on $\mathbb{R}\times\mathbb{R}^n$, and $d\alpha$ is the antisymmetrized derivative.
  • An isotopy is a jointly smooth $\psi:\mathbb{R}\times\mathbb{R}^n\to\mathbb{R}^n$ that restricts, for $t\in[0,1]$, to diffeomorphisms of $M$.
• Committed conventions.
  • Contact structures are cooriented, i.e. given by global contact forms.
  • The contact condition is the non-degeneracy of $d\alpha$ on $\xi$ (Remark 2.3), not a wedge power.
  • Only the restrictions to $TM$ and the values for $t\in[0,1]$ matter.
• Scope relative to the source. Every closed manifold embeds in some $\mathbb{R}^n$, but not every closed manifold is a regular level set, since that requires a trivial normal bundle. The targets cover regular level sets, including all spheres and all star-shaped energy levels. The abstract version on any closed manifold is outside the targets until Mathlib has differential forms on manifolds.
• Ruling out vacuous encodings. The isotopy must start at the identity on $M$, map $M$ onto $M$ for every $t\in[0,1]$, and be a diffeomorphism there. Dropping any of these makes the goal trivial; for instance, the constant isotopy satisfies the goal whenever all $\xi_t$ agree. The Hopf family milestone checks that the contact condition is satisfiable and that the conformal factor is necessary.
• Contributions welcome. The linear-algebra milestones (Reeb vector, Moser equation), Lemma 2.19, global flows on compact level sets, and the Hopf-family example. Moser's theorem for volume forms would be a natural sibling result built on the same infrastructure.

Selected references

• J. W. Gray, Some global properties of contact structures, Ann. of Math. 69 (1959), 421–450. https://doi.org/10.2307/1970192
• H. Geiges, Contact geometry, in Handbook of Differential Geometry, Vol. II, Elsevier (2006), 315–382; §2.2, Lemma 2.19, Theorem 2.20, Remark 2.21. https://arxiv.org/abs/math/0307242
• H. Geiges, An Introduction to Contact Topology, Cambridge Stud. Adv. Math. 109, Cambridge Univ. Press (2008), §2.2. https://doi.org/10.1017/CBO9780511611438
• J. Moser, On the volume elements on a manifold, Trans. Amer. Math. Soc. 120 (1965), 286–294. https://doi.org/10.1090/S0002-9947-1965-0182927-5
• 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