The kernel of the asymptotic operator

Proved

FiniteEnergyPlane.asympOp_eq_zero_iff

by Mazecto · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

asymptotic-operatorpseudoholomorphic-curvesreeb-dynamicssymplectic-geometrysymplectization

Let $S=H^{-1}(1)$ be a strictly star-shaped level, $J$ a smooth $d\lambda_0$ -compatible complex structure on $\xi$ , and $P=(x,T)$ a periodic Reeb orbit with linearized Reeb flow $\Phi$ . A $\xi$ -loop $\eta$ along $P$ satisfies $A_P\eta=0$ if and only if $\eta(t)=\Phi(Tt)\eta(0)$ for all $t$ . Moreover $P$ is nondegenerate if and only if the only $\xi$ -loop $\eta$ with $A_P\eta=0$ is $\eta=0$ .

Formalization Note The first claim is stated for every Φ with IsLinReebFlow P Φ.

Preamble

import Definitions.Def_FiniteEnergyPlane_Asymptotics

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- The kernel of the asymptotic operator: a `ξ`-loop `η` satisfies `A_P η = 0` if and only if
`η(t) = Φ(Tt) η(0)` for the linearized Reeb flow `Φ`. Consequently `P` is nondegenerate if and
only if `A_P` has trivial kernel on `ξ`-loops. -/
theorem asympOp_eq_zero_iff {n : ℕ} (H : V n → ℝ) (hH : IsStrictlyStarShapedLevel H)
    (J : V n → V n →L[ℝ] V n) (hJ : IsCompatibleXiStructure H J) (P : ReebOrbit H) :
    (∀ Φ : ℝ → V n →L[ℝ] V n, IsLinReebFlow P Φ → ∀ η : ℝ → V n, IsXiLoop P η →
      ((∀ t : ℝ, asympOp J P η t = 0) ↔ ∀ t : ℝ, η t = Φ (P.T * t) (η 0))) ∧
    (P.IsNondegenerate ↔
      ∀ η : ℝ → V n, IsXiLoop P η → (∀ t : ℝ, asympOp J P η t = 0) → ∀ t : ℝ, η t = 0) := 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, Definition 2.5; C. Wendl, Lectures on Symplectic Field Theory, lecture notes, Humboldt-Universität zu Berlin (2026 version); earlier version arXiv:1612.01009, Section 3.1

Read-back

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

Read-back: `FiniteEnergyPlane.asympOp_eq_zero_iff`

Setting. Fix $n \in \mathbb N$ (including $n = 0$ ) and let $V = \mathbb R^{2n+2}$ with coordinates $v_0, \dots, v_{2n+1}$ . Write $(j_0 v)_{2i} = -v_{2i+1}$ , $(j_0 v)_{2i+1} = v_{2i}$ , $\langle u, v\rangle = \sum_k u_k v_k$ , and

\omega_0(u, v) = \langle j_0 u, v\rangle = \sum_i \bigl(u_{2i} v_{2i+1} - u_{2i+1} v_{2i}\bigr), \qquad \lambda_x(v) = \tfrac12\, \omega_0(x, v).

For $H : V \to \mathbb R$ , $dH_x$ is the Fréchet derivative at $x$ (the zero map where $H$ is not differentiable), $\nabla H(x) = (dH_x(e_k))_k$ , $X_H = j_0 \nabla H$ , and the Reeb field is $R(x) = \lambda_x(X_H(x))^{-1} X_H(x)$ with $0^{-1} = 0$ ; $DR(x)$ is its Fréchet derivative (zero where $R$ is not differentiable). For $x \in V$ , $\xi_x = \{v : \lambda_x(v) = 0,\ dH_x(v) = 0\}$ .

Hypotheses.

$H$ is strictly star-shaped: $H$ is $C^\infty$ ; for every $u \neq 0$ there is exactly one $r > 0$ with $H(r u) = 1$ ; and $dH_x(x) > 0$ whenever $H(x) = 1$ .
$J$ assigns to each $x \in V$ a linear map $J_x : V \to V$ , and $J$ is compatible with $\xi$ : $x \mapsto J_x$ is $C^\infty$ , and for every $x$ with $H(x) = 1$ and all $v, w \in \xi_x$ :

J_x v \in \xi_x, \quad J_x J_x v = -v, \quad v \neq 0 \Rightarrow \omega_0(v, J_x v) > 0, \quad \omega_0(J_x v, J_x w) = \omega_0(v, w).

$P$ is a Reeb orbit of $H$ : $x_P : \mathbb R \to V$ and $T_P > 0$ with $H(x_P(\tau)) = 1$ , $x_P'(\tau) = R(x_P(\tau))$ and $x_P(\tau + T_P) = x_P(\tau)$ for all $\tau$ .

Terms used in the conclusion.

A linearised Reeb flow along $P$ is $\Phi : \mathbb R \to \mathrm L(V,V)$ with $\Phi(0) = \mathrm{id}$ and $\Phi'(\tau) = DR(x_P(\tau)) \circ \Phi(\tau)$ for every $\tau$ .
A $\xi$ -loop along $P$ is a $C^\infty$ , $1$ -periodic $\eta : \mathbb R \to V$ with $\eta(t) \in \xi_{x_P(T_P t)}$ for all $t$ .
The asymptotic operator: $(A\eta)(t) = J_{x_P(T_P t)}\bigl( -\eta'(t) + T_P\, DR(x_P(T_P t))\, \eta(t) \bigr)$ .
$P$ is nondegenerate if for every linearised Reeb flow $\Phi$ and every $v \in \xi_{x_P(0)}$ , $\Phi(T_P) v = v$ implies $v = 0$ .

Conclusion. Both of the following hold.

For every linearised Reeb flow $\Phi$ along $P$ and every $\xi$ -loop $\eta$ along $P$ :

\Bigl( (A\eta)(t) = 0 \text{ for all } t \Bigr) \iff \Bigl( \eta(t) = \Phi(T_P t)\, \eta(0) \text{ for all } t \Bigr).

P \text{ is nondegenerate} \iff \text{every } \xi\text{-loop } \eta \text{ along } P \text{ with } A\eta \equiv 0 \text{ satisfies } \eta \equiv 0.

In part 1 the equivalence is asserted for each linearised flow separately (if none existed, part 1 would be vacuous). Both parts concern only $\xi$ -loops, i.e. smooth $1$ -periodic sections of $\xi$ along $t \mapsto x_P(T_P t)$ .

Human review

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

View graph

The kernel of the asymptotic operator

Read-back: FiniteEnergyPlane.asympOp_eq_zero_iff

Read-back: `FiniteEnergyPlane.asympOp_eq_zero_iff`