One eigenvector's winding determines the eigenvalue's winding

Let $S=H^{-1}(1)\subset\mathbb{R}^4$ be a strictly star-shaped level with contact structure $\xi$, let $J$ be a $d\lambda_0$-compatible complex structure on $\xi$, and let $P=(x,T)$ be a periodic Reeb orbit on $S$ (not necessarily nondegenerate) with asymptotic operator $A_P$. If $v$ is an eigenvector of $A_P$ with eigenvalue $\mu$ whose winding number in Hryniewicz's global frame of $\xi$ is $k$, then $\mu$ has eigenvector winding $k$: every eigenvector of $A_P$ with eigenvalue $\mu$ has winding number $k$ in the global frame.

So the winding of a single eigenvector determines the winding attached to its eigenvalue. This is what is needed to compare the asymptotic winding $\mathrm{wind}_\infty$ of a finite-energy curve with the numbers $\alpha^\pm(P)$.

Formalization Note "$v$ is an eigenvector with eigenvalue $\mu$" is IsAsymptoticEigen J P μ v; its winding in the global frame is HasXiLoopWind P v k; the conclusion HasEigenWind J P μ k says that some eigenvector for $\mu$ exists and every one has winding $k$.