The change of argument along a path in $S^1$ is invariant under homotopies fixing the endpoints

Let $H:[0,1]\times[0,1]\to\mathbb C$ be continuous with $|H(s,t)|=1$ for all $(s,t)$, and suppose that $H(s,0)=H(0,0)$ and $H(s,1)=H(0,1)$ for all $s$. Let $\theta,\theta':[0,1]\to\mathbb R$ be continuous with $H(0,t)=e^{i\theta(t)}$ and $H(1,t)=e^{i\theta'(t)}$ for all $t$. Then

So the total change of argument of a path in $S^1$ depends only on its homotopy class relative to the endpoints. It is used for paths $t\mapsto\hat\rho(\psi(t))$ in the definitions of the Conley–Zehnder and Maslov indices.

Formalization note: the first coordinate of H : C(unitInterval × unitInterval, ℂ) is the homotopy parameter $s$; "continuous argument" is the predicate IsArgLift of the definition module ConleyZehnder_Setting.