Every Hamiltonian matrix without eigenvalue $1$ is joined, avoiding eigenvalue $1$, to a Hamiltonian $Y$ with $Y^3=9Y$

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}$.

For every $X\in\mathcal H^*(2n)$ there exist a Hamiltonian matrix $Y$ with $Y^3=9Y$ and a continuous path $[0,1]\to\mathcal H^*(2n)$ from $X$ to $Y$. (Such a $Y$ automatically lies in $\mathcal H^*(2n)$.)

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.