A Hamiltonian matrix $Y$ with $Y^3=9Y$ is joined, avoiding eigenvalue $1$, to $0$ or to $\mathrm{diag}(3,0,\dots,0,-3,0,\dots,0)$

Let $J_0=\begin{pmatrix}0&-\mathrm{Id}\ \mathrm{Id}&0\end{pmatrix}$ and call a real $2n\times 2n$ matrix $X$ Hamiltonian if $XJ_0+J_0X^{T}=0$. Let $\mathcal H^*(2n)$ be the set of Hamiltonian matrices $X$ such that $1$ is not an eigenvalue of $X$, i.e. $\det(\mathrm{Id}-X)\neq 0$, with the topology of $\mathbb R^{2n\times 2n}$.

Let $Y$ be a Hamiltonian matrix with $Y^3=9Y$. Then there is a continuous path $[0,1]\to\mathcal H^*(2n)$ from $Y$ to $0$ or to $Y_-=\mathrm{diag}(3,0,\dots,0,-3,0,\dots,0)$, the diagonal matrix with entry $3$ at the first coordinate of the first block, $-3$ at the first coordinate of the second block, and $0$ elsewhere.

Together with its companion statement, this shows that every element of $\mathcal H^*(2n)$ lies in the path component of $0$ or of $\mathrm{diag}(3,0,\dots,0,-3,0,\dots,0)$ in $\mathcal H^*(2n)$. It serves the description of the path components of $\mathrm{Sp}^*(2n)$ used in the definition of the Conley–Zehnder index.

Formalization note: Mat n is the type of real matrices indexed by Fin n ⊕ Fin n and J₀ n is Mathlib's Matrix.J, both from the definition module ConleyZehnder_Setting; the set $\mathcal H^*(2n)$ is written inline, and "joined by a continuous path inside a set" is Mathlib's JoinedIn. For $n=0$ the statement is trivial.