The $\hat\rho$-increment along symplectic paths is invariant under homotopy rel end points

Let $\Phi:[0,1]\times[0,1]\to\mathrm{Sp}(2n,\mathbb R)$ be continuous with $\Phi(s,0)=\Phi(0,0)$ and $\Phi(s,1)=\Phi(0,1)$ for all $s$, and let $\hat\rho:\mathrm{Sp}(2n,\mathbb R)\to S^1$ is 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$ (Gutt, eq. (9)). If $\theta,\theta':[0,1]\to\mathbb R$ are continuous arguments of $t\mapsto\hat\rho(\Phi(0,t))$ and $t\mapsto\hat\rho(\Phi(1,t))$, i.e. $\hat\rho(\Phi(0,t))=e^{i\theta(t)}$ and $\hat\rho(\Phi(1,t))=e^{i\theta'(t)}$, then

So the total change of the argument of $\hat\rho$ along a path of symplectic matrices depends only on the homotopy class of the path relative to its end points; in particular the Maslov index $\deg(\hat\rho\circ\varphi)$ of a loop is a homotopy invariant (Gutt, §2; Wendl, Lecture 3, §3.4).

Formalization Note. $\mathbb R^{2n\times2n}$ is Mat n (real matrices indexed by Fin n ⊕ Fin n, first block $q$, second block $p$) and $J_0=\begin{pmatrix}0&-\mathrm{Id}\\ \mathrm{Id}&0\end{pmatrix}$ is Matrix.J; IsSymplectic A is membership in Matrix.symplecticGroup. Vectors of $\mathbb R^{2n}$ are functions Fin n ⊕ Fin n → ℝ and $Av$ is A *ᵥ v. $\hat\rho$ is rhoHat and the argument conditions are IsArgLift (fun t => rhoHat (Φ (0, t))) θ and IsArgLift (fun t => rhoHat (Φ (1, t))) θ' from the setting definitions.