Lemma 2.1: an endpoint of the winding interval is an integer iff $\varphi(1)$ has eigenvalue $1$

Proved

HryniewiczCriterion.winding_interval_frontier_integer_iff

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

contact-geometrydynamical-systemssymplectic-geometry

Let $\varphi:[0,1]\to Sp(1)$ be a smooth path of $2\times2$ real matrices with $\det\varphi(t)=1$ and $\varphi(0)=I$ , and let $I(\varphi)=[a,b]$ be its winding interval (total rotations of the vectors $e^{is}$ , in turns). Then

\partial I(\varphi)\cap\mathbb{Z}\neq\emptyset\iff\det\big(\varphi(1)-I\big)=0,

that is, an endpoint $a$ or $b$ of the winding interval is an integer exactly when $1$ is an eigenvalue of $\varphi(1)$ , i.e. $\varphi\notin\Sigma^*(1)$ .

This identifies degenerate paths with paths whose winding interval has an integer endpoint. It is the basis of the formula for the Conley–Zehnder index by winding intervals and of its lower semicontinuous extension to degenerate paths.

Formalization Note Smoothness is asked for the entries $t\mapsto\varphi(t)_{ij}$ on $[0,1]$ .

Preamble

import Definitions.Def_HryniewiczCriterion_ConleyZehnder

open scoped ContDiff

Formal statement

namespace HryniewiczCriterion

/-- Hryniewicz, Lemma 2.1: for a smooth path `φ : [0, 1] → Sp(1)` with `φ(0) = I`,
an endpoint of the winding interval `I(φ)` is an integer iff `φ(1)` has eigenvalue `1`. -/
theorem winding_interval_frontier_integer_iff (φ : ℝ → 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) :
    (∃ k : ℤ, sInf (windingInterval φ) = k ∨ sSup (windingInterval φ) = k) ↔
      (φ 1 - 1).det = 0 := by sorry

end HryniewiczCriterion

Source

Hryniewicz, Systems of global surfaces of section for dynamically convex Reeb flows on the 3-sphere, J. Symplectic Geom. 12 (2014) 791-862, https://arxiv.org/abs/1105.2077, Section 2.1.1, Lemma 2.1, p. 6

Read-back

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

Read-back. Let $\varphi : \mathbb{R} \to \mathbb{R}^{2\times 2}$ be any function assigning a real $2\times 2$ matrix to every real number $t$ . The hypotheses are:

(smoothness) the map $t \mapsto \varphi(t)$ , viewed as a map into the four matrix entries, is $C^\infty$ on the closed interval $[0,1]$ (in the sense of smoothness on a set, i.e. "ContDiffOn"); nothing is assumed about $\varphi(t)$ for $t \notin [0,1]$ ;
(determinant one) $\det \varphi(t) = 1$ for every $t \in [0,1]$ ;
(starts at identity) $\varphi(0) = I$ , the $2\times 2$ identity matrix.

The winding set. Write $v(s) = (\cos s, \sin s)$ . Define $W(\varphi) \subseteq \mathbb{R}$ as the set of all real numbers $d$ for which there exist a starting angle $s \in [0, 2\pi]$ (both endpoints allowed) and a function $\theta : \mathbb{R} \to \mathbb{R}$ such that

$\theta$ is continuous on $[0,1]$ ,
$\theta(0) = s$ ,
for every $t \in [0,1]$ there is a real $r > 0$ with $\varphi(t)\, v(s) = r\, v(\theta(t))$ (the image of the fixed unit vector $v(s)$ under $\varphi(t)$ is a positive multiple of the unit vector at angle $\theta(t)$ ),

and

d = \frac{\theta(1) - s}{2\pi}.

So $W(\varphi)$ collects the normalized total rotation angles, over $t \in [0,1]$ , of the vectors $\varphi(t)v(s)$ , measured by a continuous angle lift starting at $s$ , for all starting angles $s \in [0,2\pi]$ . Values of $\theta$ outside $[0,1]$ play no role. Under the hypotheses, $\varphi(t)$ is invertible for $t \in [0,1]$ , so $\varphi(t)v(s) \neq 0$ there.

Conclusion (an equivalence).

\Bigl(\exists k \in \mathbb{Z} :\ \inf W(\varphi) = k \ \text{ or } \ \sup W(\varphi) = k\Bigr) \iff \det\bigl(\varphi(1) - I\bigr) = 0 .

That is: the infimum of $W(\varphi)$ or the supremum of $W(\varphi)$ is an integer if and only if $1$ is an eigenvalue of the endpoint matrix $\varphi(1)$ (equivalently, $\det(\varphi(1)-I)=0$ ). Both directions are asserted.

Edge cases and conventions. $\inf$ and $\sup$ are the real-number infimum/supremum with the convention that the infimum (resp. supremum) of an empty set, or of a set unbounded below (resp. above), is $0$ ; with that convention $0$ is an integer, so if $W(\varphi)$ were empty or unbounded the left-hand side would hold automatically. The hypotheses constrain $\varphi$ only on $[0,1]$ , and the conclusion involves only $\varphi$ on $[0,1]$ (through $W$ ) and $\varphi(1)$ . The integer $k$ is a single integer equal to whichever of $\inf W$ or $\sup W$ is chosen; it is not required that both be integers.

Human review

Endorsed by Shuze Chen · Oct 6, 2026
Confirmed by the moderator at approval.
Endorsed by Mazecto · Oct 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Lemma 2.1: an endpoint of the winding interval is an integer iff φ(1)\varphi(1)φ(1) has eigenvalue 111

Lemma 2.1: an endpoint of the winding interval is an integer iff $\varphi(1)$ has eigenvalue $1$