Nondegeneracy of Reeb orbits in $\mathbb{R}^4$ and of Hamiltonian periodic orbits

Proved

FiniteEnergyPlane.isNondegenerate_bridge

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

asymptotic-operatorpseudoholomorphic-curves

Let $H_0:\mathbb{R}^4\to\mathbb{R}$ have a strictly star-shaped level, in the sense of HryniewiczCriterion, and let $H$ be the same function on $V=\mathbb{R}^{2\cdot(1+1)}$ . Let $P$ be a periodic orbit of $X_{H_0}$ on $H_0^{-1}(1)$ (in HryniewiczCriterion) and $Q$ a periodic Reeb orbit of $H$ with the same image and with period equal to the action $\int_0^{T_P}\lambda_0(\dot x)$ of $P$ . Then $Q$ is nondegenerate if and only if, for the linearized flow $Y$ of $X_{H_0}$ along $P$ , the path $\varphi$ of HryniewiczCriterion.linearizedXiPath satisfies: $\varphi(1)v=v$ only for $v=0$ .

Formalization Note The coordinates are transported by Fin.cast along 2 * (1 + 1) = 4, as in periodicOrbit_bridge of the previous mission. The right-hand side is the nondegeneracy hypothesis appearing in HryniewiczCriterion (for every Y with IsLinearizedFlow H₀ P.x Y).

Preamble

