A unitary frame along a Reeb orbit homotopic to the global frame

Proved

FiniteEnergyPlane.exists_unitaryXiFrame_hasXiLoopWind_iff

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

conley-zehnder-indexpseudoholomorphic-curvesreeb-dynamicssymplectic-geometrysymplectizationwinding-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$ . For every periodic Reeb orbit $P=(x,T)$ there is a unitary frame $Z$ of $\xi$ along $P$ such that for every continuous $1$ -periodic nowhere-vanishing $\zeta:\mathbb{R}\to\mathbb{R}^2$ and every $k\in\mathbb{Z}$ : the loop $t\mapsto Z(t)\zeta(t)$ has winding $k$ in the global frame if and only if $\zeta$ has winding $k$ as a loop in $\mathbb{C}$ .

Formalization Note Unitary frames are IsUnitaryXiFrame J P Z of FiniteEnergyPlane_Asymptotics; $\mathbb{R}^2\to\mathbb{C}$ is $(q,p)\mapsto q+ip$ (vecToC).

Preamble

import Definitions.Def_FiniteEnergyPlane_Winding

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- Hryniewicz, Remark 2.6, for `n = 1`: along every periodic Reeb orbit `P` there is a unitary
frame `Z` of `ξ` that is homotopic to the global frame `Z₁, Z₂`, in the sense that a loop
`t ↦ Z(t) ζ(t)` has the same winding number in the global frame as `ζ` has in `ℝ² = ℂ`. -/
theorem exists_unitaryXiFrame_hasXiLoopWind_iff (H : V 1 → ℝ) (hH : IsStrictlyStarShapedLevel H)
    (J : V 1 → V 1 →L[ℝ] V 1) (hJ : IsCompatibleXiStructure H J) (P : ReebOrbit H) :
    ∃ Z : ℝ → CauchyRiemannIndex.Vec 1 →L[ℝ] V 1, IsUnitaryXiFrame J P Z ∧
      ∀ ζ : ℝ → CauchyRiemannIndex.Vec 1, Continuous ζ → Function.Periodic ζ 1 →
        (∀ t : ℝ, ζ t ≠ 0) → ∀ k : ℤ,
          (HasXiLoopWind P (fun t => Z t (ζ t)) k ↔ HasLoopWind (fun t => vecToC (ζ t)) k) := by
  sorry

end FiniteEnergyPlane

Source

U. Hryniewicz, Systems of global surfaces of section for dynamically convex Reeb flows on the 3-sphere, J. Symplectic Geom. 12 (2014), arXiv:1105.2077, Remark 2.6 and Remark 2.13

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Theorem `FiniteEnergyPlane.exists_unitaryXiFrame_hasXiLoopWind_iff`

Work in $V = \mathbb{R}^4$ (coordinates $x_0,\dots,x_3$ ) with $\omega_0(u,v) = u_0v_1 - u_1v_0 + u_2v_3 - u_3v_2$ , Liouville form $\lambda_x(v) = \tfrac12\omega_0(x,v)$ , and $j_0(v) = (-v_1, v_0, -v_3, v_2)$ . Write $\mathbb{R}^2$ for the Euclidean plane with coordinates $(a_L, a_R)$ , $J_0(a_L,a_R) = (-a_R, a_L)$ , and $\langle\cdot,\cdot\rangle$ its standard inner product.

Hypotheses.

