Constant loops c·I with 0 < c < 2π are nondegenerate

Proved

FiniteEnergyPlane.isNondegenerate_const_smul_one

by Mazecto · Nov 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

conley-zehnder-indexpseudoholomorphic-curvessymplectic-geometry

Let $m \in \mathbb{N}$ and $0 < c < 2\pi$ . The constant loop $S(t) = c\,\mathbb{1}$ of real $2m\times 2m$ matrices is a symmetric loop (IsSymLoop) and is nondegenerate (IsNondegenerate: the time-one map $\Psi(1)$ of the fundamental solution of $\dot\Psi = J_0 S \Psi$ , $\Psi(0) = \mathbb{1}$ , has no eigenvalue $1$ ).

Role. Supplies a family of explicit nondegenerate asymptotic operators, for instance as end-points or reference operators in index computations for Cauchy-Riemann type operators on the cylinder.

Preamble

import Definitions.Def_CauchyRiemannIndex_Setting
import Mathlib.Analysis.Calculus.ContDiff.Basic

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology Set CauchyRiemannIndex
open scoped ContDiff ENNReal Real

/-- For `c ∈ (0, 2π)`, the constant loop `t ↦ c • 1` of `2m × 2m` matrices is a symmetric loop and
is nondegenerate. -/
theorem isNondegenerate_const_smul_one (m : ℕ) (c : ℝ) (hc : c ∈ Ioo 0 (2 * π)) :
    IsSymLoop (fun _ : ℝ => c • (1 : Mat m)) ∧ IsNondegenerate (fun _ : ℝ => c • (1 : Mat m)) := by
  sorry

end FiniteEnergyPlane

Source

Setting of C. Wendl, Lectures on Holomorphic Curves in Symplectic and Contact Geometry (arXiv:1011.1690), Ch. 4

View graph