Prove2Me

The Conley–Zehnder index of the conjugate asymptotic operator

Proved
CauchyRiemannIndex.asymptoticCZIndex_conj

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

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

Let SS be a continuous loop of symmetric matrices whose asymptotic operator A=−J0∂t−SA=-J_0\partial_t-S is nondegenerate, and let CC be complex conjugation on Cn=R2n\mathbb{C}^n=\mathbb{R}^{2n}. Then the conjugate asymptotic operator Aˉ=−J0∂t+CSC\bar A=-J_0\partial_t+CSC is nondegenerate and

μCZ(Aˉ)=−μCZ(A).\mu_{CZ}(\bar A)=-\mu_{CZ}(A).

Formalization Note CC is conjMat n and Aˉ\bar A is the asymptotic operator of the loop fun t => -(conjMat n * S t * conjMat n). In Wendl, Aˉ=−A\bar A=-A acts on the conjugate bundle and the index is taken in the conjugate trivialization; written in the original coordinates this is the operator above.

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.8 (p. 87), Conley–Zehnder part, trivial bundle: for a nondegenerate loop `S` of
symmetric matrices, the conjugate asymptotic operator `-J₀ ∂ₜ - S̄`, `S̄ = -C S C` with `C`
complex conjugation, is nondegenerate and `μ_CZ(-J₀ ∂ₜ - S̄) = -μ_CZ(-J₀ ∂ₜ - S)`. -/
theorem asymptoticCZIndex_conj (n : ℕ) (S : ℝ → Mat n) (hS : IsSymLoop S)
    (hn : IsNondegenerate S) :
    IsNondegenerate (fun t => -(conjMat n * S t * conjMat n)) ∧
      asymptoticCZIndex (fun t => -(conjMat n * S t * conjMat n)) = -asymptoticCZIndex S := 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.8, p. 87 (Conley–Zehnder part, trivial bundle)
Read-back

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

Read-back: CauchyRiemannIndex.asymptoticCZIndex_conj

Setting. n∈Nn\in\mathbb N; S:R→R2n×2nS:\mathbb R\to\mathbb R^{2n\times2n}. CC = conjMat n =diag⁡(In,−In)=\operatorname{diag}(I_n,-I_n), i.e. (x,y)↦(x,−y)(x,y)\mapsto(x,-y), complex conjugation on Cn\mathbb C^n.

Hypotheses. SS is a continuous 1-periodic loop of symmetric matrices, nondegenerate (det⁡(I−Ψ(1))≠0\det(I-\Psi(1))\ne0 for Ψ′=J0SΨ\Psi'=J_0S\Psi, Ψ(0)=I\Psi(0)=I).

Definitions used. Sˉ(t):=−(C S(t) C)\bar S(t):=-(C\,S(t)\,C). IsNondegenerate, asymptoticCZIndex as in asymptoticCZIndex_eq_iff_joined.md (Gutt's deg⁡ρ^2\deg\hat\rho^2 of the fundamental-solution path, extended in Sp∗\mathrm{Sp}^* to W±W^\pm).

Conclusion.

Sˉ is nondegenerateandμCZ(−J0∂t−Sˉ)=−μCZ(−J0∂t−S).\bar S\text{ is nondegenerate}\quad\text{and}\quad\mu_{CZ}(-J_0\partial_t-\bar S)=-\mu_{CZ}(-J_0\partial_t-S).

Degenerate cases. n=0n=0: 0=−00=-0. S=diag⁡(1,−1)S=\operatorname{diag}(1,-1) (n=1n=1): CSC=SCSC=S, Sˉ=diag⁡(−1,1)\bar S=\operatorname{diag}(-1,1), μ=0\mu=0 both, 0=−00=-0.

Remarks. Parenthesisation: -(conjMat n * S t * conjMat n) is −(CSC)-(CSC), as intended; Sˉ\bar S is again symmetric and continuous periodic.

Soundness checks.

  1. Coercions/junk: none beyond the choose fallback, which is not triggered (nondegenerate, continuous). The first conjunct is needed and asserted, so the index of Sˉ\bar S is a genuine value.
  2. Direct verification: CJ0C=−J0CJ_0C=-J_0, so Φ:=CΨC\Phi:=C\Psi C satisfies Φ′=CJ0C⋅CSC⋅Φ=J0(−CSC)Φ=J0SˉΦ\Phi'=CJ_0C\cdot CSC\cdot\Phi=J_0(-CSC)\Phi=J_0\bar S\Phi, Φ(0)=I\Phi(0)=I: the fundamental solution of Sˉ\bar S. det⁡(I−Φ(1))=det⁡(I−Ψ(1))≠0\det(I-\Phi(1))=\det(I-\Psi(1))\ne0. CC is anti-symplectic, so A↦CACA\mapsto CAC preserves Sp\mathrm{Sp} and Sp∗\mathrm{Sp}^*, fixes W±W^\pm (diagonal), and det⁡CCCAC=det⁡CCA‾\det_{\mathbb C}C_{CAC}=\overline{\det_{\mathbb C}C_A}, so ρ^(CAC)=ρ^(A)‾\hat\rho(CAC)=\overline{\hat\rho(A)} and all argument changes flip sign: μ↦−μ\mu\mapsto-\mu. Hand values: S=εIS=\varepsilon I has μ=1\mu=1; Sˉ=−εI\bar S=-\varepsilon I has Ψ\Psi = rotation by −εt-\varepsilon t, μ=−1\mu=-1. ✓. Model Sk=πkI+σ antilin(e2πikt)S_k=\pi kI+\sigma\,\mathrm{antilin}(e^{2\pi ikt}) (μ=k\mu=k): C antilin(β)C=antilin(βˉ)C\,\mathrm{antilin}(\beta)C=\mathrm{antilin}(\bar\beta), so Sˉk=−πkI+σ antilin(−e−2πikt)\bar S_k=-\pi kI+\sigma\,\mathrm{antilin}(-e^{-2\pi ikt}), a phase-rotated model with k→−kk\to-k, μ=−k\mu=-k ✓. True, 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