Prove2Me

Nondegenerate asymptotic operators with equal Conley–Zehnder index are homotopic through nondegenerate ones

Proved
CauchyRiemannIndex.asymptoticCZIndex_eq_iff_joined

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

cauchy-riemannconley-zehnder-indexfredholm-indexsobolev-spacessymplectic-geometry

Let S0S_0, S1S_1 be continuous loops of symmetric matrices whose asymptotic operators −J0∂t−S0-J_0\partial_t-S_0, −J0∂t−S1-J_0\partial_t-S_1 are nondegenerate. Then μCZ(−J0∂t−S0)=μCZ(−J0∂t−S1)\mu_{CZ}(-J_0\partial_t-S_0)=\mu_{CZ}(-J_0\partial_t-S_1) if and only if there is a continuous family (Sτ)τ∈[0,1](S_\tau)_{\tau\in[0,1]} of loops of symmetric matrices from S0S_0 to S1S_1 such that every −J0∂t−Sτ-J_0\partial_t-S_\tau is nondegenerate.

Formalization Note The family is a continuous map H : C(unitInterval × ℝ, Mat n) with IsSymLoop (H (τ, ·)) and IsNondegenerate (H (τ, ·)) for every τ\tau. Wendl states the theorem for the space of smooth asymptotic operators on a Hermitian bundle with a trivialization; here the bundle is trivial and the loops are continuous.

Preamble
import Definitions.Def_CauchyRiemannIndex_Setting
import Mathlib.Analysis.Calculus.ContDiff.Basic
Formal statement
namespace CauchyRiemannIndex

open MeasureTheory Matrix Filter Topology
open scoped ENNReal NNReal ContDiff RealInnerProductSpace

/-- Wendl, Theorem 3.34 (p. 62), trivial bundle: two nondegenerate loops `S₀`, `S₁` of symmetric
matrices have the same Conley–Zehnder index `μ_CZ(-J₀ ∂ₜ - S)` if and only if they are joined by
a continuous family of nondegenerate loops of symmetric matrices. -/
theorem asymptoticCZIndex_eq_iff_joined (n : ℕ) (S₀ S₁ : ℝ → Mat n) (h₀ : IsSymLoop S₀)
    (h₁ : IsSymLoop S₁) (hn₀ : IsNondegenerate S₀) (hn₁ : IsNondegenerate S₁) :
    asymptoticCZIndex S₀ = asymptoticCZIndex S₁ ↔
      ∃ H : C(unitInterval × ℝ, Mat n), (∀ t, H (0, t) = S₀ t) ∧ (∀ t, H (1, t) = S₁ t) ∧
        ∀ τ, IsSymLoop (fun t => H (τ, t)) ∧ IsNondegenerate (fun t => H (τ, t)) := by
  sorry

end CauchyRiemannIndex
Source
C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lecture 3, Theorem 3.34, p. 62 (trivial bundle)
Read-back

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

Read-back: CauchyRiemannIndex.asymptoticCZIndex_eq_iff_joined

Setting. n∈Nn\in\mathbb N; S0,S1:R→R2n×2nS_0,S_1:\mathbb R\to\mathbb R^{2n\times2n}.

