Each winding number belongs to a two-dimensional space of eigenfunctions

Proved

FiniteEnergyPlane.loopEigenSpan_finrank_eq_two

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}$ . For every $k\in\mathbb{Z}$ , the eigenfunctions of $A$ whose eigenvalue has winding $k$ span a real vector space of dimension exactly $2$ .

Formalization Note The span is loopEigenSpan Sinf k, a submodule of ℝ → CauchyRiemannIndex.Vec 1; the statement includes FiniteDimensional, so Module.finrank is the actual dimension.

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 (4): for every `k ∈ ℤ`, the eigenfunctions of `A = -J₀ ∂ₜ - S∞` with
winding number `k` span a real vector space of dimension exactly `2`. In particular every
winding number is attained, by one eigenvalue of multiplicity `2` or by two eigenvalues of
multiplicity `1`. -/
theorem loopEigenSpan_finrank_eq_two (Sinf : ℝ → CauchyRiemannIndex.Mat 1) (hSinf : CauchyRiemannIndex.IsSymLoop Sinf)
    (hSinf' : ∀ i j, ContDiff ℝ ∞ (fun t => Sinf t i j)) (k : ℤ) :
    FiniteDimensional ℝ (loopEigenSpan Sinf k) ∧ Module.finrank ℝ (loopEigenSpan Sinf k) = 2 := 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 (4); 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.loopEigenSpan_finrank_eq_two`

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 $k \in \mathbb{Z}$ be arbitrary.

Consider the real vector space of all functions $\mathbb{R} \to \mathbb{R}^2$ , and in it the subspace

E_k = \operatorname{span}_{\mathbb{R}}\big\{\, e \;:\; \exists \mu \in \mathbb{R},\ e \text{ is a loop eigenfunction for } (S_\infty,\mu) \text{ and } \mathrm{HasLoopEigenWind}(S_\infty, \mu, k) \,\big\}.

Here 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 $\mathrm{HasLoopEigenWind}(S_\infty, \mu, k)$ means that $\mu$ has at least one loop eigenfunction and every loop eigenfunction $e$ of $\mu$ has winding number $k$ , i.e. $f(t) = e_L(t) + i\,e_R(t)$ is continuous, $1$ -periodic, nowhere zero, with a continuous argument $\theta$ ( $f = |f| e^{i\theta}$ ) satisfying $\theta(1) - \theta(0) = 2\pi k$ .

The theorem asserts that $E_k$ is finite-dimensional over $\mathbb{R}$ and

\dim_{\mathbb{R}} E_k = 2.

Since $k$ ranges over all integers with no further hypothesis, this claims in particular that for every integer $k$ (positive, zero or negative) the set of eigenvalues all of whose eigenfunctions wind exactly $k$ times is non-empty, and the eigenfunctions of all such eigenvalues together span exactly a 2-dimensional space.

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

Each winding number belongs to a two-dimensional space of eigenfunctions

Theorem FiniteEnergyPlane.loopEigenSpan_finrank_eq_two

Theorem `FiniteEnergyPlane.loopEigenSpan_finrank_eq_two`