The Reeb vector field of a star-shaped level

Proved

FiniteEnergyPlane.reeb_spec

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

finite-energypseudoholomorphic-curvesreeb-dynamicssymplectic-geometrysymplectization

Let $S=H^{-1}(1)$ be a strictly star-shaped level and $x\in S$ . Then $\lambda_0(x)X_H(x)>0$ , and $R(x)=X_H(x)/\lambda_0(x)X_H(x)$ satisfies $\lambda_0(x)R(x)=1$ , $dH(x)R(x)=0$ , and $\omega_0(R(x),w)=0$ for every $w$ with $dH(x)w=0$ .

Formalization Note $R$ is reeb H x; the tangent space $T_xS$ is $\ker dH(x)$ , with fderiv ℝ H x.

Preamble

import Definitions.Def_FiniteEnergyPlane_Setting

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- The Reeb field of `λ₀|S` (Hofer 1993, § 1; Hryniewicz 2014, § 2.1). On a strictly
star-shaped level `S`, `λ₀(X_H) > 0`, and `R = X_H / λ₀(X_H)` is tangent to `S`, satisfies
`λ₀(R) = 1`, and `ω₀(R, w) = 0` for every `w ∈ T_x S`. -/
theorem reeb_spec {n : ℕ} (H : V n → ℝ) (hH : IsStrictlyStarShapedLevel H) (x : V n)
    (hx : x ∈ energySurface H) :
    0 < liouville x (hamVF H x) ∧ liouville x (reeb H x) = 1 ∧ fderiv ℝ H x (reeb H x) = 0 ∧
      ∀ w : V n, fderiv ℝ H x w = 0 → omega0 (reeb H x) w = 0 := by
  sorry

end FiniteEnergyPlane

Source

H. Hofer, Pseudoholomorphic curves in symplectizations with applications to the Weinstein conjecture in dimension three, Invent. Math. 114 (1993), 515–563, Section 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.1

Read-back

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

Read-back: `FiniteEnergyPlane.reeb_spec`

Setting. Fix a natural number $n \ge 0$ (implicit) and let $V = \mathbb{R}^{2(n+1)}$ , with coordinates indexed $0, 1, \dots, 2n+1$ (so $\dim V \ge 2$ ). The following fixed structures are used:

$j_0 : V \to V$ is the linear map with $(j_0 v)_k = -v_{k+1}$ for $k$ even and $(j_0 v)_k = v_{k-1}$ for $k$ odd; on each coordinate pair $(v_{2i}, v_{2i+1})$ it acts as $(a, b) \mapsto (-b, a)$ .
$\omega_0(u, v) = \sum_k (j_0 u)_k\, v_k = \sum_i \big(u_{2i} v_{2i+1} - u_{2i+1} v_{2i}\big)$ .
$\lambda_x(v) = \tfrac12 \omega_0(x, v)$ for $x, v \in V$ .
For $H : V \to \mathbb{R}$ , $dH_x$ is the Fréchet derivative of $H$ at $x$ (by convention the zero map where $H$ is not differentiable); $\nabla H(x)$ is the vector with components $dH_x(e_k)$ ( $e_k$ the standard basis vectors); $X_H(x) = j_0 \nabla H(x)$ .
$R(x) = \lambda_x(X_H(x))^{-1}\, X_H(x)$ , with the convention $0^{-1} = 0$ (so $R(x) = 0$ whenever $\lambda_x(X_H(x)) = 0$ ).

Hypotheses. A function $H : V \to \mathbb{R}$ such that (i) $H$ is $C^\infty$ ; (ii) for every $u \ne 0$ there is exactly one $r \in \mathbb{R}$ with $r > 0$ and $H(r u) = 1$ ; (iii) for every $x$ with $H(x) = 1$ , $dH_x(x) > 0$ . And a point $x \in V$ with $H(x) = 1$ .

Conclusion. All four of the following hold:

$\lambda_x(X_H(x)) > 0$ , i.e. $\tfrac12 \omega_0\big(x, j_0 \nabla H(x)\big) > 0$ ;
$\lambda_x(R(x)) = 1$ ;
$dH_x(R(x)) = 0$ ;
for every $w \in V$ with $dH_x(w) = 0$ , one has $\omega_0(R(x), w) = 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

The Reeb vector field of a star-shaped level

Read-back: FiniteEnergyPlane.reeb_spec

Read-back: `FiniteEnergyPlane.reeb_spec`