Motivation

A finite-energy pseudoholomorphic plane in the symplectization of a contact $3$-manifold approaches, at its puncture, a periodic Reeb orbit $P$, and the previous mission of this series identifies the leading term of the approach: an eigenvector of the asymptotic operator $A_P$. In dimension three this eigenvector is a nowhere-vanishing section of the contact plane bundle $\xi$ along $P$, so it has a winding number. H. Hofer, K. Wysocki and E. Zehnder (GAFA 5, 1995) introduced the winding invariants $\mathrm{wind}_\infty$ (the winding of the curve at its punctures) and $\mathrm{wind}_\pi$ (the number of zeros of the transverse derivative $\pi\,du$), related them to the Conley–Zehnder index of the asymptotic orbits, and used them to single out the fast planes, which project to immersions transverse to the Reeb flow. These invariants are the basic tool in the theory of global surfaces of section of dynamically convex Reeb flows: U. Hryniewicz's characterization of the Reeb orbits that bound disk-like global surfaces of section (arXiv:1105.2077, arXiv:0812.4076) rests on them.

This mission formalizes these invariants and their main properties for finite-energy curves in the symplectization of a strictly star-shaped hypersurface $S\subset\mathbb{R}^4$, following Hryniewicz, Systems of global surfaces of section for dynamically convex Reeb flows on the 3-sphere, § 2.2.4, Hryniewicz, Fast finite-energy planes in symplectizations and applications, §§ 3–4, and C. Wendl, Lectures on Symplectic Field Theory (2026 notes), § 3.7. It is the ninth mission in a series on symplectic field theory.

Setting

All objects are those of FiniteEnergyPlane_Setting and FiniteEnergyPlane_Asymptotics with $n=1$: a strictly star-shaped level $S=H^{-1}(1)\subset\mathbb{R}^4$ with Reeb field $R$ and contact planes $\xi$, a compatible complex structure $J$ on $\xi$, finite-energy $\tilde J$-holomorphic curves, nondegenerate punctures (Hryniewicz, Definition 2.9), the asymptotic operator $A_P$ and asymptotic eigenvectors.

• Global frame. $\xi$ is trivialized over $S$ by Hryniewicz's quaternionic frame $Z_1,Z_2$ with $\omega_0(Z_1,Z_2)=1$; $v=aZ_1+bZ_2$ has coordinate $a+ib$. All windings are measured in this frame.
• Eigenvector windings. For a loop $S_\infty$ of symmetric $2\times2$ matrices, eigenvalues of $-J_0\partial_t-S_\infty$ carry the winding number of their eigenfunctions; likewise for $A_P$. $\alpha^-(P)$ is the largest winding of a negative eigenvalue and $\alpha^+(P)$ the smallest winding of a nonnegative one; $p=\alpha^+-\alpha^-$ is the parity.
• Conley–Zehnder index. $\mu_{CZ}(P)$ is Hryniewicz's index of the linearized flow on $\xi$ in the global frame (HryniewiczCriterion.czIndexOfPath). One milestone compares it with the index of the first mission of this series.
• $\mathrm{wind}_\pi$ and $\mathrm{wind}_\infty$. For a curve $u$ on $\mathbb{C}\setminus\Gamma$, $\mathrm{wind}_\pi(u)$ is the sum of the local indices of the zeros of $\pi\partial_su$ (Hryniewicz (14)), and $\mathrm{wind}_\infty$ at a puncture of sign $\varepsilon$ is the winding of $t\mapsto\pi\partial_su(s,\varepsilon t)$ for large $s$ in cylindrical coordinates (Hryniewicz (16)).
• Fast planes (Hryniewicz, Definition 2.14): finite-energy planes with a nondegenerate puncture at $\infty$ over a prime orbit and $\mathrm{wind}_\pi=0$.

Formalization targets

Goal: winding bounds for finite-energy planes

Let $u$ be a finite-energy $\tilde J$-holomorphic plane whose puncture $\infty$ is nondegenerate, with a nondegenerate asymptotic limit $P$. Then

$$\mathrm{wind}_\pi(u)=\mathrm{wind}_\infty(u)-1\qquad\text{and}\qquad1\le\mathrm{wind}_\infty(u)\le\Big\lfloor\frac{\mu_{CZ}(P)}{2}\Big\rfloor.$$

The orbit is related to the periodic orbits of the HryniewiczCriterion setting by image and action, so the bound is stated in that setting's Conley–Zehnder index.

Milestones

