Zero ρ̂-winding along Sp* paths between symmetric matrices

Let $\mathrm{Sp}^*(2n)$ be the set of real symplectic $2n\times 2n$ matrices $A$ ($AJ_0A^{T}=J_0$) 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 complex-linear part $C_A=\tfrac12(A-J_0AJ_0)$ (Gutt, formula (9)).

Let $\chi:[0,1]\to\mathrm{Sp}^*(2n)$ be a continuous path whose endpoints are symmetric matrices, $\chi(0)^{T}=\chi(0)$ and $\chi(1)^{T}=\chi(1)$. Then every continuous function $\theta:[0,1]\to\mathbb R$ with $\hat\rho(\chi(t))=e^{i\theta(t)}$ for all $t$ satisfies

The matrices $W^{\pm}$ that normalize the Conley–Zehnder index, and all real diagonal symplectic matrices, are symmetric. So the statement says that a path in $\mathrm{Sp}^*$ joining such normal forms contributes nothing to the index. This is useful when an extension of a path in $\mathrm{SP}(n)$ has to be continued from one diagonal normal form to $W^{\pm}$, as for the product property (Gutt, Proposition 8 (4)).

Formalization note: SpStar, rhoHat, IsArgLift and Mat n come from the definition module ConleyZehnder_Setting; paths are C(unitInterval, Mat n), and IsArgLift f θ means that θ is continuous with f t = exp(i θ t). Symmetry is Mᵀ = M.