The Conley–Zehnder index is constant along continuous families of paths in SP(n)

Let $\mathrm{SP}(n)$ be the set of continuous paths $\psi:[0,1]\to\mathrm{Sp}(2n)$ with $\psi(0)=\mathrm{Id}$ and $\det(\mathrm{Id}-\psi(1))\neq 0$ (Gutt, Definition 4), and let $\mu_{CZ}$ be the Conley–Zehnder index (Gutt, Definition 7 and Corollary 12).

Let $H:[0,1]\times[0,1]\to\mathbb R^{2n\times 2n}$ be continuous such that for every $s$ the path $t\mapsto H(s,t)$ lies in $\mathrm{SP}(n)$: every $H(s,t)$ is symplectic, $H(s,0)=\mathrm{Id}$ and $1$ is not an eigenvalue of $H(s,1)$. Then

So $\mu_{CZ}$ is invariant under continuous deformations inside $\mathrm{SP}(n)$; the endpoint $H(s,1)$ is allowed to move within the matrices without eigenvalue $1$. This is the deformation form of the homotopy property and is reused for the naturality and homotopy properties of the index.

Formalization note: IsSymplectic, czIndex and Mat n come from the definition module ConleyZehnder_Setting. The two end paths are passed as ψ₀ ψ₁ : C(unitInterval, Mat n) with ψ₀ t = H (0, t) and ψ₁ t = H (1, t).