Hypotheses. S0,S1S_0,S_1 are continuous, 1-periodic, pointwise symmetric (IsSymLoop) and nondegenerate (IsNondegenerate: det⁡(I−Ψi(1))≠0\det(I-\Psi_i(1))\ne0 for the fundamental solution Ψi′=J0SiΨi\Psi_i'=J_0S_i\Psi_i, Ψi(0)=I\Psi_i(0)=I).

Definitions used.

  • asymptoticCZIndex S = the kk with IsAsymptoticCZValue S k (chosen; fallback 0): there is a fundamental solution Ψ\Psi of SS and the path ψ=Ψ∣[0,1]\psi=\Psi|_{[0,1]} has IsCZValue ψ k.
  • IsCZValue ψ k: there is a path χ\chi in Sp∗={A∈Sp(2n):det⁡(I−A)≠0}\mathrm{Sp}^*=\{A\in\mathrm{Sp}(2n):\det(I-A)\ne0\} from ψ(1)\psi(1) to W+=−IW^+=-I or W−=diag⁡(2,−1,…,−1,12,−1,…,−1)W^-=\operatorname{diag}(2,-1,\dots,-1,\tfrac12,-1,\dots,-1), and continuous arguments θ1,θ2\theta_1,\theta_2 of ρ^∘ψ\hat\rho\circ\psi, ρ^∘χ\hat\rho\circ\chi with 2[(θ1(1)−θ1(0))+(θ2(1)−θ2(0))]=2πk2[(\theta_1(1)-\theta_1(0))+(\theta_2(1)-\theta_2(0))]=2\pi k, where ρ^(A)=det⁡CCA/∣det⁡CCA∣\hat\rho(A)=\det_{\mathbb C}C_A/|\det_{\mathbb C}C_A|, CA=12(A−J0AJ0)C_A=\tfrac12(A-J_0AJ_0), det⁡C\det_{\mathbb C} of X+iYX+iY for C_A=\begin{psmallmatrix}X&-Y\\Y&X\end{psmallmatrix} (blocks toBlocks₁₁, toBlocks₂₁, checked). This is Gutt's deg⁡(ρ^2∘ψ~)\deg(\hat\rho^2\circ\tilde\psi).

Conclusion.

μCZ(S0)=μCZ(S1)  ⟺  ∃H∈C([0,1]×R,R2n×2n): H(0,⋅)=S0, H(1,⋅)=S1, ∀τ, H(τ,⋅) is a continuous 1-periodic symmetric nondegenerate loop.\mu_{CZ}(S_0)=\mu_{CZ}(S_1)\iff\exists H\in C([0,1]\times\mathbb R,\mathbb R^{2n\times2n}):\ H(0,\cdot)=S_0,\ H(1,\cdot)=S_1,\ \forall\tau,\ H(\tau,\cdot)\text{ is a continuous 1-periodic symmetric nondegenerate loop.}

Degenerate cases. n=0n=0: every index is 0 and HH constant works; both sides true. S0=S1S_0=S_1: both sides true (constant HH).

Remarks. Joint continuity of HH on [0,1]×R[0,1]\times\mathbb R with periodic slices is equivalent to a continuous path in the space of loops with the uniform topology, which is the natural topology for Wendl's Thm 3.34 (stated there for asymptotic operators; on the trivial bundle these are exactly −J0∂t−S-J_0\partial_t-S). The "⇒" direction asks for a family of genuinely periodic symmetric loops (not merely a homotopy of the paths Ψ\Psi through nondegenerate paths); this is the stronger claim, and it is what Wendl 3.34 asserts. Not a mis-formalization.

Soundness checks.

  1. Junk values: czIndex/asymptoticCZIndex fall back to 0 only when no value exists; for a nondegenerate continuous loop Ψ\Psi exists, is unique, is symplectic (J0SJ_0S Hamiltonian), Ψ(1)∈Sp∗\Psi(1)\in\mathrm{Sp}^*, and CAC_A is invertible on Sp\mathrm{Sp}, so a value exists. Uniqueness of the value: W+W^+, W−W^- lie in different components of Sp∗\mathrm{Sp}^* (det⁡(I−W+)=22n>0\det(I-W^+)=2^{2n}>0, det⁡(I−W−)<0\det(I-W^-)<0), so two extensions end at the same point and differ by a loop in Sp∗\mathrm{Sp}^*, along which deg⁡ρ^2=0\deg\hat\rho^2=0 (Gutt); lifts are unique up to constants. So choose returns the genuine index. Coercion unitInterval → ℝ in ψ t = Ψ t is the subtype coercion. τ\tau ranges over unitInterval.
  2. Hand checks: S=εIS=\varepsilon I (n=1n=1, 0<ε<π0<\varepsilon<\pi): Ψ(t)\Psi(t) = rotation by εt\varepsilon t, ρ^=eiεt\hat\rho=e^{i\varepsilon t}; extend by rotations to −I-I: total argument change π\pi, so μ=1\mu=1. S=diag⁡(1,−1)S=\operatorname{diag}(1,-1): \Psi(t)=\begin{psmallmatrix}\cosh t&\sinh t\\ \sinh t&\cosh t\end{psmallmatrix}, CΨ=cosh⁡t IC_\Psi=\cosh t\,I, ρ^≡1\hat\rho\equiv1; extension inside positive hyperbolic symmetric matrices to W−W^- keeps ρ^≡1\hat\rho\equiv1; μ=0\mu=0. These two loops have different indices and indeed cannot be joined through nondegenerate loops (the path endpoint would have to cross from trace <2<2 to trace >2>2 through eigenvalue 1). Consistent. Statement is not vacuous and is true (Wendl Thm 3.34; Robbin–Salamon/Gutt classification of nondegenerate paths).

Verdict: no mis-formalization observed

Human review

  • Endorsed by Shuze Chen · Oct 14, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Mazecto · Oct 14, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph