Reeb orbits and periodic Hamiltonian orbits on star-shaped levels in $\mathbb{R}^4$

Proved

FiniteEnergyPlane.periodicOrbit_bridge

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

finite-energypseudoholomorphic-curvesreeb-dynamicssymplectic-geometrysymplectization

Identify $\mathbb{R}^4$ with coordinates $(q_1,p_1,q_2,p_2)$ of the HryniewiczCriterion setting with $V$ for $n=1$ coordinatewise, by $\iota$ , and let $H=H_0\circ\iota^{-1}$ . Then $S=H^{-1}(1)$ is a strictly star-shaped level in the sense of this mission if and only if $H_0^{-1}(1)$ is one in the sense of HryniewiczCriterion. If it is, then:

for every periodic orbit $(y,T')$ of $X_{H_0}$ on $H_0^{-1}(1)$ there is a periodic Reeb orbit $(x,T)$ of $H$ with $x(\mathbb{R})=\iota(y(\mathbb{R}))$ and $T=\int_0^{T'}\lambda_0(\iota y)\,\tfrac{d}{d\tau}(\iota y)\,d\tau$ ;
for every periodic Reeb orbit $(x,T)$ of $H$ there is such a periodic orbit $(y,T')$ of $X_{H_0}$ with the same image and with $T$ equal to that action.

Formalization Note $\iota$ is fun x k => x (Fin.cast _ k) from HryniewiczCriterion.R4 = Fin 4 → ℝ to V 1 = Fin (2 * (1 + 1)) → ℝ. Periodic orbits on both sides need not be simple.

Preamble

import Definitions.Def_FiniteEnergyPlane_Setting
import Definitions.Def_HryniewiczCriterion_Basic

Formal statement

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- The case `n = 1` and `HryniewiczCriterion`. Identify `HryniewiczCriterion.R4` with `V 1`
coordinatewise (both are `(q₁, p₁, q₂, p₂)`) by `toV`, and let `H = H₀ ∘ toV⁻¹`. Then the two notions
of a strictly star-shaped level agree, and for such `H₀` every periodic orbit `(x, T)` of `X_{H₀}` on
`H₀⁻¹(1)` has, after `toV`, the same image as a periodic Reeb orbit of `H` whose period is the action
`∫₀ᵀ λ₀(x) x'`; every periodic Reeb orbit of `H` arises in this way. -/
theorem periodicOrbit_bridge (H₀ : HryniewiczCriterion.R4 → ℝ) :
    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))
    (IsStrictlyStarShapedLevel H ↔ HryniewiczCriterion.IsStrictlyStarShapedLevel H₀) ∧
      (HryniewiczCriterion.IsStrictlyStarShapedLevel H₀ →
        (∀ 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 : ReebOrbit H, ∃ P : HryniewiczCriterion.PeriodicOrbit H₀,
          Set.range (fun τ => toV (P.x τ)) = Set.range Q.x ∧
            Q.T = ∫ τ in (0 : ℝ)..P.T, liouville (toV (P.x τ)) (deriv (fun s => toV (P.x s)) τ)) := by
  sorry

end FiniteEnergyPlane

Source

Compatibility with the HryniewiczCriterion setting (case

n=1

); H. Hofer, Pseudoholomorphic curves in symplectizations with applications to the Weinstein conjecture in dimension three, Invent. Math. 114 (1993), 515–563, Section 1

Read-back

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

Read-back: `FiniteEnergyPlane.periodicOrbit_bridge`

Setting. Two copies of $\mathbb R^4$ appear: $\mathbb R^4_{\mathrm{H}}$ (functions on indices $0,1,2,3$ , used by the Hryniewicz-criterion definitions) and $V = \mathbb R^{2(1+1)} = \mathbb R^4$ (used by the finite-energy-plane definitions). The statement fixes an arbitrary function $H_0 : \mathbb R^4_{\mathrm H} \to \mathbb R$ (no hypothesis) and introduces

$\iota : \mathbb R^4_{\mathrm H} \to V$ , $\iota(x)_k = x_k$ for $k = 0,1,2,3$ (the coordinate-wise identification);
$H : V \to \mathbb R$ , $H(y) = H_0(y_0, y_1, y_2, y_3)$ , i.e. $H = H_0 \circ \iota^{-1}$ .

Definitions used (with $\partial_k F(x) = DF(x)\, e_k$ , which is $0$ wherever $F$ is not differentiable).

Strictly star-shaped level (same text on both sides, for $F : \mathbb R^4 \to \mathbb R$ ): $F$ is $C^\infty$ on all of $\mathbb R^4$ ; for every $u \neq 0$ there is exactly one $r > 0$ with $F(r u) = 1$ ; and for every $x$ with $F(x) = 1$ , $DF(x)\,x > 0$ .
Liouville form on $V$ : $\lambda_x(v) = \tfrac12\,\omega_0(x, v)$ with $\omega_0(u,v) = u_0 v_1 - u_1 v_0 + u_2 v_3 - u_3 v_2$ .
Hamiltonian vector field: $X_F(x) = (-\partial_1 F(x),\ \partial_0 F(x),\ -\partial_3 F(x),\ \partial_2 F(x))$ (the same formula is used on both sides).
Reeb field of $H$ on $V$ : $R_H(x) = \lambda_x(X_H(x))^{-1}\, X_H(x)$ , with the convention $0^{-1} = 0$ (so $R_H(x) = 0$ when $\lambda_x(X_H(x)) = 0$ ).
Periodic orbit of $H_0$ (Hryniewicz side): a pair $(x, T)$ with $x : \mathbb R \to \mathbb R^4_{\mathrm H}$ , $T > 0$ , $x$ differentiable at every $t$ with $x'(t) = X_{H_0}(x(t))$ , $H_0(x(t)) = 1$ for all $t$ , and $x(t + T) = x(t)$ for all $t$ . $T$ is any period, not necessarily the minimal one.
Reeb orbit of $H$ (finite-energy-plane side): a pair $(x, T)$ with $x : \mathbb R \to V$ , $T > 0$ , $H(x(\tau)) = 1$ for all $\tau$ , $x$ differentiable at every $\tau$ with $x'(\tau) = R_H(x(\tau))$ , and $x(\tau + T) = x(\tau)$ for all $\tau$ . Again $T$ need not be minimal.

For a periodic orbit $P = (x_P, T_P)$ of $H_0$ define its action

\mathcal A(P) = \int_0^{T_P} \lambda_{\iota(x_P(\tau))}\Big( \tfrac{d}{d\tau}\,\iota(x_P(\tau)) \Big)\, d\tau ,

an oriented interval (Bochner) integral, which by convention is $0$ if the integrand is not integrable; the derivative is the ordinary derivative of $\tau \mapsto \iota(x_P(\tau))$ , taken as $0$ at any point of non-differentiability.

Assertion. The statement is the conjunction of the following:

$H$ is strictly star-shaped (on $V$ ) if and only if $H_0$ is strictly star-shaped (on $\mathbb R^4_{\mathrm H}$ ).
If $H_0$ $H_{0}$ is strictly star-shaped, then both of the following hold:
- (a) for every periodic orbit $P = (x_P, T_P)$ of $H_0$ there is a Reeb orbit $Q = (x_Q, T_Q)$ of $H$ with

x_Q(\mathbb R) = \iota\big(x_P(\mathbb R)\big) \quad\text{and}\quad T_Q = \mathcal A(P);

(b) for every Reeb orbit $Q = (x_Q, T_Q)$ of $H$ there is a periodic orbit $P = (x_P, T_P)$ of $H_0$ with

\iota\big(x_P(\mathbb R)\big) = x_Q(\mathbb R) \quad\text{and}\quad T_Q = \mathcal A(P).

The correspondence is stated only through equality of images (as subsets of $\mathbb R^4$ ) and the equation relating $T_Q$ to the action of $P$ ; no relation between parametrizations, between $T_P$ and $T_Q$ directly, or about minimal periods is asserted, and no uniqueness is claimed. Part 2 carries the star-shapedness of $H_0$ as its only hypothesis; part 1 holds for every $H_0$ , with no hypothesis. If $H_0$ is not strictly star-shaped, part 2 is vacuous.

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

Reeb orbits and periodic Hamiltonian orbits on star-shaped levels in R4\mathbb{R}^4R4

Read-back: FiniteEnergyPlane.periodicOrbit_bridge

Reeb orbits and periodic Hamiltonian orbits on star-shaped levels in $\mathbb{R}^4$

Read-back: `FiniteEnergyPlane.periodicOrbit_bridge`