The index threshold three is equivalent to winding strictly above one

Proved

HryniewiczCriterion.czIndexOfPath_ge_three_iff

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

differential-calculussymplectic-geometry

Suppose the winding set of a matrix path is $[a,b]$ , with $a\le b$ and $b-a<1$ . Then the lower semicontinuous index defined from its endpoints satisfies $\mu\ge3$ if and only if every element of the winding set is strictly greater than $1$ . This includes integer endpoints and needs no regularity assumption beyond the stated interval description.

Preamble

import Definitions.Def_HryniewiczCriterion_ConleyZehnder

open HryniewiczCriterion
open scoped ContDiff

Formal statement

theorem HryniewiczCriterion.czIndexOfPath_ge_three_iff (φ : ℝ → Matrix (Fin 2) (Fin 2) ℝ) (a b : ℝ)
    (hab : a ≤ b) (hw : windingInterval φ = Set.Icc a b) (hwidth : b - a < 1) :
    3 ≤ czIndexOfPath φ ↔ ∀ d ∈ windingInterval φ, 1 < d := 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