Prove2Me

Model asymptotic operators with prescribed Conley–Zehnder index

Proved
CauchyRiemannIndex.model_asymptotic_operator

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

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

Let k∈Zk\in\mathbb{Z} and σ>0\sigma>0. On loops η:S1→C\eta:S^1\to\mathbb{C} the asymptotic operator

η↦−J0η˙−πk η−σe2πikt ηˉ\eta\mapsto-J_0\dot\eta-\pi k\,\eta-\sigma e^{2\pi ikt}\,\bar\eta

is nondegenerate and its Conley–Zehnder index is kk.

Formalization Note This is −J0∂t−S(t)-J_0\partial_t-S(t) with S(t)=πk Id+σ⋅S(t)=\pi k\,\mathrm{Id}+\sigma\cdot antilinearMat (exp (2πikt)), where antilinearMat β is the symmetric real matrix of z↦βzˉz\mapsto\beta\bar z on C=R2\mathbb{C}=\mathbb{R}^2 (Mat 1).

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.29 (p. 103): for `k ∈ ℤ` and `σ > 0`, the asymptotic operator
`η ↦ -J₀ ∂ₜη - π k η - σ e^{2πikt} η̄` on `C^∞(S¹, ℂ)` is nondegenerate and has Conley–Zehnder
index `k`. -/
theorem model_asymptotic_operator (k : ℤ) (σ : ℝ) (hσ : 0 < σ) :
    IsNondegenerate (fun t : ℝ => (Real.pi * k) • (1 : Mat 1) +
        σ • antilinearMat (Complex.exp (2 * Real.pi * k * t * Complex.I))) ∧
      asymptoticCZIndex (fun t : ℝ => (Real.pi * k) • (1 : Mat 1) +
        σ • antilinearMat (Complex.exp (2 * Real.pi * k * t * Complex.I))) = 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
Read-back

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

Read-back: CauchyRiemannIndex.model_asymptotic_operator

Setting. n=1n=1; k∈Zk\in\mathbb Z, σ∈R\sigma\in\mathbb R. R2=C\mathbb R^2=\mathbb C via (x,y)↦x+iy(x,y)\mapsto x+iy, J0=iJ_0=i.

Hypotheses. σ>0\sigma>0.

Definitions used. antilinearMat β =\begin{psmallmatrix}\Re\beta&\Im\beta\\ \Im\beta&-\Re\beta\end{psmallmatrix}, the real matrix of z↦βzˉz\mapsto\beta\bar z (checked: βzˉ=(ℜβ x+ℑβ y)+i(ℑβ x−ℜβ y)\beta\bar z=(\Re\beta\,x+\Im\beta\,y)+i(\Im\beta\,x-\Re\beta\,y)). The loop is

Sk(t)=πk I+σ antilin(e2πikt),Sk(t)η=πkη+σe2πiktηˉ.S_k(t)=\pi k\,I+\sigma\,\mathrm{antilin}(e^{2\pi ikt}),\qquad S_k(t)\eta=\pi k\eta+\sigma e^{2\pi ikt}\bar\eta .

IsNondegenerate, asymptoticCZIndex: Gutt CZ index of the fundamental solution Ψ′=J0SkΨ\Psi'=J_0S_k\Psi, Ψ(0)=I\Psi(0)=I (see asymptoticCZIndex_eq_iff_joined.md).

Conclusion. SkS_k is nondegenerate and μCZ(−J0∂t−Sk)=k\mu_{CZ}(-J_0\partial_t-S_k)=k, i.e. the operator η↦−iη′−πkη−σe2πiktηˉ\eta\mapsto-i\eta'-\pi k\eta-\sigma e^{2\pi ikt}\bar\eta has CZ index kk.

Degenerate cases. k=0k=0: S0=σdiag⁡(1,−1)S_0=\sigma\operatorname{diag}(1,-1); \Psi(t)=\begin{psmallmatrix}\cosh\sigma t&\sinh\sigma t\\ \sinh\sigma t&\cosh\sigma t\end{psmallmatrix}, ρ^≡1\hat\rho\equiv1, endpoint positive hyperbolic, extend to W−W^- with ρ^≡1\hat\rho\equiv1: μ=0\mu=0 ✓ (matches the hand value for diag⁡(1,−1)\operatorname{diag}(1,-1), σ=1\sigma=1).

Remarks. Casts: Real.pi * k is π⋅(k:R)\pi\cdot(k:\mathbb R); 2 * Real.pi * k * t * Complex.I is 2πkt i2\pi kt\,i in C\mathbb C. SkS_k is continuous, 1-periodic and symmetric, so it is a legitimate IsSymLoop (not hypothesised, but true).

Soundness checks.

  1. No junk: SkS_k continuous, so Ψ\Psi exists uniquely; nondegeneracy is asserted (first conjunct), so the index is a genuine value. Scalar actions: • on Mat 1 by reals, fine.
  2. Hand computation for general kk: put η=eiπktξ\eta=e^{i\pi kt}\xi. Then η′=i(πkη+σe2πiktηˉ)\eta'=i(\pi k\eta+\sigma e^{2\pi ikt}\bar\eta) becomes ξ′=iσξˉ\xi'=i\sigma\bar\xi, i.e. (a,b)′=σ(b,a)(a,b)'=\sigma(b,a), so Ψ(t)=eiπktH(t)\Psi(t)=e^{i\pi kt}H(t) with H(t)=\exp(\sigma t\begin{psmallmatrix}0&1\\1&0\end{psmallmatrix}). Ψ(1)=(−1)kH(1)\Psi(1)=(-1)^kH(1) has eigenvalues (−1)ke±σ≠1(-1)^ke^{\pm\sigma}\ne1: nondegenerate ✓. ρ^(Ψ(t))=eiπkt\hat\rho(\Psi(t))=e^{i\pi kt} (rotation is C\mathbb C-linear, CH=cosh⁡(σt)IC_H=\cosh(\sigma t)I), argument change πk\pi k. kk even: Ψ(1)\Psi(1) positive hyperbolic, extend to W−W^- with constant ρ^\hat\rho. kk odd: Ψ(1)=−H(1)\Psi(1)=-H(1), extend by −H(s)-H(s), s:1→0s:1\to0, to W+=−IW^+=-I, ρ^≡−1\hat\rho\equiv-1. Total πk\pi k, so 2πk=2πμ2\pi k=2\pi\mu, μ=k\mu=k ✓. Statement true and not vacuous.

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