Prove2Me

The index formula for Cauchy–Riemann operators on the cylinder

Proved
CauchyRiemannIndex.index_formula

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

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

Let 1<p<∞1<p<\infty, let S±S^\pm be continuous loops of symmetric matrices and let S:R×S1→R2n×2nS:\mathbb{R}\times S^1\to\mathbb{R}^{2n\times2n} be continuous with S(s,⋅)→S±S(s,\cdot)\to S^\pm uniformly as s→±∞s\to\pm\infty; DS=∂s+J0∂t+S(s,t)D_S=\partial_s+J_0\partial_t+S(s,t). Assume that the asymptotic operators A±=−J0∂t−S±(t)A^\pm=-J_0\partial_t-S^\pm(t) are nondegenerate. Then DS:W1,p(R×S1,R2n)→Lp(R×S1,R2n)D_S:W^{1,p}(\mathbb{R}\times S^1,\mathbb{R}^{2n})\to L^p(\mathbb{R}\times S^1,\mathbb{R}^{2n}) is Fredholm and

ind⁡DS=μCZ(A+)−μCZ(A−).\operatorname{ind}D_S=\mu_{CZ}(A^+)-\mu_{CZ}(A^-).

This is Wendl's Riemann–Roch formula with punctures, ind⁡D=nχ(Σ˙)+2c1τ(E)+∑z∈Γ+μCZτ(Az)−∑z∈Γ−μCZτ(Az)\operatorname{ind}D=n\chi(\dot\Sigma)+2c_1^\tau(E)+\sum_{z\in\Gamma^+}\mu_{CZ}^\tau(A_z)-\sum_{z\in\Gamma^-}\mu_{CZ}^\tau(A_z), for the cylinder Σ˙=R×S1\dot\Sigma=\mathbb{R}\times S^1 (the sphere with one positive puncture at s=+∞s=+\infty and one negative puncture at s=−∞s=-\infty), where χ(Σ˙)=0\chi(\dot\Sigma)=0 and c1τ(E)=0c_1^\tau(E)=0 for the global trivialization of E=Σ˙×CnE=\dot\Sigma\times\mathbb{C}^n. It is the dimension formula for moduli spaces of Floer trajectories and of holomorphic cylinders in symplectizations.

