Paths in $SP(n)$ with the same Conley–Zehnder index are joined inside $SP(n)$

Let $SP(n)$ be the set of continuous paths $\psi:[0,1]\to\mathrm{Sp}(2n,\mathbb R)$ with $\psi(0)=\mathrm{Id}$ such that $1$ is not an eigenvalue of $\psi(1)$, and let $\mu_{CZ}:SP(n)\to\mathbb Z$ be the Conley–Zehnder index. If $\psi_0,\psi_1\in SP(n)$ satisfy

then there is a continuous map $G:[0,1]\times[0,1]\to\mathbb R^{2n\times2n}$ with $G(0,\cdot)=\psi_0$, $G(1,\cdot)=\psi_1$ and $G(s,\cdot)\in SP(n)$ for every $s\in[0,1]$.

Together with the homotopy invariance of the index, this is the classical statement that the Conley–Zehnder index classifies the path components of $SP(n)$ (the homotopy classes of nondegenerate symplectic arcs; Wendl, Lecture 3, p. 62).

Formalization Note. $\mathbb R^{2n\times2n}$ is Mat n (real matrices indexed by Fin n ⊕ Fin n) and $J_0=\begin{pmatrix}0&-\mathrm{Id}\\ \mathrm{Id}&0\end{pmatrix}$ is Matrix.J. The paths are ψ₀ ψ₁ : C(unitInterval, Mat n); membership in $SP(n)$ is written out as ∀ t, IsSymplectic (ψ t), ψ 0 = 1 and (1 - ψ 1).det ≠ 0, and the index is czIndex from the setting definitions (Gutt, Definition 7, chosen with fallback $0$). The family is G : C(unitInterval × unitInterval, Mat n); the conditions on each $G(s,\cdot)$ are stated pointwise in the same form.