A family of fundamental-solution paths in $SP(n)$ yields a family of nondegenerate asymptotic operators

Let $S_0,S_1:\mathbb R\to\mathbb R^{2n\times2n}$ be continuous $1$-periodic loops of symmetric matrices whose asymptotic operators $-J_0\partial_t-S_0$ and $-J_0\partial_t-S_1$ are nondegenerate, and let $\Psi_0,\Psi_1$ be their fundamental solutions: $\Psi_i(0)=\mathrm{Id}$ and $\Psi_i'=J_0S_i\Psi_i$ on $\mathbb R$. Suppose there is a continuous map $G:[0,1]\times[0,1]\to\mathbb R^{2n\times2n}$ with

such that for every $s\in[0,1]$ the path $G(s,\cdot)$ takes values in $\mathrm{Sp}(2n,\mathbb R)$, starts at $\mathrm{Id}$, and $1$ is not an eigenvalue of $G(s,1)$. Then there is a continuous family $(S_\tau)_{\tau\in[0,1]}$ of continuous $1$-periodic loops of symmetric matrices from $S_0$ to $S_1$ such that every $-J_0\partial_t-S_\tau$ is nondegenerate.

This passes from the classification of paths in $SP(n)$ to the classification of nondegenerate asymptotic operators on the trivial bundle (Wendl, Theorem 3.34): a joining of the time-$[0,1]$ fundamental-solution paths through nondegenerate symplectic arcs produces a joining of the operators through nondegenerate ones.

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 loops satisfy IsSymLoop and IsNondegenerate, and the fundamental solutions IsFundamentalSolution S₀ Ψ₀, IsFundamentalSolution S₁ Ψ₁. The given family is G : C(unitInterval × unitInterval, Mat n) with G (0, t) = Ψ₀ t, G (1, t) = Ψ₁ t, IsSymplectic (G (s, t)), G (s, 0) = 1 and (1 - G (s, 1)).det ≠ 0. The conclusion has the same form as Theorem 3.34: a continuous H : C(unitInterval × ℝ, Mat n) with H (0, t) = S₀ t, H (1, t) = S₁ t, and IsSymLoop, IsNondegenerate for every slice fun t => H (τ, t).