Finitely many families of nondegenerate Reeb orbits below a period bound

Proved

FiniteEnergyPlane.exists_reebOrbit_families_finite

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

compactnessfast-planespseudoholomorphic-curvesreeb-dynamicssymplectic-geometrysymplectization

Let $S=H^{-1}(1)\subset\mathbb{R}^{2n+2}$ be a strictly star-shaped level and $T\in\mathbb{R}$ , and suppose every periodic Reeb orbit of period at most $T$ is nondegenerate. Then there are finitely many periodic orbits $Q_1=(x_1,T_1),\dots,Q_N=(x_N,T_N)$ with $T_i\le T$ and a number $\delta>0$ such that

every periodic orbit $(x,T')$ with $T'\le T$ is a time shift of some $Q_i$ with the same period: $T'=T_i$ and $x(\tau)=x_i(\tau+c)$ for some $c$ ;
for $i\neq j$ and all phases $c,c'$ , $\sup_t|x_i(T_it+c)-x_j(T_jt+c')|\ge\delta$ .

Formalization Note Part 2 is stated as: there is $t$ with $\delta\le\|x_i(T_it+c)-x_j(T_jt+c')\|$ (sup norm on $\mathbb{R}^{2n+2}$ ).

Preamble

import Definitions.Def_FiniteEnergyPlane_Compactness

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- Let `S = H⁻¹(1)` be a strictly star-shaped level and `T > 0`, and suppose every periodic Reeb
orbit of period at most `T` is nondegenerate. Then these orbits form finitely many families: there
are orbits `Q₁, …, Q_N` of period at most `T` such that every periodic orbit of period at most `T`
is a time shift of some `Qᵢ` with the same period, and the normalized loops of distinct families
`t ↦ Qᵢ.x(Tᵢ t + c)` and `t ↦ Qⱼ.x(Tⱼ t + c')` stay `C⁰`-distance at least `δ > 0` apart for all
phases `c, c'`. (Hryniewicz, Trans. AMS 2012, (6) and § 4.4: finiteness of the orbits of bounded
period.) -/
theorem exists_reebOrbit_families_finite {n : ℕ} (H : V n → ℝ) (hH : IsStrictlyStarShapedLevel H)
    (T : ℝ) (hnd : ∀ Q : ReebOrbit H, Q.T ≤ T → Q.IsNondegenerate) :
    ∃ (N : ℕ) (Q : Fin N → ReebOrbit H) (δ : ℝ), 0 < δ ∧ (∀ i, (Q i).T ≤ T) ∧
      (∀ R : ReebOrbit H, R.T ≤ T →
        ∃ i, (Q i).T = R.T ∧ ∃ c : ℝ, ∀ τ : ℝ, R.x τ = (Q i).x (τ + c)) ∧
      ∀ i j, i ≠ j → ∀ c c' : ℝ, ∃ t : ℝ,
        δ ≤ ‖(Q i).x ((Q i).T * t + c) - (Q j).x ((Q j).T * t + c')‖ := by
  sorry

end FiniteEnergyPlane

Source

U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. Amer. Math. Soc. 364 (2012), 1859–1931, arXiv:0812.4076, Section 2, formula (6), and Section 4.4

Read-back

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

Read-back: `FiniteEnergyPlane.exists_reebOrbit_families_finite`

Fix $n\in\mathbb{N}$ and set $V_n=\mathbb{R}^{2n+2}$ , with coordinates indexed $0,\dots,2n+1$ and the maximum norm $\|v\|=\max_k|v_k|$ . Let $H:V_n\to\mathbb{R}$ satisfy the following three conditions (strictly star-shaped level):

$H$ is $C^\infty$ ;
for every $u\neq0$ there is exactly one $r>0$ with $H(ru)=1$ ;
$DH(x)x>0$ whenever $H(x)=1$ .

Let $T\in\mathbb{R}$ be arbitrary. Assume every Reeb orbit $Q$ of $H$ with $T_Q\le T$ is nondegenerate. The theorem asserts that there exist $N\in\mathbb{N}$ , Reeb orbits $Q_0,\dots,Q_{N-1}$ of $H$ , and $\delta>0$ with the following properties.

$T_{Q_i}\le T$ for every $i$ .
Every Reeb orbit $R$ with $T_R\le T$ is a time shift of one of the $Q_i$ with the same period. That is, there are $i$ and $c\in\mathbb{R}$ with $T_{Q_i}=T_R$ and

x_R(\tau) = x_{Q_i}(\tau+c)\quad\text{for all }\tau\in\mathbb{R}.

For all $i\neq j$ and all $c,c'\in\mathbb{R}$ there is a $t\in\mathbb{R}$ with

\delta \le \big\| x_{Q_i}(T_{Q_i}t+c) - x_{Q_j}(T_{Q_j}t+c')\big\|.

$N=0$ is allowed. In that case clause 2 says there is no Reeb orbit with period $\le T$ , which is the situation for instance when $T\le0$ , since periods are positive. Clause 3 applies to every pair of distinct indices $i\neq j$ , including pairs whose periods $T_{Q_i}$ and $T_{Q_j}$ differ.

Definitions used

Forms and Reeb field.

$(j_0v)_{2i}=-v_{2i+1}$ and $(j_0v)_{2i+1}=v_{2i}$ .
$\omega_0(u,v)=\sum_i(u_{2i}v_{2i+1}-u_{2i+1}v_{2i})$ .
$\lambda_x(v)=\tfrac12\omega_0(x,v)$ .
$\nabla H(x)_k = DH(x)e_k$ .
$X_H=j_0\nabla H$ .
The Reeb field is $R_H(x)=\lambda_x(X_H(x))^{-1}X_H(x)$ , with $0^{-1}=0$ ; it is defined on all of $V_n$ .
$\xi_x=\{v:\lambda_x(v)=0,\ DH(x)v=0\}$ .

Reeb orbit. A Reeb orbit $Q=(x_Q,T_Q)$ is a map $x_Q:\mathbb{R}\to V_n$ and a number $T_Q>0$ such that:

$H(x_Q(\tau))=1$ and $x_Q'(\tau)=R_H(x_Q(\tau))$ for all $\tau$ ;
$x_Q(\tau+T_Q)=x_Q(\tau)$ for all $\tau$ .

$T_Q$ is any positive period, not necessarily the minimal one, so iterated orbits are separate Reeb orbits. The assumption and clause 2 quantify over all such pairs.

Nondegenerate. $Q$ is nondegenerate if the following holds for every $\Phi:\mathbb{R}\to L(V_n)$ with $\Phi(0)=\mathrm{id}$ and $\Phi'(\tau)=DR_H(x_Q(\tau))\circ\Phi(\tau)$ for all $\tau$ : every $v\in\xi_{x_Q(0)}$ with $\Phi(T_Q)v=v$ is $0$ .

Human review

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

View graph

Finitely many families of nondegenerate Reeb orbits below a period bound

Read-back: FiniteEnergyPlane.exists_reebOrbit_families_finite

Definitions used

Read-back: `FiniteEnergyPlane.exists_reebOrbit_families_finite`