The constant loop π·Id gives a nondegenerate asymptotic operator in every dimension

Proved

CauchyRiemannIndex.isNondegenerate_pi_smul_one

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

conley-zehnder-indexodesymplectic-geometry

Let $m\ge0$ . The constant loop $S_\infty(t)=\pi\,\mathrm{Id}$ on $\mathbb{R}^{2m}$ is a continuous $1$ -periodic loop of symmetric matrices, and its asymptotic operator $-J_0\partial_t-\pi$ is nondegenerate: the fundamental solution $\Psi$ of $\Psi'=J_0\pi\Psi$ , $\Psi(0)=\mathrm{Id}$ , has no eigenvalue $1$ at $t=1$ .

This gives a nondegenerate reference loop in every dimension.

Formalization Note Loops are IsSymLoop and nondegeneracy is IsNondegenerate (for every fundamental solution $\Psi$ , $\det(\mathrm{Id}-\Psi(1))\neq0$ ), from the setting module.

Preamble

import Definitions.Def_CauchyRiemannIndex_Setting

Formal statement

namespace CauchyRiemannIndex

open MeasureTheory Matrix Filter Topology
open scoped ENNReal NNReal ContDiff RealInnerProductSpace

/-- The constant loop `S∞ ≡ π · Id` on `ℝ^{2m}` is a loop of symmetric matrices whose asymptotic
operator `-J₀ ∂ₜ - π` is nondegenerate. -/
theorem isNondegenerate_pi_smul_one (m : ℕ) :
    IsSymLoop (fun _ : ℝ => Real.pi • (1 : Mat m)) ∧
      IsNondegenerate (fun _ : ℝ => Real.pi • (1 : Mat m)) := by
  sorry

end CauchyRiemannIndex

Source

C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lecture 3, §3.4 (nondegenerate asymptotic operators)

View graph