import Definitions.Def_FiniteEnergyPlane_Asymptotics
import Definitions.Def_HryniewiczCriterion_ConleyZehnder

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- For `n = 1`, nondegeneracy of a periodic Reeb orbit agrees with nondegeneracy of the
corresponding periodic orbit of `X_H` in `HryniewiczCriterion` (no eigenvalue `1` of the
linearized flow on `ξ` in the global frame). The coordinates are transported along
`Fin (2 * (1 + 1)) = Fin 4`; the orbits correspond by image and action, as in
`periodicOrbit_bridge`. -/
theorem isNondegenerate_bridge (H₀ : HryniewiczCriterion.R4 → ℝ)
    (hH₀ : HryniewiczCriterion.IsStrictlyStarShapedLevel H₀) :
    let toV : HryniewiczCriterion.R4 → V 1 := fun x k => x (Fin.cast (by norm_num) k)
    let H : V 1 → ℝ := fun y => H₀ (fun k => y (Fin.cast (by norm_num) k))
    ∀ (P : HryniewiczCriterion.PeriodicOrbit H₀) (Q : ReebOrbit H),
      Set.range Q.x = Set.range (fun τ => toV (P.x τ)) →
      Q.T = ∫ τ in (0 : ℝ)..P.T, liouville (toV (P.x τ)) (deriv (fun s => toV (P.x s)) τ) →
      (Q.IsNondegenerate ↔
        ∀ Y : ℝ → (HryniewiczCriterion.R4 →L[ℝ] HryniewiczCriterion.R4),
          HryniewiczCriterion.IsLinearizedFlow H₀ P.x Y →
          ∀ v : Fin 2 → ℝ, (HryniewiczCriterion.linearizedXiPath H₀ P Y 1).mulVec v = v →
            v = 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, Section 2.1

Read-back

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

Read-back: `FiniteEnergyPlane.isNondegenerate_bridge`

This statement compares two independent sets of definitions on $\mathbb{R}^4$ .

Definitions on $\mathbb{R}^4$ (first family). For $x, u, v \in \mathbb{R}^4$ (coordinates $0,1,2,3$ ):

$\omega(u, v) = u_0 v_1 - u_1 v_0 + u_2 v_3 - u_3 v_2$ and $\ell_x(v) = \tfrac12 (x_0 v_1 - x_1 v_0 + x_2 v_3 - x_3 v_2)$ ;
for $H_0 : \mathbb{R}^4 \to \mathbb{R}$ , $\partial_i H_0(x) = dH_0(x) e_i$ (Fréchet derivative, $0$ where not differentiable) and $X(x) = (-\partial_1 H_0, \partial_0 H_0, -\partial_3 H_0, \partial_2 H_0)(x)$ ;
$|x| = \sqrt{\sum_i x_i^2}$ , $Q_1 x = (-x_2, x_3, x_0, -x_1)$ , $Q_2 x = (x_3, x_2, -x_1, -x_0)$ , and

f_1(x) = |x|^{-1}\Big(Q_2 x - \tfrac{dH_0(x) Q_2 x}{dH_0(x) x}\, x\Big), \qquad f_2(x) = |x|^{-1}\Big(Q_1 x - \tfrac{dH_0(x) Q_1 x}{dH_0(x) x}\, x\Big)

(division by $0$ gives $0$ );

$\pi_x(v) = v - \dfrac{\ell_x(v)}{\ell_x(X(x))}\, X(x)$ and $\kappa_x(v) = \big(\omega(v, f_2(x)),\ \omega(f_1(x), v)\big) \in \mathbb{R}^2$ .

" $H_0$ is a strictly star-shaped level": $H_0$ is $C^\infty$ , each $y \ne 0$ has exactly one $r > 0$ with $H_0(r y) = 1$ , and $dH_0(x) x > 0$ whenever $H_0(x) = 1$ . A periodic orbit $P$ of $H_0$ is a map $x_P : \mathbb{R} \to \mathbb{R}^4$ and $T_P > 0$ with $x_P'(t) = X(x_P(t))$ and $H_0(x_P(t)) = 1$ for all $t$ , and $x_P(t + T_P) = x_P(t)$ (not necessarily the minimal period). A linearized flow along $x_P$ is a map $Y$ from $\mathbb{R}$ to linear maps $\mathbb{R}^4 \to \mathbb{R}^4$ with $Y(0) = \mathrm{id}$ and $Y'(t) = DX(x_P(t)) \circ Y(t)$ for all $t$ . Given $Y$ , $M_Y$ is the real $2 \times 2$ matrix

(M_Y)_{ij} = \Big[\kappa_{x_P(T_P)}\Big(\pi_{x_P(T_P)}\big(Y(T_P)\, g_j\big)\Big)\Big]_i, \qquad g_0 = f_1(x_P(0)),\ g_1 = f_2(x_P(0)),

(this is the value at time $1$ of the path $\tau \mapsto$ the analogous matrix built at $x_P(T_P \tau)$ with $Y(T_P \tau)$ ).

Definitions on $V = \mathbb{R}^{2(1+1)} = \mathbb{R}^4$ (second family). Identify $\mathbb{R}^4$ with $V$ coordinatewise (index $k \mapsto k$ ), and let $H : V \to \mathbb{R}$ be $H_0$ under this identification. On $V$ : $(j_0 v) = (-v_1, v_0, -v_3, v_2)$ , $\omega_0(u, v) = \langle j_0 u, v \rangle$ , $\lambda_x(v) = \tfrac12 \omega_0(x, v)$ , $X_H = j_0 \nabla H$ with $\nabla H(x) = (dH(x) e_k)_k$ , $R_H(x) = \lambda_x(X_H(x))^{-1} X_H(x)$ (with $0^{-1} = 0$ ), and $\xi_x = \{ v : \lambda_x(v) = 0,\ dH(x) v = 0 \}$ . A Reeb orbit $Q$ of $H$ is $x_Q : \mathbb{R} \to V$ and $T_Q > 0$ with $H(x_Q(\tau)) = 1$ , $x_Q'(\tau) = R_H(x_Q(\tau))$ , $x_Q(\tau + T_Q) = x_Q(\tau)$ for all $\tau$ ( $T_Q$ not necessarily minimal). " $Q$ is nondegenerate" means: for every $\Phi$ from $\mathbb{R}$ to linear maps $V \to V$ with $\Phi(0) = \mathrm{id}$ and $\Phi'(\tau) = DR_H(x_Q(\tau)) \circ \Phi(\tau)$ for all $\tau$ , and every $v \in \xi_{x_Q(0)}$ with $\Phi(T_Q) v = v$ , one has $v = 0$ .

Statement. Let $H_0 : \mathbb{R}^4 \to \mathbb{R}$ be a strictly star-shaped level (first family; no separate hypothesis is stated for $H$ ). For every periodic orbit $P$ of $H_0$ and every Reeb orbit $Q$ of $H$ such that

the image of $x_Q$ equals the image of $x_P$ (under the identification), and

T_Q = \int_0^{T_P} \lambda_{x_P(\tau)}\big(x_P'(\tau)\big)\, d\tau,

the following equivalence holds:

Q \text{ is nondegenerate} \iff \text{for every linearized flow } Y \text{ along } x_P \text{ and every } v \in \mathbb{R}^2 \text{ with } M_Y v = v, \ v = 0.

No relation between the parametrizations of $x_P$ and $x_Q$ (base points, direction, speed) is assumed beyond equality of images and the period identity. Both sides of the equivalence quantify universally over solutions ( $\Phi$ , resp. $Y$ ) of the respective linear equations; either side holds vacuously if no such solution exists.

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

Nondegeneracy of Reeb orbits in R4\mathbb{R}^4R4 and of Hamiltonian periodic orbits

Read-back: FiniteEnergyPlane.isNondegenerate_bridge

Nondegeneracy of Reeb orbits in $\mathbb{R}^4$ and of Hamiltonian periodic orbits

Read-back: `FiniteEnergyPlane.isNondegenerate_bridge`