The linearized Reeb flow along a periodic orbit

Proved

FiniteEnergyPlane.linReebFlow_spec

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

asymptotic-operatorpseudoholomorphic-curvesreeb-dynamicssymplectic-geometrysymplectization

Let $S=H^{-1}(1)\subset\mathbb{R}^{2n+2}$ be a strictly star-shaped level and $P=(x,T)$ a periodic Reeb orbit on $S$ . There is exactly one linearized Reeb flow $\Phi$ along $P$ , and for every $\tau\in\mathbb{R}$ : $\Phi(\tau)$ maps $\xi_{x(0)}$ into $\xi_{x(\tau)}$ , $\omega_0(\Phi(\tau)v,\Phi(\tau)w)=\omega_0(v,w)$ for $v,w\in\xi_{x(0)}$ , and $\Phi(\tau+T)=\Phi(\tau)\circ\Phi(T)$ .

Formalization Note The flow is IsLinReebFlow P Φ with Φ : ℝ → V n →L[ℝ] V n, with the derivative of reeb H on $V$ ; the first claim is ∃!.

Preamble

import Definitions.Def_FiniteEnergyPlane_Asymptotics

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- The linearized Reeb flow along a periodic Reeb orbit `P = (x, T)` exists and is unique. It
maps `ξ_{x(0)}` into `ξ_{x(τ)}`, preserves `ω₀` on `ξ_{x(0)}`, and satisfies
`Φ(τ + T) = Φ(τ) ∘ Φ(T)`. -/
theorem linReebFlow_spec {n : ℕ} (H : V n → ℝ) (hH : IsStrictlyStarShapedLevel H) (P : ReebOrbit H) :
    (∃! Φ : ℝ → V n →L[ℝ] V n, IsLinReebFlow P Φ) ∧
      ∀ Φ : ℝ → V n →L[ℝ] V n, IsLinReebFlow P Φ →
        (∀ τ : ℝ, ∀ v w : V n, IsInXi H (P.x 0) v → IsInXi H (P.x 0) w →
          IsInXi H (P.x τ) (Φ τ v) ∧ omega0 (Φ τ v) (Φ τ w) = omega0 v w) ∧
        ∀ τ : ℝ, Φ (τ + P.T) = (Φ τ).comp (Φ P.T) := by
  sorry

end FiniteEnergyPlane

Source

C. Wendl, Lectures on Symplectic Field Theory, lecture notes, Humboldt-Universität zu Berlin (2026 version); earlier version arXiv:1612.01009, Section 3.1; 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, Section 2.2.3

Read-back

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

Read-back: `FiniteEnergyPlane.linReebFlow_spec`

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$ . For $x \in V$ , $\xi_x = \{v : \lambda_x(v) = 0,\ dH_x(v) = 0\}$ .

Hypotheses.

$H : V \to \mathbb R$ 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$ .
$P$ is a Reeb orbit of $H$ : a map $x_P : \mathbb R \to V$ and a number $T_P > 0$ with $H(x_P(\tau)) = 1$ , $x_P'(\tau) = R(x_P(\tau))$ (differentiable everywhere) and $x_P(\tau + T_P) = x_P(\tau)$ for all $\tau$ . $T_P$ need not be the minimal period.

Call $\Phi : \mathbb R \to \mathrm L(V, V)$ (linear maps of $V$ ) a linearised Reeb flow along $P$ if $\Phi(0) = \mathrm{id}_V$ and for every $\tau$ , $\Phi$ is differentiable at $\tau$ with $\Phi'(\tau) = DR(x_P(\tau)) \circ \Phi(\tau)$ , where $DR(x)$ is the Fréchet derivative of $R$ at $x$ (zero where $R$ is not differentiable).

Conclusion. Both of the following hold.

There exists exactly one linearised Reeb flow $\Phi$ along $P$ .
Every linearised Reeb flow $\Phi$ $Φ$ along $P$ $P$ satisfies:
- for every $\tau \in \mathbb R$ and all $v, w \in \xi_{x_P(0)}$ :

\Phi(\tau) v \in \xi_{x_P(\tau)} \quad\text{and}\quad \omega_0\bigl(\Phi(\tau) v, \Phi(\tau) w\bigr) = \omega_0(v, w);

for every $\tau \in \mathbb R$ :

\Phi(\tau + T_P) = \Phi(\tau) \circ \Phi(T_P).

The preservation statements are made only for vectors in $\xi_{x_P(0)}$ , not for all of $V$ . The composition identity is stated on all of $V$ , with $\Phi(\tau)$ applied after $\Phi(T_P)$ .

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 linearized Reeb flow along a periodic orbit

Read-back: FiniteEnergyPlane.linReebFlow_spec

Read-back: `FiniteEnergyPlane.linReebFlow_spec`