A puncture with bounded symplectization coordinate is removable

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. If $a\circ u$ is bounded on some punctured neighbourhood $0<|z|<r$ of the puncture, then the puncture is removable: $u$ agrees on $\dot D$ with a smooth $\tilde J$-holomorphic map $D\to\mathbb R^{2n+2}\setminus\{0\}$.

This is the bounded case of the asymptotic description of finite-energy punctured discs: a puncture that is not removable must send $a$ to $\pm\infty$ along some sequence. No gradient bound or charge condition is assumed.

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. Finite energy is Hofer's energy energy H, as in IsFiniteEnergyCurve. Removability is IsRemovablePuncture H J u 0 1.