The global-frame coordinates of $\xi$ are symplectic

Proved

FiniteEnergyPlane.im_conj_xiCoordC_mul

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

contact-geometryreeb-dynamicswinding-numbers

Let $S=H^{-1}(1)\subset\mathbb{R}^4$ be a strictly star-shaped level, $x\in S$ , and $\psi_x:\xi_x\to\mathbb{C}$ the coordinates in Hryniewicz's global frame of $\xi$ . Then for all $a,b\in\xi_x$

\operatorname{Im}\big(\overline{\psi_x(a)}\,\psi_x(b)\big)=\omega_0(a,b).

In particular $\psi_x$ is an orientation-preserving isomorphism from $(\xi_x,\omega_0)$ to $\mathbb{C}$ with its standard symplectic form.

Formalization Note $\psi_x$ is xiCoordC H x, $\xi_x$ membership is IsInXi H x, and $\omega_0$ is omega0 on V 1.

Preamble

import Definitions.Def_FiniteEnergyPlane_Winding

Formal statement

namespace FiniteEnergyPlane

open Metric Filter Topology
open scoped ContDiff

/-- For `x ∈ S = H⁻¹(1)` and `a, b ∈ ξ_x`, the global-frame coordinates `ψ_x = xiCoordC H x` satisfy
`Im(conj ψ_x(a) · ψ_x(b)) = ω₀(a, b)`. -/
theorem im_conj_xiCoordC_mul (H : V 1 → ℝ) (hH : IsStrictlyStarShapedLevel H) {x : V 1}
    (hx : H x = 1) {a b : V 1} (ha : IsInXi H x a) (hb : IsInXi H x b) :
    (starRingEnd ℂ (xiCoordC H x a) * xiCoordC H x b).im = omega0 a b := by
  sorry

end FiniteEnergyPlane

Source

U. Hryniewicz, J. Symplectic Geom. 12 (2014), arXiv:1105.2077, Section 2.2 (global symplectic frame of the contact structure)

View graph

The global-frame coordinates of ξ\xiξ are symplectic

The global-frame coordinates of $\xi$ are symplectic