Read-back: FiniteEnergyPlane.hasLoopWind_cylInf_eq_windInf_sub

Ambient notation. Work in $V = \mathbb{R}^4$ with coordinates $y_0, y_1, y_2, y_3$ (the statement is for dimension $2(n+1)$ with $n = 1$). Let $\omega_0(u,v) = u_0 v_1 - u_1 v_0 + u_2 v_3 - u_3 v_2$, $\lambda_x(v) = \tfrac12 \omega_0(x, v)$, $X_H = j_0 \nabla H$ where $(\nabla H(x))_k = dH_x(e_k)$ and $j_0(v) = (-v_1, v_0, -v_3, v_2)$, and the Reeb field $R_H(x) = \lambda_x(X_H(x))^{-1} X_H(x)$ (with $0^{-1} = 0$). Write $\xi_x = \{ v : \lambda_x(v) = 0,\ dH_x(v) = 0\}$ and $S_H = \{ H = 1 \}$.

• Hypothesis on $H$ ("strictly star-shaped level"): $H$ is $C^\infty$; every $u \ne 0$ has exactly one $r > 0$ with $H(ru) = 1$; and $dH_x(x) > 0$ whenever $H(x) = 1$.
• Hypothesis on $J$ ("compatible $\xi$-structure"): $J : V \to \mathrm{End}(V)$ is $C^\infty$ and for $x \in S_H$, $v, w \in \xi_x$: $J(x)v \in \xi_x$, $J(x)^2 v = -v$, $\omega_0(v, J(x) v) > 0$ if $v \ne 0$, $\omega_0(J(x)v, J(x)w) = \omega_0(v,w)$.
• Scaling, projection, $a$-coordinate. $s_H(y)$ is some $r > 0$ with $H(ry) = 1$ if one exists (chosen by choice), otherwise $1$; $\pi_H(y) = s_H(y)\, y$; $a_H(y) = -\tfrac12 \log s_H(y)$.
• $\tilde J$: for $y \in V$, with $x = \pi_H(y)$, $r = s_H(y)$, $\alpha(v) = \frac{r\, dH_x(v)}{2 dH_x(x)}$, $\beta(v) = r\lambda_x(v)$, $w(v) = v - 2\alpha(v) y - \beta(v) r^{-1} R_H(x)$: $\ \tilde J(y)v = \alpha(v) r^{-1} R_H(x) - 2\beta(v) y + J(x) w(v)$.
• Derivatives. For $f$ on $\mathbb{C}$: $\partial_s f(z) = Df(z)[1]$, $\partial_t f(z) = Df(z)[i]$ (real Fréchet derivative, $0$ where not differentiable).
• Energy. Admissible $\varphi$: $C^\infty$, non-decreasing, values in $[0,1]$. With $a = a_H \circ u$, $w = \pi_H \circ u$, $e_\varphi = \varphi'(a)(\partial_s a\, \lambda_w(\partial_t w) - \partial_t a\, \lambda_w(\partial_s w)) + \varphi(a)\, \omega_0(\partial_s w, \partial_t w)$, and $E_H(U,u) = \sup_\varphi \int_U \max(e_\varphi, 0) \in [0,\infty]$.
• Finite-energy curve on $U$: $u$ is $C^\infty$ on $U$, nonvanishing on $U$, at each $z \in U$ differentiable with $\partial_s u + \tilde J(u)\, \partial_t u = 0$, and $E_H(U,u) < \infty$.
• Reeb orbit $P$: a map $x_P : \mathbb{R} \to V$ and $T_P > 0$ with $x_P(\tau) \in S_H$, $x_P' = R_H(x_P)$, $x_P(\tau + T_P) = x_P(\tau)$ (any period, not necessarily minimal).
• $\xi$-coordinates. With $Q_1 x = (-x_2, x_3, x_0, -x_1)$, $Q_2 x = (x_3, x_2, -x_1, -x_0)$, $|x|$ the Euclidean norm and

$$F_j(x) = |x|^{-1}\Big(Q x - \frac{dH_x(Qx)}{dH_x(x)}\, x\Big), \quad Q = Q_2 \text{ for } j = 1,\ Q = Q_1 \text{ for } j = 2$$

(division by $0$ read as multiplication by $0$), the complex coordinate of $v$ at $x$ is

$$\zeta_x(v) = \omega_0\big(v, F_2(x)\big) + i\, \omega_0\big(F_1(x), v\big) \in \mathbb{C}.$$

• $\xi$-projection: $\pi^\xi_x(v) = v - \lambda_x(v)\, R_H(x)$.
• $\pi\, du\, \partial_s$ in coordinates: for $u : \mathbb{C} \to V$ and $z \in \mathbb{C}$, with $p = \pi_H(u(z))$,

