The ξ-part of the derivative of a fast plane vanishes nowhere

Proved

FiniteEnergyPlane.piDs_ne_zero_of_isFastPlane

by Mazecto · Nov 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

pseudoholomorphic-curvessymplectic-geometrywinding-numbers

Let $S=H^{-1}(1)\subset\mathbb{R}^4$ be a strictly star-shaped level and $J$ a smooth $d\lambda_0$ -compatible complex structure on $\xi$ . If $u$ is a fast finite-energy plane and $w=\mathrm{proj}\circ u$ , then $\pi\,\partial_s w(z)\neq 0$ for every $z\in\mathbb{C}$ , where $\pi$ is the projection onto $\xi$ along the Reeb field.

Role: this is the pointwise form of the condition $\mathrm{wind}_\pi(u)=0$ in the definition of a fast plane, and it is the input for the immersion and transversality properties of $w$ .

Formalization Note. piDs H u z is $\pi\,\partial_s w(z)$ expressed in the global complex frame of $\xi$ (xiCoordC), as defined in Definitions.Def_FiniteEnergyPlane_Winding.

Preamble

import Definitions.Def_FiniteEnergyPlane_Winding

Formal statement

namespace FiniteEnergyPlane

/-- On a fast finite-energy plane, the `ξ`-component `π ∂ₛw` of the derivative of
`w = proj ∘ u` vanishes nowhere. -/
theorem piDs_ne_zero_of_isFastPlane (H : V 1 → ℝ) (hH : IsStrictlyStarShapedLevel H)
    (J : V 1 → V 1 →L[ℝ] V 1) (hJ : IsCompatibleXiStructure H J) (u : ℂ → V 1)
    (hfast : IsFastPlane H J u) (z : ℂ) : piDs H u z ≠ 0 := by
  sorry

end FiniteEnergyPlane

Source

U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. Amer. Math. Soc. 364 (2012), arXiv:0812.4076, Section 1 and Definition 2.14

View graph