Eigenfunctions of asymptotic operators on $\mathbb{R}^2$ have no zeros and a common winding

Proved

FiniteEnergyPlane.isLoopEigen_ne_zero_hasLoopEigenWind

by Mazecto · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

conley-zehnder-indexpseudoholomorphic-curvesreeb-dynamicssymplectic-geometrysymplectizationwinding-numbers

Let $S_\infty:\mathbb{R}\to\mathbb{R}^{2\times2}$ be a $C^\infty$ $1$ -periodic loop of symmetric matrices and $A=-J_0\partial_t-S_\infty$ on $1$ -periodic loops in $\mathbb{R}^2=\mathbb{C}$ . Every eigenfunction $e$ of $A$ vanishes nowhere, and all eigenfunctions of the same eigenvalue $\mu$ have the same winding number.

Formalization Note Eigenfunctions are IsLoopEigen Sinf μ e of FiniteEnergyPlane_Asymptotics with n = 1; the common winding is HasLoopEigenWind Sinf μ k for some k.

Preamble

import Definitions.Def_FiniteEnergyPlane_Winding

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- Wendl, Theorem 3.7.1 (1)–(2), after Hofer–Wysocki–Zehnder: for a smooth loop `S∞` of symmetric
`2 × 2` matrices, every eigenfunction of `A = -J₀ ∂ₜ - S∞` vanishes nowhere, and all eigenfunctions
of one eigenvalue have the same winding number. -/
theorem isLoopEigen_ne_zero_hasLoopEigenWind (Sinf : ℝ → CauchyRiemannIndex.Mat 1) (hSinf : CauchyRiemannIndex.IsSymLoop Sinf)
    (hSinf' : ∀ i j, ContDiff ℝ ∞ (fun t => Sinf t i j)) (μ : ℝ)
    (e : ℝ → CauchyRiemannIndex.Vec 1) (he : IsLoopEigen Sinf μ e) :
    (∀ t : ℝ, e t ≠ 0) ∧ ∃ k : ℤ, HasLoopEigenWind Sinf μ k := by
  sorry

end FiniteEnergyPlane

Source

C. Wendl, Lectures on Symplectic Field Theory, lecture notes, Humboldt-Universität zu Berlin (2026 version); earlier version arXiv:1612.01009, Theorem 3.7.1 (1), (2); 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, Section 3

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Theorem `FiniteEnergyPlane.isLoopEigen_ne_zero_hasLoopEigenWind`

Let $S_\infty : \mathbb{R} \to \mathbb{R}^{2\times 2}$ be a loop of real $2\times 2$ matrices (rows and columns indexed by two symbols "left", "right") such that $S_\infty$ is continuous, $1$ -periodic, each $S_\infty(t)$ is symmetric, and every entry $t \mapsto S_\infty(t)_{ij}$ is $C^\infty$ . Let $\mu \in \mathbb{R}$ , and let $e : \mathbb{R} \to \mathbb{R}^2$ be a loop eigenfunction for $(S_\infty, \mu)$ , meaning: $e$ is $C^\infty$ , $1$ -periodic, $e(t_0) \ne 0$ for at least one $t_0$ , and

-J_0\, e'(t) - S_\infty(t)\, e(t) = \mu\, e(t) \quad \text{for all } t \in \mathbb{R}, \qquad J_0 = \begin{pmatrix} 0 & -1 \\ 1 & 0 \end{pmatrix}

( $J_0$ sends $(a_L, a_R)$ to $(-a_R, a_L)$ ).

Then both of the following hold:

$e(t) \ne 0$ for every $t \in \mathbb{R}$ ;
there is an integer $k$ such that $\mathrm{HasLoopEigenWind}(S_\infty, \mu, k)$ holds, i.e. ( $\mu$ has a loop eigenfunction, and) every loop eigenfunction $\tilde e$ for $(S_\infty, \mu)$ has winding number $k$ in the following sense: the complex loop $f(t) = \tilde e_L(t) + i\,\tilde e_R(t)$ is continuous, $1$ -periodic, nowhere zero, and admits a continuous $\theta : \mathbb{R} \to \mathbb{R}$ with $f(t) = |f(t)|e^{i\theta(t)}$ for all $t$ and $\theta(1) - \theta(0) = 2\pi k$ .

So the second conclusion asserts that the winding number is the same integer $k$ for all eigenfunctions of the eigenvalue $\mu$ , not just for the given $e$ . The hypothesis that $e$ exists is a genuine assumption; if $\mu$ admits no loop eigenfunction the statement is vacuous.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Mazecto · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Eigenfunctions of asymptotic operators on R2\mathbb{R}^2R2 have no zeros and a common winding

Theorem FiniteEnergyPlane.isLoopEigen_ne_zero_hasLoopEigenWind

Eigenfunctions of asymptotic operators on $\mathbb{R}^2$ have no zeros and a common winding

Theorem `FiniteEnergyPlane.isLoopEigen_ne_zero_hasLoopEigenWind`