$$\Pi_u(z) = \zeta_p\Big(\pi^\xi_p\big(\partial_s(\pi_H \circ u)(z)\big)\Big) \in \mathbb{C}.$$

• Cylindrical end at infinity: $e_\infty(s,t) = e^{2\pi s} e^{2\pi i t}$. Put $W(s,t) = \pi_H(u(e_\infty(s,t)))$ and $A(s,t) = a_H(u(e_\infty(s,t)))$, and $\partial_s W(s,t) = DW(s,t)[(1,0)]$ (derivative of $W : \mathbb{R}^2 \to V$; $0$ where not differentiable).
• Nondegenerate end (with sign $1$) of $u$ at $e_\infty$ asymptotic to $P$: there are $d, c \in \mathbb{R}$ and $b > 0$ with

$$\sup_t |A(s,t) - T_P\, s - d| \to 0, \qquad \sup_t e^{bs}\, \big|W(s,t) - x_P(T_P t + c)\big| \to 0 \quad (s \to +\infty).$$

(Both are stated as: for every $\varepsilon > 0$ there is $s_0$ with the quantity $\le \varepsilon$ for all $s \ge s_0$ and all real $t$.)

• Loop winding $\mathrm{wind}(f) = k$, for $f : \mathbb{R} \to \mathbb{C}$ and $k \in \mathbb{Z}$: $f$ is continuous, $1$-periodic, never $0$, and there is a continuous $\theta : \mathbb{R} \to \mathbb{R}$ with $f(t) = |f(t)|\, e^{i\theta(t)}$ for all $t$ and $\theta(1) - \theta(0) = 2\pi k$.
• Zero index of $f : \mathbb{C} \to \mathbb{C}$ at $z_0$ equal to $m \in \mathbb{Z}$: $f(z_0) = 0$, and there is $r > 0$ such that $f(z) \ne 0$ for all $z$ with $0 < |z - z_0| \le r$, and for every $\rho \in (0, r)$ the loop $t \mapsto f(z_0 + \rho e^{2\pi i t})$ has winding $m$.
• Winding at infinity $= k$ (for sign $1$): there is $s_1$ such that for every $s \ge s_1$ the loop

$$t \mapsto \zeta_{W(s,t)}\big(\pi^\xi_{W(s,t)}(\partial_s W(s,t))\big)$$

has winding $k$.

Statement. Let $H : \mathbb{R}^4 \to \mathbb{R}$ be a strictly star-shaped level function and $J$ a compatible $\xi$-structure. Let $\Gamma \subset \mathbb{C}$ be a finite set (possibly empty), $u : \mathbb{C} \to \mathbb{R}^4$ a finite-energy curve on $\mathbb{C} \setminus \Gamma$, and $P_\infty$ a Reeb orbit such that $u$ has a nondegenerate end (sign $1$) at $e_\infty$ asymptotic to $P_\infty$. Assume $\Pi_u(z) \ne 0$ for at least one $z \notin \Gamma$. Let $k \in \mathbb{Z}$ be such that the winding of $u$ at infinity is $k$ in the sense above. Let $s_0 \in \mathbb{R}$, set $R_0 = e^{2\pi s_0}$, and assume

• every $z \in \Gamma$ satisfies $|z| < R_0$;
• $\Pi_u(z) \ne 0$ for every $z$ with $|z| = R_0$.

Then there exist a finite set $Z \subset \mathbb{C}$ and a function $\mathrm{idx} : \mathbb{C} \to \mathbb{Z}$ such that

1. $Z = \{ z \in \mathbb{C} : |z| > R_0,\ \Pi_u(z) = 0 \}$ (in particular this set is finite);
2. for every $z \in Z$, $\Pi_u$ has zero index $\mathrm{idx}(z)$ at $z$;
3. the loop at the fixed level $s_0$,

$$t \mapsto \zeta_{W(s_0,t)}\big(\pi^\xi_{W(s_0,t)}(\partial_s W(s_0,t))\big), \qquad W(s_0,t) = \pi_H\big(u(R_0 e^{2\pi i t})\big),$$

has winding exactly

$$k - \sum_{z \in Z} \mathrm{idx}(z).$$

Remarks on the literal content. $s_0$ is any real number satisfying the two displayed conditions; it is not required to be at least the threshold $s_1$ from the winding-at-infinity hypothesis. Conclusion 3 includes the assertion that this loop is continuous, $1$-periodic and nowhere zero. The zero set $Z$ is taken over the whole exterior region $|z| > R_0$, which lies in $\mathbb{C} \setminus \Gamma$ by the first assumption. $\Pi_u$ is defined through total functions: at points where $u$ or $\pi_H \circ u$ is not differentiable the derivative entering $\Pi_u$ is $0$.