Along paths in $\mathrm{Sp}^*(2n)$ the increment of $\arg\hat\rho$ depends only on the endpoints

Let $\mathrm{Sp}^*(2n)$ be the set of real symplectic $2n\times 2n$ matrices without eigenvalue $1$, and let $\hat\rho(A)=\det_{\mathbb C}C_A/|\det_{\mathbb C}C_A|$ be the normalized complex determinant of the $\mathbb C$-linear part $C_A=\tfrac12(A-J_0AJ_0)$.

Let $\chi,\chi':[0,1]\to\mathrm{Sp}^*(2n)$ be continuous paths with $\chi(0)=\chi'(0)$ and $\chi(1)=\chi'(1)$, and let $\theta,\theta':[0,1]\to\mathbb R$ be continuous with $\hat\rho(\chi(t))=e^{i\theta(t)}$ and $\hat\rho(\chi'(t))=e^{i\theta'(t)}$ for all $t$. Then

This is the uniqueness half of the definition of the Conley–Zehnder index: the degree $\deg(\hat\rho^2\circ\tilde\psi)$ does not depend on the chosen extension $\tilde\psi$ of $\psi\in\mathrm{SP}(n)$ through $\mathrm{Sp}^*(2n)$.

Formalization note: paths are C(unitInterval, Mat n); "continuous argument" is the predicate IsArgLift of the definition module ConleyZehnder_Setting, and $\hat\rho$ is rhoHat. The statement is about arbitrary continuous arguments of $\hat\rho\circ\chi$ and $\hat\rho\circ\chi'$.