Definition module FiniteEnergyPlane_Winding

This module defines winding numbers of loops, eigen-winding notions for asymptotic operators, the "alpha" extremal windings, primality of a Reeb orbit, and winding/zero-counting quantities for maps from the plane, culminating in the predicate "fast plane". Throughout, $V = V_1 = \mathbb{R}^4$ (functions $\mathrm{Fin}\,4 \to \mathbb{R}$, coordinates $x_0,\dots,x_3$), and $\mathbb{R}^2$ below means the Euclidean space $\mathrm{Vec}_1$ indexed by two symbols "left" and "right", with vectors written $a = (a_L, a_R)$. Notation imported from earlier modules is recalled where used:

• $j_0(v) = (-v_1, v_0, -v_3, v_2)$ (for general $V_n$: even slot $k$ gets $-v_{k+1}$, odd slot gets $v_{k-1}$); $\omega_0(u,v) = \langle j_0 u, v\rangle = u_0v_1 - u_1v_0 + u_2v_3 - u_3v_2$; the Liouville form $\lambda_x(v) = \tfrac12\omega_0(x,v)$.
• $X_H(x) = j_0 \nabla H(x)$, and the Reeb field $R_H(x) = \lambda_x(X_H(x))^{-1} X_H(x)$ (with the convention $0^{-1} = 0$).
• $v \in \xi_x$ ("$v$ is in $\xi$ at $x$") means $\lambda_x(v) = 0$ and $dH_x(v) = 0$.
• A Reeb orbit $P$ consists of $x_P : \mathbb{R} \to V$ and a period $T_P > 0$ with $H(x_P(\tau)) = 1$, $x_P'(\tau) = R_H(x_P(\tau))$ and $x_P(\tau + T_P) = x_P(\tau)$ for all $\tau$. It is not required that $T_P$ be the minimal period.
• $J_0$ is the $2\times 2$ block matrix $\begin{pmatrix} 0 & -1 \\ 1 & 0\end{pmatrix}$, acting on $\mathbb{R}^2$ by $(a_L, a_R) \mapsto (-a_R, a_L)$.
• $\operatorname{proj}_H(y) = r(y)\,y$, where $r(y)$ is some $r > 0$ with $H(r y) = 1$ if such $r$ exists (chosen by choice), and $r(y) = 1$ otherwise; $a_H(y) = -\tfrac12 \log r(y)$.

Winding of a loop, $\mathrm{HasLoopWind}(f, k)$. For $f : \mathbb{R} \to \mathbb{C}$ and $k \in \mathbb{Z}$: $f$ is continuous, $1$-periodic, never zero, and there is a continuous $\theta : \mathbb{R} \to \mathbb{R}$ with

$$f(t) = |f(t)|\, e^{i\theta(t)} \ \text{ for all } t, \qquad \theta(1) - \theta(0) = 2\pi k.$$

$\mathrm{vecToC}$. The map $\mathbb{R}^2 \to \mathbb{C}$, $a \mapsto a_L + i\,a_R$. (Under it, $J_0$ acts as multiplication by $i$.)

$\mathrm{toR4}$, $\mathrm{ofR4}$. The identity re-indexing between $V_1 = \mathbb{R}^{\mathrm{Fin}(2\cdot 2)}$ and $\mathbb{R}^{\mathrm{Fin}\,4}$.

$\xi$-coordinates, $\mathrm{xiCoordC}(H, x, v) \in \mathbb{C}$. For $H : V \to \mathbb{R}$ and $x, v \in V$, set

$$Q_1(x) = (-x_2, x_3, x_0, -x_1), \qquad Q_2(x) = (x_3, x_2, -x_1, -x_0),$$ $$F_j(x) = |x|^{-1}\Big(Q_{j'}(x) - \frac{dH_x(Q_{j'}(x))}{dH_x(x)}\, x\Big), \quad \text{with } F_1 \text{ using } Q_2 \text{ and } F_2 \text{ using } Q_1,$$

where $|x|$ is the Euclidean norm, $|0|^{-1} = 0$ and division by $0$ gives $0$. Then

$$\mathrm{xiCoordC}(H, x, v) = \omega_0(v, F_2(x)) + i\,\omega_0(F_1(x), v).$$

No projection of $v$ onto $\xi_x$ is applied here; $v$ is arbitrary.