Formalization Note pp is in ℝ≥0∞ with Fact (1 ≤ p), 1<p1<p and p≠∞p\ne\infty. The hypotheses on SS are IsSymLoop S± and IsAsymptoticTo S Splus Sminus. Nondegeneracy is IsNondegenerate S±: det⁡(Id−Ψ(1))≠0\det(\mathrm{Id}-\Psi(1))\ne0 for the fundamental solution Ψ\Psi. "Fredholm" is IsFredholmCR p S (finite-dimensional kernel, closed range, finite-dimensional cokernel), and the index is crIndex p S =dim⁡ker⁡−dim⁡(Lp/im⁡)=\dim\ker-\dim(L^p/\operatorname{im}). μCZ(A±)\mu_{CZ}(A^\pm) is asymptoticCZIndex S±, the Conley–Zehnder index of the path Ψ∣[0,1]\Psi|_{[0,1]} of the fundamental solution of Ψ′=J0S±Ψ\Psi'=J_0S^\pm\Psi. Wendl's operators have smooth coefficients converging in C∞C^\infty; here SS is only continuous, with uniform convergence at the ends (Remark 4.4).

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 5.4 (p. 82) with Theorem 4.3 (p. 69), for the cylinder `ℝ × S¹` (one positive
puncture at `s = +∞`, one negative puncture at `s = -∞`) and the trivial bundle with its global
trivialization: if `D_S = ∂ₛ + J₀ ∂ₜ + S(s, t)` is asymptotic to nondegenerate loops `S±` of
symmetric matrices and `1 < p < ∞`, then `D_S : W^{1,p} → L^p` is Fredholm and
`ind D_S = μ_CZ(-J₀ ∂ₜ - S⁺) - μ_CZ(-J₀ ∂ₜ - S⁻)`. -/
theorem index_formula (n : ℕ) (p : ℝ≥0∞) [Fact (1 ≤ p)] (hp : 1 < p) (hp' : p ≠ ⊤)
    (Splus Sminus : ℝ → Mat n) (hSplus : IsSymLoop Splus) (hSminus : IsSymLoop Sminus)
    (S : ℝ × ℝ → Mat n) (hS : IsAsymptoticTo S Splus Sminus) (hplus : IsNondegenerate Splus) (hminus : IsNondegenerate Sminus) :
    IsFredholmCR p S ∧ crIndex p S = asymptoticCZIndex Splus - asymptoticCZIndex Sminus := by
  sorry

end CauchyRiemannIndex
Source
C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lecture 5, Theorem 5.4, p. 82, with Lecture 4, Theorem 4.3, p. 69 (cylinder, trivial bundle, k = 1)
Read-back

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

Read-back: CauchyRiemannIndex.index_formula

Setting. n∈Nn\in\mathbb N; p∈[1,∞]p\in[1,\infty]; loops S±:R→R2n×2nS^\pm:\mathbb R\to\mathbb R^{2n\times2n}; S:R×R→R2n×2nS:\mathbb R\times\mathbb R\to\mathbb R^{2n\times2n}.

Hypotheses. 1<p<∞1<p<\infty; S±S^\pm continuous 1-periodic symmetric loops, nondegenerate; SS continuous, tt-periodic, S(s,⋅)→S+S(s,\cdot)\to S^+ as s→+∞s\to+\infty and →S−\to S^- as s→−∞s\to-\infty, entrywise uniformly in tt.

Definitions used. IsFredholmCR, crIndex (= dim⁡Rker⁡−dim⁡Rcoker⁡\dim_{\mathbb R}\ker-\dim_{\mathbb R}\operatorname{coker} of DS=∂s+J0∂t+S:W1,p→LpD_S=\partial_s+J_0\partial_t+S:W^{1,p}\to L^p on R×S1\mathbb R\times S^1; see isFredholm.md), asymptoticCZIndex (Gutt CZ index of Ψ∣[0,1]\Psi|_{[0,1]}, Ψ′=J0S±Ψ\Psi'=J_0S^\pm\Psi, Ψ(0)=I\Psi(0)=I; see asymptoticCZIndex_eq_iff_joined.md).

Conclusion.

DS is Fredholm and ind⁡DS=μCZ(−J0∂t−S+)−μCZ(−J0∂t−S−).D_S\text{ is Fredholm and }\operatorname{ind}D_S=\mu_{CZ}(-J_0\partial_t-S^+)-\mu_{CZ}(-J_0\partial_t-S^-).

Degenerate cases. n=0n=0: 0=0−00=0-0. S≡S+=S−S\equiv S^+=S^- (ss-independent): DSD_S invertible, 0=μ−μ0=\mu-\mu ✓.

Remarks. Positive puncture at s=+∞s=+\infty carries +μCZ+\mu_{CZ}, matching Wendl's sign for D=∂s+J∂t+SD=\partial_s+J\partial_t+S with asymptotic operator A=−J0∂t−SA=-J_0\partial_t-S. The first conjunct duplicates isFredholm; it is what makes crIndex meaningful (no finrank-0 junk).

Soundness checks.

  1. Junk/coercions: crIndex casts both finranks to ℤ before subtracting; ℤ subtraction on the right. CZ values are genuine (nondegenerate continuous loops, see the CZ read-backs). All data universally quantified.
  2. Hand test (a): n=1n=1, S(s,t)=c(s)IS(s,t)=c(s)I, c→−εc\to-\varepsilon at −∞-\infty, c→+εc\to+\varepsilon at +∞+\infty, 0<ε<π0<\varepsilon<\pi. Fourier in tt with J0=iJ_0=i: u=∑kak(s)e2πiktu=\sum_ka_k(s)e^{2\pi ikt}, J0∂tu⇝−2πkakJ_0\partial_tu\leadsto-2\pi k a_k, so ak′+(c−2πk)ak=0a_k'+(c-2\pi k)a_k=0, ak=ak(0)e−∫0s(c−2πk)a_k=a_k(0)e^{-\int_0^s(c-2\pi k)}. k=0k=0: decays at both ends (rate ε\varepsilon); k≥1k\ge1: grows at +∞+\infty; k≤−1k\le-1: grows at −∞-\infty. Kernel ={e−∫0scv:v∈R2}=\{e^{-\int_0^sc}v:v\in\mathbb R^2\}, real dimension 2. Formal adjoint D∗=−∂s+J0∂t+cD^*=-\partial_s+J_0\partial_t+c: −ak′+(c−2πk)ak=0-a_k'+(c-2\pi k)a_k=0, ak=e∫0s(c−2πk)a_k=e^{\int_0^s(c-2\pi k)}; k=0k=0 grows at both ends, k≥1k\ge1 grows at −∞-\infty, k≤−1k\le-1 grows at +∞+\infty: cokernel 00. Index =2=2. CZ side: S+=εIS^+=\varepsilon I: Ψ\Psi = rotation by εt\varepsilon t, μ=1\mu=1; S−=−εIS^-=-\varepsilon I: μ=−1\mu=-1 (computed from the Lean definitions, see asymptoticCZIndex_eq_iff_joined.md and asymptoticCZIndex_conj.md). 1−(−1)=21-(-1)=2 ✓. Sign and normalization conventions agree. Not vacuous; true (Wendl Thm 5.4 + 4.3 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