Periods of Reeb orbits on a star-shaped level are bounded away from zero

Proved

FiniteEnergyPlane.exists_period_lower_bound

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

finite-energypseudoholomorphic-curvesreeb-dynamicssymplectic-geometrysymplectization

Let $S=H^{-1}(1)\subset\mathbb{R}^{2n+2}$ be a strictly star-shaped level. There is $T_0>0$ such that $T\ge T_0$ for every periodic Reeb orbit $(x,T)$ on $S$ .

Formalization Note Periods are not required to be minimal (ReebOrbit allows multiple covers), which does not affect the statement.

Preamble

import Definitions.Def_FiniteEnergyPlane_Setting

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- Periods of Reeb orbits on a strictly star-shaped level are bounded away from `0`: there is
`T₀ > 0` with `T₀ ≤ T` for every periodic Reeb orbit `(x, T)` on `S`. -/
theorem exists_period_lower_bound {n : ℕ} (H : V n → ℝ) (hH : IsStrictlyStarShapedLevel H) :
    ∃ T₀ : ℝ, 0 < T₀ ∧ ∀ P : ReebOrbit H, T₀ ≤ P.T := by
  sorry

end FiniteEnergyPlane

Source

Standard fact for a compact contact-type hypersurface; stated in 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, p. 26

Read-back

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

Read-back: `FiniteEnergyPlane.exists_period_lower_bound`

Ambient space. Fix a natural number $n$ (including $n = 0$ ) and let $V = \mathbb{R}^{2(n+1)}$ , with coordinates indexed $k = 0, 1, \dots, 2n+1$ . On $V$ the code uses:

the linear map $j_0$ given by $(j_0 v)_k = -v_{k+1}$ when $k$ is even and $(j_0 v)_k = v_{k-1}$ when $k$ is odd;
the Euclidean dot product $\langle u, v\rangle = \sum_k u_k v_k$ , the form $\omega_0(u, v) = \langle j_0 u, v\rangle$ , and the Liouville form $\lambda_x(v) = \tfrac12 \omega_0(x, v)$ ;
for $H : V \to \mathbb{R}$ , the vector $\nabla H(x)$ with components $(\nabla H(x))_k = DH(x)(e_k)$ , where $DH(x)$ is the Fréchet derivative (taken to be $0$ at points where $H$ is not differentiable), the Hamiltonian vector field $X_H(x) = j_0 \nabla H(x)$ , and the energy surface $S = \{x \in V : H(x) = 1\}$ ;
the "Reeb" field

R(x) = \big(\lambda_x(X_H(x))\big)^{-1} X_H(x),

where the inverse of $0$ is taken to be $0$ (so $R(x) = 0$ wherever $\lambda_x(X_H(x)) = 0$ ).

Hypothesis. $H : V \to \mathbb{R}$ satisfies the predicate "strictly star-shaped level", which by definition means all three of:

$H$ is $C^\infty$ on all of $V$ ;
for every $u \in V$ with $u \neq 0$ there is exactly one real $r$ with $r > 0$ and $H(r u) = 1$ ;
for every $x \in V$ with $H(x) = 1$ , $DH(x)(x) > 0$ .

Reeb orbits. An object "Reeb orbit of $H$ " consists of a map $x : \mathbb{R} \to V$ and a real number $T$ such that $T > 0$ ; $x(\tau) \in S$ for all $\tau$ ; $x$ is differentiable at every $\tau$ with $x'(\tau) = R(x(\tau))$ ; and $x(\tau + T) = x(\tau)$ for all $\tau$ . Here $T$ is any positive period of $x$ , not necessarily the minimal one; nothing excludes constant maps $x$ if $R$ vanishes at a point of $S$ (in which case every $T > 0$ is admissible).

Conclusion. There exists a real number $T_0 > 0$ such that for every Reeb orbit $(x, T)$ of $H$ ,

T_0 \le T.

If $H$ has no Reeb orbits, the conclusion holds with any $T_0 > 0$ .

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

Periods of Reeb orbits on a star-shaped level are bounded away from zero

Read-back: FiniteEnergyPlane.exists_period_lower_bound

Read-back: `FiniteEnergyPlane.exists_period_lower_bound`