$\xi$-projection, $\pi_\xi(H, x, v)$ (any $n$): $\pi_\xi(H,x,v) = v - \lambda_x(v)\, R_H(x)$.

$\mathrm{HasXiLoopWind}(P, \eta, k)$. For a Reeb orbit $P$ of $H$, $\eta : \mathbb{R} \to V$, $k \in \mathbb{Z}$: the loop $t \mapsto \mathrm{xiCoordC}(H, x_P(T_P t), \eta(t))$ satisfies $\mathrm{HasLoopWind}$ with winding $k$. ($\eta$ is not required to lie in $\xi$.)

$\mathrm{HasLoopEigenWind}(S_\infty, \mu, k)$. For $S_\infty : \mathbb{R} \to \mathbb{R}^{2\times 2}$, $\mu \in \mathbb{R}$, $k \in \mathbb{Z}$: there exists at least one loop eigenfunction $e$ for $(S_\infty, \mu)$, and every loop eigenfunction $e$ for $(S_\infty, \mu)$ has $\mathrm{HasLoopWind}(\mathrm{vecToC}\circ e, k)$. Here "$e : \mathbb{R} \to \mathbb{R}^2$ is a loop eigenfunction for $(S_\infty,\mu)$" means: $e$ is $C^\infty$, $1$-periodic, not identically zero, and

$$-J_0\, e'(t) - S_\infty(t)\, e(t) = \mu\, e(t) \quad \text{for all } t.$$

If $\mu$ has no loop eigenfunction, the predicate is false for every $k$.

$\mathrm{loopEigenSpan}(S_\infty, k)$. The real linear span, inside the vector space of all functions $\mathbb{R} \to \mathbb{R}^2$, of the set of those $e$ for which there is some $\mu \in \mathbb{R}$ such that $e$ is a loop eigenfunction for $(S_\infty, \mu)$ and $\mathrm{HasLoopEigenWind}(S_\infty, \mu, k)$ holds.

$\mathrm{HasEigenWind}(J, P, \mu, k)$. For $J : V \to \mathrm{End}(V)$, a Reeb orbit $P$ of $H$, $\mu \in \mathbb{R}$, $k \in \mathbb{Z}$: there exists an asymptotic eigenvector $v$ for $(J, P, \mu)$, and every such $v$ satisfies $\mathrm{HasXiLoopWind}(P, v, k)$. "$v : \mathbb{R} \to V$ is an asymptotic eigenvector for $(J,P,\mu)$" means: $v$ is $C^\infty$, $1$-periodic, $v(t) \in \xi_{x_P(T_P t)}$ for all $t$, $v$ is not identically zero, and for all $t$

$$J\big(x_P(T_P t)\big)\Big(-v'(t) + T_P\, dR_H\big(x_P(T_P t)\big)\, v(t)\Big) = \mu\, v(t).$$

$\mathrm{IsAlphaMinus}(J, P, k)$. There is some $\mu < 0$ with $\mathrm{HasEigenWind}(J,P,\mu,k)$, and for every $\mu < 0$ and every $k' \in \mathbb{Z}$ with $\mathrm{HasEigenWind}(J,P,\mu,k')$ one has $k' \le k$. (So $k$ is the attained maximum of the windings carried by negative $\mu$.)

$\mathrm{IsAlphaPlus}(J, P, k)$. There is some $\mu \ge 0$ with $\mathrm{HasEigenWind}(J,P,\mu,k)$, and for every $\mu \ge 0$ and every $k'$ with $\mathrm{HasEigenWind}(J,P,\mu,k')$ one has $k \le k'$. (So $k$ is the attained minimum over $\mu \ge 0$; note $\mu = 0$ is included here.)

$\mathrm{IsPrime}(P)$ (any $n$): $x_P(\tau) \ne x_P(0)$ for every $\tau$ with $0 < \tau < T_P$.

$\mathrm{cylEndAt}(z_0)(s,t) \in \mathbb{C}$. $z_0 + e^{-2\pi s}\, e^{-2\pi i t}$ (a clockwise loop around $z_0$ of radius $e^{-2\pi s}$, shrinking to $z_0$ as $s \to +\infty$). For comparison, the imported $\mathrm{cylInf}(s,t) = e^{2\pi s} e^{2\pi i t}$.

