A Conley–Zehnder value of a nondegenerate symplectic path is its index

Proved

CauchyRiemannIndex.czIndex_eq_of_isCZValue

by Mazecto · Oct 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

cauchy-riemannconley-zehnder-indexsymplectic-geometry

Let $\psi:[0,1]\to\mathrm{Sp}(2n)$ be a continuous path of symplectic matrices with $\psi(0)=\mathrm{Id}$ and $\det(\mathrm{Id}-\psi(1))\neq0$ . If $k\in\mathbb{Z}$ is a Conley–Zehnder value of $\psi$ (the degree of $\hat\rho^2$ along $\psi$ followed by some extension in $\mathrm{Sp}^*$ ending at $W^\pm$ ), then $\mu_{CZ}(\psi)=k$ .

This lets one evaluate the mission's Conley–Zehnder index from any single admissible extension.

Formalization Note IsCZValue ψ k and czIndex ψ are the mission's definitions (Gutt, Definition 7 with Corollary 12); czIndex is defined by choice, so the statement says that this choice returns $k$ .

Preamble

import Definitions.Def_CauchyRiemannIndex_Setting

Formal statement

namespace CauchyRiemannIndex

open Matrix

/-- For a path `ψ` of symplectic matrices with `ψ(0) = Id` and `1` not an eigenvalue of `ψ(1)`,
every Conley–Zehnder value `k` of `ψ` is its Conley–Zehnder index: `czIndex ψ = k`. -/
theorem czIndex_eq_of_isCZValue {n : ℕ} (ψ : C(unitInterval, Mat n))
    (hsymp : ∀ t, IsSymplectic (ψ t)) (h0 : ψ 0 = 1) (h1 : (1 - ψ 1).det ≠ 0) (k : ℤ)
    (hk : IsCZValue ψ k) : czIndex ψ = k := by
  sorry

end CauchyRiemannIndex

Source

C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lecture 5, Lemma 5.29, p. 103

View graph