The index of a Cauchy–Riemann operator on the cylinder from antilinear deformations of its asymptotic operators

Proved

CauchyRiemannIndex.index_eq_winding_of_antilinear_deformation

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

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

Let $n=1$ , let $S^\pm$ be continuous loops of symmetric $2\times2$ matrices with nondegenerate asymptotic operators, and let $S:\mathbb{R}\times S^1\to\mathbb{R}^{2\times2}$ be continuous with $S(s,\cdot)\to S^\pm$ uniformly as $s\to\pm\infty$ . Suppose that for each sign there are a continuous loop $S'^\pm$ of symmetric matrices with

\mu_{CZ}(-J_0\partial_t-S'^\pm)=\mu_{CZ}(-J_0\partial_t-S^\pm)

and a continuous loop $\beta_\pm:S^1\to\mathbb{C}\setminus\{0\}$ such that the asymptotic operator

\eta\mapsto-J_0\dot\eta-S'^\pm\eta-\sigma\beta_\pm\bar\eta

is nondegenerate for every $\sigma\ge0$ . Then the index of $D_S:W^{1,2}\to L^2$ is

\operatorname{ind}D_S=\operatorname{wind}(\beta_+)-\operatorname{wind}(\beta_-).

Formalization Note $\eta\mapsto\beta\bar\eta$ is the matrix antilinearMat β, so the deformed operator is the asymptotic operator of the loop $S'^\pm+\sigma\cdot$ antilinearMat ∘ β±. The winding numbers $w_\pm$ are given through continuous arguments: $\beta_\pm(t)=|\beta_\pm(t)|e^{i\theta_\pm(t)}$ with $\theta_\pm(1)-\theta_\pm(0)=2\pi w_\pm$ . The index is crIndex 2 S; for the cylinder $\chi=0$ and $c_1^\tau=0$ in Wendl's formula. The exponent is $p=2$ (Wendl, Assumption 5.7).

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, Lemma 5.28 (p. 102), on the cylinder with the trivial line bundle and its global
trivialization, `p = 2`: let `D_S` (`n = 1`) be asymptotic to nondegenerate loops `S±` of symmetric
matrices. Suppose that for each end there are a loop `S'±` of symmetric matrices with
`μ_CZ(-J₀ ∂ₜ - S'±) = μ_CZ(-J₀ ∂ₜ - S±)` and a nowhere-vanishing loop `β± : S¹ → ℂ` such that
`η ↦ -J₀ η' - S'± η - σ β± η̄` is nondegenerate for every `σ ≥ 0`. Then
`ind D_S = wind(β⁺) - wind(β⁻)`. -/
theorem index_eq_winding_of_antilinear_deformation (Splus Sminus : ℝ → Mat 1)
    (hSplus : IsSymLoop Splus) (hSminus : IsSymLoop Sminus)
    (hplus : IsNondegenerate Splus) (hminus : IsNondegenerate Sminus)
    (S : ℝ × ℝ → Mat 1) (hS : IsAsymptoticTo S Splus Sminus)
    (S'plus S'minus : ℝ → Mat 1) (h'plus : IsSymLoop S'plus) (h'minus : IsSymLoop S'minus)
    (hμplus : asymptoticCZIndex S'plus = asymptoticCZIndex Splus)
    (hμminus : asymptoticCZIndex S'minus = asymptoticCZIndex Sminus)
    (βplus βminus : ℝ → ℂ) (hβplus : Continuous βplus) (hβminus : Continuous βminus)
    (hperplus : Function.Periodic βplus 1) (hperminus : Function.Periodic βminus 1)
    (hnzplus : ∀ t, βplus t ≠ 0) (hnzminus : ∀ t, βminus t ≠ 0)
    (hndplus : ∀ σ : ℝ, 0 ≤ σ → IsNondegenerate (fun t => S'plus t + σ • antilinearMat (βplus t)))
    (hndminus : ∀ σ : ℝ, 0 ≤ σ → IsNondegenerate (fun t => S'minus t + σ • antilinearMat (βminus t)))
    (wplus wminus : ℤ) (θplus θminus : ℝ → ℝ) (hθplus : Continuous θplus)
    (hθminus : Continuous θminus)
    (hargplus : ∀ t, βplus t = ‖βplus t‖ * Complex.exp (θplus t * Complex.I))
    (hargminus : ∀ t, βminus t = ‖βminus t‖ * Complex.exp (θminus t * Complex.I))
    (hwplus : θplus 1 - θplus 0 = 2 * Real.pi * wplus)
    (hwminus : θminus 1 - θminus 0 = 2 * Real.pi * wminus) :
    crIndex 2 S = wplus - wminus := 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.28, p. 102 (cylinder, trivial line bundle, global trivialization, p = 2)

Read-back

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

Read-back: `CauchyRiemannIndex.index_eq_winding_of_antilinear_deformation`

Setting. $n=1$ , $p=2$ ; loops $S^\pm,S'^\pm:\mathbb R\to\mathbb R^{2\times2}$ ; $S:\mathbb R\times\mathbb R\to\mathbb R^{2\times2}$ ; loops $\beta^\pm:\mathbb R\to\mathbb C$ ; integers $w^\pm$ ; functions $\theta^\pm:\mathbb R\to\mathbb R$ .

Hypotheses. $S^\pm$ continuous 1-periodic symmetric loops, nondegenerate; $S$ continuous, $t$ -periodic, asymptotic to $S^\pm$ . $S'^\pm$ continuous 1-periodic symmetric loops with $\mu_{CZ}(-J_0\partial_t-S'^\pm)=\mu_{CZ}(-J_0\partial_t-S^\pm)$ (as asymptoticCZIndex). $\beta^\pm$ continuous, 1-periodic, nowhere zero, and for every $\sigma\ge0$ the loop $S'^\pm+\sigma\,$ antilinearMat $(\beta^\pm)$ is nondegenerate, i.e. $\eta\mapsto-J_0\eta'-S'^\pm\eta-\sigma\beta^\pm\bar\eta$ has no nonzero 1-periodic solution. $\theta^\pm$ continuous with $\beta^\pm(t)=|\beta^\pm(t)|e^{i\theta^\pm(t)}$ for all $t$ , and $\theta^\pm(1)-\theta^\pm(0)=2\pi w^\pm$ .

Definitions used. crIndex ( $\dim_{\mathbb R}\ker-\dim_{\mathbb R}\operatorname{coker}$ of $D_S=\partial_s+J_0\partial_t+S:W^{1,2}\to L^2$ ), asymptoticCZIndex, IsNondegenerate, antilinearMat ( $\beta\mapsto$ real matrix of $z\mapsto\beta\bar z$ ; checked in large_antilinear_perturbation_index.md).

Conclusion.

\operatorname{ind}D_S=w^+-w^-,\qquad w^\pm=\mathrm{wind}(\beta^\pm).

Degenerate cases. $\beta^\pm$ constant: $w^\pm=0$ , so the claim is $\operatorname{ind}D_S=0$ ; the hypotheses then force $\mu(S^\pm)=\mu(S'^\pm)=\mu(\text{large-}\sigma\text{ hyperbolic loop})=0$ , consistent with index_formula ( $0-0$ ). Example $S'=\varepsilon I$ , $\beta=1$ : $-i\eta'-\varepsilon\eta-\sigma\bar\eta=0$ gives $x'=(\sigma-\varepsilon)y$ , $y'=(\sigma+\varepsilon)x$ , degenerate at $\sigma=\varepsilon$ (solution $\eta=i$ ): the hypothesis correctly excludes the pair ( $\mu(\varepsilon I)=1\ne0=\mathrm{wind}\,1$ ).

Remarks.

Winding encoding: $\theta^\pm$ is continuous on all of $\mathbb R$ and $\beta^\pm$ is 1-periodic, so $\theta^\pm(1)-\theta^\pm(0)\in2\pi\mathbb Z$ and is independent of the lift; hwplus pins $w^\pm$ to that integer. Since $\beta^\pm\neq0$ a lift exists, so the $\theta$ / $w$ hypotheses are not an extra restriction. Coercion ‖β t‖ : ℂ is the real modulus; Complex.exp (θ t * I) is $e^{i\theta}$ . Correct.
Model test. $S'_k(t)=\pi k I+\delta\,$ antilinearMat $(e^{2\pi ikt})$ , $\delta\ge0$ , $\beta=e^{2\pi ikt}$ (winding $k$ , $\theta=2\pi kt$ ). With $\eta=e^{\pi ikt}\xi$ : $-i\eta'-\pi k\eta-(\delta+\sigma)e^{2\pi ikt}\bar\eta=e^{\pi ikt}(-i\xi'-(\delta+\sigma)\bar\xi)$ , i.e. $x'=(\delta+\sigma)y$ , $y'=(\delta+\sigma)x$ : hyperbolic for $\delta+\sigma>0$ , so nondegenerate for all $\sigma\ge0$ when $\delta>0$ (any $k$ ), or when $\delta=0$ and $k$ odd ( $\sigma=0$ : $\Psi(1)=e^{i\pi k}=-I$ ). CZ index from the Lean definition: $\Psi(t)=e^{i\pi kt}H(t)$ , $H=\cosh(ct)I+\sinh(ct)K$ with $K$ antilinear, $C_H=\cosh(ct)I$ , so $\hat\rho(\Psi(t))=e^{i\pi kt}$ , $\Delta\theta_1=\pi k$ ; the extension from $\Psi(1)=\pm H(1)$ to $W^-$ ( $k$ even, $\det(1-\Psi(1))<0$ ) or $W^+$ ( $k$ odd, $\det(1-\Psi(1))>0$ ) can be taken with $\hat\rho$ constant ( $=\pm1$ ), so $\Delta\theta_2=0$ and $\mu=k$ . Hence with $S^\pm$ of indices $k_\pm$ and these $S'^\pm,\beta^\pm$ , all hypotheses hold and the conclusion reads $\operatorname{ind}D_S=k_+-k_-=\mu(S^+)-\mu(S^-)$ , agreeing with index_formula. Signs and normalization agree.
General truth: nondegeneracy for all $\sigma\ge0$ makes $\mu(S'^\pm+\sigma B^\pm)$ constant in $\sigma$ ; for large $\sigma$ the loop is uniformly hyperbolic-dominated and its index equals $\mathrm{wind}(\beta^\pm)$ (smooth approximation of the merely continuous $\beta^\pm$ changes $\sigma B$ by $\sigma\delta$ with $\delta<\min|\beta|/2$ , below the $\sim\sigma\min|\beta|$ spectral gap, so continuity of $\beta^\pm$ suffices). With index_formula this gives the claim. Note $S'^\pm$ and $\beta^\pm$ are linked to $S$ only through the CZ index, which is all that matters.

Soundness checks.

Junk/coercions: crIndex is junk (finrank 0) unless $D_S$ is Fredholm, and Fredholmness is not a hypothesis or conjunct here; but the hypotheses hplus, hminus, hS (with $p=2\in(1,\infty)$ ) are exactly those of index_formula, whose conclusion includes IsFredholmCR 2 S, so in every instance the index is genuine. asymptoticCZIndex values are genuine since $S^\pm$ and $S'^\pm$ (the $\sigma=0$ case of hndplus/hndminus) are nondegenerate. ℤ arithmetic on the right; wplus wminus : ℤ cast to ℝ in hwplus. All data universally quantified; ∀ σ, 0 ≤ σ → … scope correct.
Not vacuous (model above satisfies every hypothesis for any $k_\pm$ , with $S$ any coefficient asymptotic to $S^\pm$ ); not trivially true or false. No hypothesis contradicts another: the constraint $\mu(S'^\pm)=\mathrm{wind}\,\beta^\pm$ implied by hnd* is satisfiable for every integer. True (Wendl Lemma 5.28 / Thm 5.4 on the cylinder).

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

The index of a Cauchy–Riemann operator on the cylinder from antilinear deformations of its asymptotic operators

Read-back: CauchyRiemannIndex.index_eq_winding_of_antilinear_deformation

Read-back: `CauchyRiemannIndex.index_eq_winding_of_antilinear_deformation`