The winding set of a normalized symplectic plane path is a narrow closed interval

Proved

HryniewiczCriterion.windingInterval_narrow

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

differential-calculussymplectic-geometry

For a smooth determinant-one plane path starting at the identity, its winding set is a nonempty closed interval $[a,b]$ with $b-a<1/2$ . Endpoint degeneracy is allowed.

Preamble

import Definitions.Def_HryniewiczCriterion_ConleyZehnder

open HryniewiczCriterion
open scoped ContDiff

Formal statement

theorem HryniewiczCriterion.windingInterval_narrow (φ : ℝ → Matrix (Fin 2) (Fin 2) ℝ)
    (hφ : ContDiffOn ℝ ∞ (fun t i j => φ t i j) (Set.Icc 0 1))
    (hsymp : ∀ t ∈ Set.Icc (0 : ℝ) 1, (φ t).det = 1)
    (h0 : φ 0 = 1) :
    ∃ a b : ℝ, a ≤ b ∧ windingInterval φ = Set.Icc a b ∧ b - a < 1 / 2 := by sorry

Source

Hryniewicz, https://arxiv.org/html/1105.2077v5#S2.SS1.SSS1, Section 2.1.1, pp. 5–6, the winding interval and equations (4)–(5).

View graph