$\mathrm{piDs}(H, u, z) \in \mathbb{C}$. For $u : \mathbb{C} \to V$ and $w = \operatorname{proj}_H \circ u$: with $\partial_s w(z)$ the real derivative of $w$ at $z$ in the direction $1 \in \mathbb{C}$ (Fréchet derivative, which is $0$ by convention where $w$ is not differentiable),

$$\mathrm{piDs}(H,u,z) = \mathrm{xiCoordC}\big(H,\ w(z),\ \pi_\xi(H, w(z), \partial_s w(z))\big).$$

$\mathrm{HasZeroIndex}(f, z_0, k)$. For $f : \mathbb{C} \to \mathbb{C}$: $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 $\mathrm{HasLoopWind}$ with winding $k$.

$\mathrm{HasWindPi}(H, u, \Gamma, k)$. For a finite set $\Gamma \subset \mathbb{C}$: there is a finite set $Z \subset \mathbb{C}$ with $z \in Z \iff (z \notin \Gamma \text{ and } \mathrm{piDs}(H,u,z) = 0)$ (so the zero set of $\mathrm{piDs}$ off $\Gamma$ is required to be finite), and there is a function $\mathrm{idx} : \mathbb{C} \to \mathbb{Z}$ with $\mathrm{HasZeroIndex}(\mathrm{piDs}(H,u,\cdot), z, \mathrm{idx}(z))$ for every $z \in Z$, and $\sum_{z \in Z}\mathrm{idx}(z) = k$. If there are no such zeros, this says $k = 0$.

$\mathrm{HasWindInfAt}(H, u, e, \varepsilon, k)$. For $e : \mathbb{R}\times\mathbb{R} \to \mathbb{C}$, $\varepsilon \in \mathbb{R}$, and $W(s,t) = \operatorname{proj}_H(u(e(s,t)))$: there is $s_0$ such that for every $s \ge s_0$ the loop

$$t \mapsto \mathrm{xiCoordC}\Big(H,\ W(s, \varepsilon t),\ \pi_\xi\big(H, W(s,\varepsilon t), \partial_s W(s, \varepsilon t)\big)\Big)$$

has $\mathrm{HasLoopWind}$ with winding $k$ ($\partial_s W$ is the Fréchet derivative of $W$ in direction $(1,0)$, $0$ where not differentiable). Since $\mathrm{HasLoopWind}$ requires $1$-periodicity in $t$, the loop must be $1$-periodic after the rescaling $t \mapsto \varepsilon t$; $\varepsilon$ is otherwise unrestricted.

$\mathrm{IsFastPlane}(H, J, u)$. For $u : \mathbb{C} \to V$, all three hold:

1. $u$ is a finite-energy curve on all of $\mathbb{C}$: $u$ is $C^\infty$, $u(z) \ne 0$ everywhere, $u$ is $\tilde J$-holomorphic on $\mathbb{C}$ (differentiable with $\partial_s u + \tilde J(u)\,\partial_t u = 0$, where $\tilde J = \tilde J_{H,J}$ is the imported almost complex structure on $V$ built from $H$ and $J$), and its energy (supremum over smooth monotone $\varphi$ with values in $[0,1]$ of the integral of the positive part of the imported energy density) is finite;
2. there exists a Reeb orbit $P$ of $H$ with $\mathrm{IsPrime}(P)$ such that $u$ has a "nondegenerate end" at $\infty$ asymptotic to $P$ with sign $1$ along $\mathrm{cylInf}$: there are $d, c \in \mathbb{R}$ and $b > 0$ with

$$a_H\big(u(\mathrm{cylInf}(s,t))\big) - T_P s - d \to 0 \quad\text{and}\quad e^{bs}\Big(\operatorname{proj}_H\big(u(\mathrm{cylInf}(s,t))\big) - x_P(T_P t + c)\Big) \to 0$$

uniformly in $t \in \mathbb{R}$ as $s \to +\infty$; 3. $\mathrm{HasWindPi}(H, u, \varnothing, 0)$: $\mathrm{piDs}(H,u,\cdot)$ has finitely many zeros in $\mathbb{C}$, each isolated with a well-defined local winding index, and these indices sum to $0$.

No hypotheses on $H$ or $J$ (star-shapedness, compatibility, smoothness) are built into any of these definitions; they are stated for arbitrary $H$, $J$, $u$.