The Conley–Zehnder index of a nondegenerate loop operator equals $\alpha^-+\alpha^+$

Proved

FiniteEnergyPlane.exists_loopAlpha_czIndexOfPath_eq

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

conley-zehnder-indexsymplectic-geometrywinding-numbers

Let $S_\infty:\mathbb{R}\to\mathbb{R}^{2\times 2}$ be a smooth $1$ -periodic loop of symmetric matrices, and suppose the asymptotic operator $A=-J_0\,\partial_t-S_\infty$ on $1$ -periodic loops in $\mathbb{R}^2=\mathbb{C}$ is nondegenerate, i.e. $0$ is not an eigenvalue. Let $\Psi$ be the fundamental solution, $\Psi(0)=I$ , $\Psi'(t)=J_0S_\infty(t)\Psi(t)$ . Then:

$\alpha^-$ , the largest winding number of the eigenfunctions of a negative eigenvalue of $A$ , exists;
$\alpha^+$ , the smallest winding number of the eigenfunctions of a nonnegative eigenvalue of $A$ , exists;
$\alpha^+-\alpha^-\in\{0,1\}$ ;
the Conley–Zehnder index (Hryniewicz's winding-interval index) of the path $t\mapsto\Psi(t)$ , $t\in[0,1]$ , equals $\alpha^-+\alpha^+$ .

This is the loop form of Hofer–Wysocki–Zehnder's formula $\mu_{CZ}=2\alpha^-+p$ with $p=\alpha^+-\alpha^-$ : it expresses the Conley–Zehnder index of a nondegenerate asymptotic operator in dimension two through the winding numbers of its eigenfunctions.

Formalization Note " $\mu$ is an eigenvalue whose eigenfunctions have winding $k$ " is HasLoopEigenWind Sinf μ k (winding of $t\mapsto e(t)$ as a loop in $\mathbb{C}$ via vecToC). $\alpha^\pm$ are spelled out as an attained upper (resp. lower) bound. Nondegeneracy is CauchyRiemannIndex.IsNondegenerate, the index is HryniewiczCriterion.czIndexOfPath, and matrices are transported along finSumFinEquiv : Fin 1 ⊕ Fin 1 ≃ Fin 2 ( $q\mapsto0$ , $p\mapsto1$ ).

Preamble

import Definitions.Def_FiniteEnergyPlane_Winding

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- Hofer–Wysocki–Zehnder (GAFA 1995, Theorem 3.10) for a loop of symmetric `2 × 2` matrices: if
`A = -J₀ ∂ₜ - S∞` is nondegenerate, then `a = α⁻` (the largest winding number of a negative
eigenvalue) and `b = α⁺` (the smallest winding number of a nonnegative eigenvalue) exist,
`b - a ∈ {0, 1}`, and Hryniewicz's index of the path `t ↦ Ψ(t)`, `t ∈ [0, 1]`, of the fundamental
solution `Ψ` of `S∞` is `a + b`. The matrices are transported along `Fin 1 ⊕ Fin 1 ≃ Fin 2`. -/
theorem exists_loopAlpha_czIndexOfPath_eq (Sinf : ℝ → CauchyRiemannIndex.Mat 1)
    (hSinf : CauchyRiemannIndex.IsSymLoop Sinf)
    (hSinf' : ∀ i j, ContDiff ℝ ∞ (fun t => Sinf t i j))
    (hnd : CauchyRiemannIndex.IsNondegenerate Sinf) :
    ∃ a b : ℤ,
      ((∃ μ < 0, HasLoopEigenWind Sinf μ a) ∧
        ∀ μ < 0, ∀ k : ℤ, HasLoopEigenWind Sinf μ k → k ≤ a) ∧
      ((∃ μ, 0 ≤ μ ∧ HasLoopEigenWind Sinf μ b) ∧
        ∀ μ, 0 ≤ μ → ∀ k : ℤ, HasLoopEigenWind Sinf μ k → b ≤ k) ∧
      (b = a ∨ b = a + 1) ∧
      ∀ Ψ : ℝ → CauchyRiemannIndex.Mat 1, CauchyRiemannIndex.IsFundamentalSolution Sinf Ψ →
        HryniewiczCriterion.czIndexOfPath
          (fun τ => Matrix.reindex finSumFinEquiv finSumFinEquiv (Ψ τ)) = a + b := by
  sorry

end FiniteEnergyPlane

Source

H. Hofer, K. Wysocki, E. Zehnder, GAFA 5 (1995), Theorem 3.10; U. Hryniewicz, J. Symplectic Geom. 12 (2014), Remark 2.6 (auxiliary lemma)

View graph

The Conley–Zehnder index of a nondegenerate loop operator equals α−+α+\alpha^-+\alpha^+α−+α+

The Conley–Zehnder index of a nondegenerate loop operator equals $\alpha^-+\alpha^+$