The winding of eigenfunctions is monotone in the eigenvalue

Proved

FiniteEnergyPlane.hasLoopEigenWind_mono

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}$ . If $\mu_1<\mu_2$ are eigenvalues of $A$ with windings $k_1$ and $k_2$ , then $k_1\le k_2$ .

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 (3): the winding number of the eigenfunctions of `A = -J₀ ∂ₜ - S∞` is a
nondecreasing function of the eigenvalue. -/
theorem hasLoopEigenWind_mono (Sinf : ℝ → CauchyRiemannIndex.Mat 1) (hSinf : CauchyRiemannIndex.IsSymLoop Sinf)
    (hSinf' : ∀ i j, ContDiff ℝ ∞ (fun t => Sinf t i j)) {μ₁ μ₂ : ℝ} {k₁ k₂ : ℤ}
    (h₁ : HasLoopEigenWind Sinf μ₁ k₁) (h₂ : HasLoopEigenWind Sinf μ₂ k₂) (hμ : μ₁ < μ₂) :
    k₁ ≤ 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 (3); 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.hasLoopEigenWind_mono`

Let $S_\infty : \mathbb{R} \to \mathbb{R}^{2\times 2}$ be a loop of real $2\times 2$ matrices (indices "left", "right") that is continuous, $1$ -periodic, symmetric at every $t$ , and has $C^\infty$ entries $t \mapsto S_\infty(t)_{ij}$ . Let $\mu_1, \mu_2 \in \mathbb{R}$ and $k_1, k_2 \in \mathbb{Z}$ , and assume:

$\mathrm{HasLoopEigenWind}(S_\infty, \mu_1, k_1)$ and $\mathrm{HasLoopEigenWind}(S_\infty, \mu_2, k_2)$ ;
$\mu_1 < \mu_2$ (strict).

Then $k_1 \le k_2$ (non-strict).

Here $\mathrm{HasLoopEigenWind}(S_\infty, \mu, k)$ means: there exists at least one loop eigenfunction for $(S_\infty, \mu)$ , and every loop eigenfunction $e$ for $(S_\infty,\mu)$ has winding number $k$ . A loop eigenfunction for $(S_\infty,\mu)$ is a $C^\infty$ , $1$ -periodic $e : \mathbb{R} \to \mathbb{R}^2$ , not identically zero, with

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

and " $e$ has winding number $k$ " means that $f(t) = e_L(t) + i\,e_R(t)$ is continuous, $1$ -periodic, nowhere zero, and has a continuous argument $\theta$ ( $f = |f|e^{i\theta}$ ) with $\theta(1) - \theta(0) = 2\pi k$ .

In particular both $\mu_1$ and $\mu_2$ are assumed to be eigenvalues in this sense; the statement says nothing about values of $\mu$ that are not.

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

The winding of eigenfunctions is monotone in the eigenvalue

Theorem FiniteEnergyPlane.hasLoopEigenWind_mono

Theorem `FiniteEnergyPlane.hasLoopEigenWind_mono`