Zero charge keeps the symplectization coordinate bounded near a puncture

Let $S=H^{-1}(1)\subset\mathbb R^{2n+2}$ be a strictly star-shaped level with contact form $\lambda=\lambda_0|_S$ and $d\lambda$-compatible complex structure $J$ on $\xi$, and let $u=(a,w):\dot D=D\setminus\{0\}\to\mathbb R\times S\cong\mathbb R^{2n+2}\setminus\{0\}$ be a finite-energy $\tilde J$-holomorphic curve on the punctured unit disc. Write $Q(\rho)=\int_0^1 w(\gamma_\rho(t))^*\lambda$ for the action of the clockwise loop $\gamma_\rho(t)=\rho e^{-2\pi i t}$, and assume the gradient bound $|z|\,|\nabla u(z)|\le C$ for $0<|z|<r$, where $|\nabla u|=\|Da\|+\|Dw\|$. If $Q(\rho)\to0$ as $\rho\to0^+$, then the coordinate $a$ is bounded near the puncture: there are $r'>0$ and $A$ with $|a(u(z))|\le A$ for $0<|z|<r'$.

In other words, a puncture of zero charge is neither positive nor negative: $u$ does not escape to either end of the symplectization. This is a step in the zero-charge case of the asymptotic description of finite-energy punctured discs (Hofer; Wendl, Theorem 9.8).

Formalization Note $\mathbb R\times S$ is identified with $\mathbb R^{2n+2}\setminus\{0\}$ by $(a,x)\mapsto e^{2a}x$, and $a$ is aCoord H. The charge hypothesis is Tendsto (fun ρ => loopAction H u (cwLoop 0 ρ)) (𝓝[>] 0) (𝓝 0), and the gradient bound uses gradNorm.