Winding of $\pi\partial_s u$ along one circle versus in cylindrical coordinates at $\infty$

Let $S=H^{-1}(1)\subset\mathbb{R}^4$ be a strictly star-shaped level, $J$ a $d\lambda_0$-compatible complex structure on $\xi$, and $\tilde J$ the induced almost complex structure on $\mathbb{R}^4\setminus\{0\}\cong\mathbb{R}\times S$. Let $U\subset\mathbb{C}$ be open, $u$ smooth, nonvanishing and $\tilde J$-holomorphic on $U$, and $s\in\mathbb{R}$ such that the circle $|z|=e^{2\pi s}$ lies in $U$. Suppose that the $\xi$-component $\pi\,\partial_s u$, read in Hryniewicz's global frame of $\xi$, has winding number $k$ along $t\mapsto e^{2\pi s}e^{2\pi it}$. Then the loop $t\mapsto\pi\partial_s w(s,t)$ of $w=\mathrm{pr}\circ u\circ\mathrm{cylInf}$, in the cylindrical coordinates $(s,t)\mapsto e^{2\pi(s+it)}$ at $\infty$, has winding number $k+1$ in the same frame.

This compares the two natural loops attached to a single circle: the section read in the plane coordinate $z$ and the same section read in cylindrical coordinates. It holds at each individual radius, with no condition on the other circles.

Formalization Note $\mathbb{R}^4$ is V 1, $\tilde J$ is Jtilde H J, and $\pi\partial_s u$ in the global frame is piDs H u : ℂ → ℂ. The circle is ccwLoop (Real.exp (2 * π * s)) t. The hypothesis HasLoopWind includes that piDs H u has no zero on the circle. No energy bound or asymptotic hypothesis is assumed.