$H : V \to \mathbb{R}$ has a strictly star-shaped level set: $H$ is $C^\infty$ ; for every $u \ne 0$ there is exactly one $r > 0$ with $H(ru) = 1$ ; and $dH_x(x) > 0$ whenever $H(x) = 1$ .
$J : V \to \operatorname{End}(V)$ is a compatible complex structure on $\xi$ : $J$ is $C^\infty$ , and for every $x$ with $H(x) = 1$ and all $v, w \in \xi_x$ (where $v \in \xi_x$ means $\lambda_x(v) = 0$ and $dH_x(v) = 0$ ): $J(x)v \in \xi_x$ , $J(x)^2 v = -v$ , $\omega_0(v, J(x)v) > 0$ if $v \ne 0$ , and $\omega_0(J(x)v, J(x)w) = \omega_0(v,w)$ .
$P$ is a Reeb orbit of $H$ : a map $x_P : \mathbb{R} \to V$ and $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$ , where $R_H(x) = \lambda_x(X_H(x))^{-1}X_H(x)$ , $X_H = j_0\nabla H$ . $T_P$ need not be the minimal period (no primality assumed).

Conclusion. There exists $Z : \mathbb{R} \to \mathrm{Lin}(\mathbb{R}^2, V)$ which is a unitary $\xi$ -frame along $P$ , namely: $Z$ is $C^\infty$ and $1$ -periodic, and for every $t$ , with $x = x_P(T_P t)$ ,

$Z(t)a \in \xi_x$ for all $a \in \mathbb{R}^2$ , and every $w \in \xi_x$ equals $Z(t)a$ for some $a$ ;
$J(x)\,Z(t)a = Z(t)\,J_0 a$ for all $a$ ;
$\omega_0(Z(t)a, Z(t)b) = \langle J_0 a, b\rangle$ for all $a, b$ ;

and such that for every continuous, $1$ -periodic, nowhere-vanishing $\zeta : \mathbb{R} \to \mathbb{R}^2$ and every $k \in \mathbb{Z}$ :

\mathrm{HasLoopWind}\Big(t \mapsto \mathrm{xiCoordC}\big(H,\ x_P(T_P t),\ Z(t)\zeta(t)\big),\ k\Big) \iff \mathrm{HasLoopWind}\big(t \mapsto \zeta_L(t) + i\,\zeta_R(t),\ k\big).

Definitions used:

$\mathrm{HasLoopWind}(f, k)$ for $f : \mathbb{R}\to\mathbb{C}$ : $f$ is continuous, $1$ -periodic, nowhere zero, and there is a continuous $\theta:\mathbb{R}\to\mathbb{R}$ with $f(t) = |f(t)|e^{i\theta(t)}$ for all $t$ and $\theta(1)-\theta(0) = 2\pi k$ .
$\mathrm{xiCoordC}(H, x, v) = \omega_0(v, F_2(x)) + i\,\omega_0(F_1(x), v)$ , a fixed coordinate system built from $H$ alone, where

F_1(x) = |x|^{-1}\Big(Q_2(x) - \tfrac{dH_x(Q_2(x))}{dH_x(x)}\,x\Big),\qquad F_2(x) = |x|^{-1}\Big(Q_1(x) - \tfrac{dH_x(Q_1(x))}{dH_x(x)}\,x\Big),

$Q_1(x) = (-x_2, x_3, x_0, -x_1)$ , $Q_2(x) = (x_3, x_2, -x_1, -x_0)$ , $|x|$ the Euclidean norm (conventions $|0|^{-1} = 0$ , division by $0$ gives $0$ ).

So the frame $Z$ is asserted to exist with the property that, for every nowhere-zero loop $\zeta$ in $\mathbb{R}^2$ , the winding of $\zeta$ (viewed in $\mathbb{C}$ ) equals the winding of $Z\zeta$ read in the fixed coordinates $\mathrm{xiCoordC}$ ; the equivalence is required for each integer $k$ separately. The existence of a single such $Z$ is asserted for each $H$ , $J$ , $P$ satisfying the hypotheses; uniqueness is not claimed.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Mazecto · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

A unitary frame along a Reeb orbit homotopic to the global frame

Theorem FiniteEnergyPlane.exists_unitaryXiFrame_hasXiLoopWind_iff

Theorem `FiniteEnergyPlane.exists_unitaryXiFrame_hasXiLoopWind_iff`