1. Nonvanishing and winding. Eigenfunctions of $-J_0\partial_t-S_\infty$ on $\mathbb{R}^2$ have no zeros, and all eigenfunctions of one eigenvalue have the same winding (Wendl, Theorem 3.7.1).
2. Monotonicity. The winding is a nondecreasing function of the eigenvalue.
3. Multiplicity two. For every $k\in\mathbb{Z}$, the eigenfunctions with winding $k$ span a space of dimension exactly $2$.
4. Unitary frames. Along every orbit some unitary frame of $\xi$ measures windings as the global frame does (Hryniewicz, Remark 2.6).
5. Conley–Zehnder index. For nondegenerate paths in $\mathrm{Sp}(2)$, the index of the first mission of this series equals Hryniewicz's winding-interval index.
6. $\mu_{CZ}=2\alpha^-+p$ for nondegenerate orbits, with $p\in\{0,1\}$ (Hofer–Wysocki–Zehnder, Theorem 3.10).
7. Index at least 3. If $\mu_{CZ}(P)\ge3$, every eigenvalue $\mu\ge0$ of $A_P$ has winding at least $2$ (Hryniewicz 2012, Lemma 4.5).
8. $\mathrm{wind}_\pi\ge0$. For curves on $\mathbb{C}\setminus\Gamma$ with nondegenerate punctures and $\pi\,du\not\equiv0$, the zeros of $\pi\,du$ are finitely many, each of positive local index.
9. $\mathrm{wind}_\infty$ and eigenvectors. At a puncture with an asymptotic eigenvector $v$, $\mathrm{wind}_\infty$ equals the winding of $v$ (Hryniewicz, Lemma 2.16, Remark 2.17).
10. Bounds by $\alpha^\pm$. At a nondegenerate puncture of sign $\varepsilon$, $\mathrm{wind}_\infty$ is the winding of an eigenvalue $\mu$ with $\varepsilon\mu<0$; so $\mathrm{wind}_\infty\le\alpha^-$ at positive and $\mathrm{wind}_\infty\ge\alpha^+$ at negative punctures.
11. $\mathrm{wind}_\pi=\mathrm{wind}_\infty-\chi+\#\Gamma$ for curves on $\mathbb{C}\setminus\Gamma$ with a positive puncture at $\infty$ and negative punctures in $\Gamma$ (Hryniewicz, Lemma 2.15).
12. Planes: $\mathrm{wind}_\infty\ge1$ (Hryniewicz 2012, Remark 3.20).
13. Fast planes. Over a prime orbit, a plane is fast if and only if $\mathrm{wind}_\infty=1$.
14. Transversality. The projection of a fast plane to $S$ is an immersion transverse to the Reeb field.

Significance

The results. The goal bounds the winding of a finite-energy plane in terms of the Conley–Zehnder index of its asymptotic orbit; together with milestones 7 and 13 it gives the characterization of fast planes that underlies the existence of disk-like global surfaces of section for dynamically convex Reeb flows on $S^3$ (Hofer–Wysocki–Zehnder 1998, Hryniewicz 2012 and 2014). Milestone 11 is stated for punctured spheres with negative punctures, the form that appears in the compactness theory of families of fast planes. Milestones 1–3 are results about $2\times2$ symmetric loops, independent of the geometry, and milestone 5 connects Hryniewicz's index with the axiomatic Conley–Zehnder index of the first mission.

Formalizing them. All results are classical and proved in the cited sources. None of them has been formalized in Lean or another interactive theorem prover, as far as a literature search shows; Mathlib has no winding numbers of sections of plane bundles and no asymptotic operators.

Difficulty

The invariants mix analysis and topology: $\mathrm{wind}_\pi$ counts zeros of a section that is not holomorphic, only of Cauchy–Riemann type, and $\mathrm{wind}_\infty$ is a winding of a derivative in cylindrical coordinates, which is only defined after the asymptotic description of the end. Windings are measured in a global frame that is not unitary for $J$, so every statement about eigenvectors must be read through a change of frame. The eigenvalue results concern an operator on loops whose spectrum is infinite in both directions, with each winding number shared by exactly two dimensions of eigenfunctions. Two different definitions of the Conley–Zehnder index, one defined from windings of a path and the other from a determinant map, have to be matched with consistent orientations.

Formalization scope

• Namespace FiniteEnergyPlane; the definition module FiniteEnergyPlane_Winding imports FiniteEnergyPlane_Asymptotics (previous mission) and HryniewiczCriterion_ConleyZehnder. The bridge milestone also imports ConleyZehnder_Setting (first mission).
• Dimension three only ($n=1$, $S\subset\mathbb{R}^4$); V 1 and HryniewiczCriterion.R4 are identified coordinatewise.
• Invariants are predicates "defined and equal to $k$"; nothing is a total function with a default value.
• Punctures in $\mathbb{C}$ use the coordinates $z_0+e^{-2\pi(s+it)}$, the puncture $\infty$ uses $e^{2\pi(s+it)}$.
• Not included. Embeddedness of fast planes, intersection theory of punctured curves, compactness of families of fast planes and the open book decomposition are left to later missions.

Contributions welcome: general lemmas on winding numbers of loops in $\mathbb{C}\setminus\{0\}$ and on zeros of functions satisfying Cauchy–Riemann type equations.

Selected references

• U. Hryniewicz, Systems of global surfaces of section for dynamically convex Reeb flows on the 3-sphere, J. Symplectic Geom. 12 (2014), § 2.2.4. https://arxiv.org/abs/1105.2077
• U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. Amer. Math. Soc. 364 (2012), 1859–1931, §§ 3–4. https://arxiv.org/abs/0812.4076
• H. Hofer, K. Wysocki, E. Zehnder, Properties of pseudoholomorphic curves in symplectisations II: Embedding controls and algebraic invariants, Geom. Funct. Anal. 5 (1995), 270–328, § 3.
• H. Hofer, K. Wysocki, E. Zehnder, The dynamics on three-dimensional strictly convex energy surfaces, Ann. of Math. 148 (1998), 197–289.
• C. Wendl, Lectures on Symplectic Field Theory, lecture notes, Humboldt-Universität zu Berlin (2026 version), § 3.7; earlier version arXiv:1612.01009. https://arxiv.org/abs/1612.01009
• J. Gutt, Generalized Conley–Zehnder index, Ann. Fac. Sci. Toulouse Math. 23 (2014), § 2. https://arxiv.org/abs/1307.7239