Symplectic loops along which $\hat\rho$ has degree zero are contractible

Let $\varphi:[0,1]\to\mathrm{Sp}(2n,\mathbb R)$ be a continuous loop with $\varphi(0)=\varphi(1)=\mathrm{Id}$, and let $\hat\rho:\mathrm{Sp}(2n,\mathbb R)\to S^1$ be the map $\hat\rho(A)=\det_{\mathbb C}C_A/|\det_{\mathbb C}C_A|$, where $C_A=\tfrac12(A-J_0AJ_0)$ is the complex linear part of $A$. Suppose that a continuous argument $\theta:[0,1]\to\mathbb R$ of $\hat\rho\circ\varphi$, i.e. $\hat\rho(\varphi(t))=e^{i\theta(t)}$, satisfies

Then there is a continuous map $\Phi:[0,1]\times[0,1]\to\mathrm{Sp}(2n,\mathbb R)$ with

In other words, a loop in $\mathrm{Sp}(2n,\mathbb R)$ based at the identity whose Maslov index $\deg(\hat\rho\circ\varphi)$ vanishes is null-homotopic relative to the base point; equivalently, the Maslov index is injective on $\pi_1(\mathrm{Sp}(2n,\mathbb R),\mathrm{Id})$.

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; IsSymplectic A is membership in Matrix.symplecticGroup. $\hat\rho$ is rhoHat and the argument condition is IsArgLift (fun t => rhoHat (φ t)) θ from the setting definitions (continuity of θ and rhoHat (φ t) = exp (θ t * I)). The homotopy is Φ : C(unitInterval × unitInterval, Mat n) with IsSymplectic (Φ (s, t)) for all $s,t$.