Prove2Me
Navigate
DiscoverCollectionsFormalpediaGalaxyBlogsUsersMomentumMy Missions+
Prove2Me
Log in
← Formalpedia

Compactness of fast finite-energy planes

Proved
FiniteEnergyPlane.isSeqCompact_fastPlaneSet

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

compactnessfast-planespseudoholomorphic-curvesreeb-dynamicssymplectic-geometrysymplectization

Let H0:R4→RH_0:\mathbb{R}^4\to\mathbb{R}H0​:R4→R have a strictly star-shaped level (in the sense of HryniewiczCriterion), HHH the same function on V=R2⋅(1+1)V=\mathbb{R}^{2\cdot(1+1)}V=R2⋅(1+1), JJJ a smooth dλ0d\lambda_0dλ0​-compatible complex structure on ξ\xiξ and PPP a periodic Reeb orbit of HHH. Suppose every periodic orbit of HryniewiczCriterion of action at most TPT_PTP​ is nondegenerate and has μCZ≥3\mu_{CZ}\ge3μCZ​≥3. Let γ>0\gamma>0γ>0 be smaller than every period at most TPT_PTP​ and than every difference of two distinct such periods, and let K⊂R4∖{0}K\subset\mathbb{R}^4\setminus\{0\}K⊂R4∖{0} be compact with K∩(R×x(R))=∅K\cap(\mathbb{R}\times x(\mathbb{R}))=\emptysetK∩(R×x(R))=∅, where P=(x,TP)P=(x,T_P)P=(x,TP​). Then Θ(K,P)\Theta(K,P)Θ(K,P) is sequentially compact in Cloc∞(C,R4)C^\infty_{loc}(\mathbb{C},\mathbb{R}^4)Cloc∞​(C,R4).

Formalization Note The orbit hypotheses have the form of exists_transverse_disk_open_book_of_approx at a single level: for every R : PeriodicOrbit H₀ and Y with IsLinearizedFlow H₀ R.x Y and action ∫0TRλ0(x˙)≤TP\int_0^{T_R}\lambda_0(\dot x)\le T_P∫0TR​​λ0​(x˙)≤TP​, linearizedXiPath H₀ R Y 1 fixes no nonzero vector and 3 ≤ czIndexOfPath (linearizedXiPath H₀ R Y). K∩(R×x(R))=∅K\cap(\mathbb{R}\times x(\mathbb{R}))=\emptysetK∩(R×x(R))=∅ is ∀ y ∈ K, proj H y ∉ Set.range P.x. Θ(K,P)\Theta(K,P)Θ(K,P) is fastPlaneSet H J P K γ.

Preamble
import Definitions.Def_FiniteEnergyPlane_Compactness
Formal statement
namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- Hryniewicz (Trans. AMS 2012), Theorem 2.2 (2), for `Θ`; Hryniewicz (J. Symplectic Geom. 2014),
Theorem 3.10. Let `S = H⁻¹(1) ⊂ ℝ⁴` be strictly star-shaped and `P` a periodic Reeb orbit. Suppose
every periodic orbit of `HryniewiczCriterion` of action at most `P.T` is nondegenerate with
Conley–Zehnder index at least `3` (as in `exists_transverse_disk_open_book_of_approx`), let
`0 < γ` be smaller than every period at most `P.T` and every difference of two distinct such
periods, and let `K ⊂ V 1 \ {0}` be a compact set disjoint from the cone `ℝ × x(ℝ)` over the image
of `P`. Then `fastPlaneSet H J P K γ` is sequentially compact in `C^∞_loc(ℂ, V 1)`. -/
theorem isSeqCompact_fastPlaneSet (H₀ : HryniewiczCriterion.R4 → ℝ)
    (hH₀ : HryniewiczCriterion.IsStrictlyStarShapedLevel H₀) :
    let H : V 1 → ℝ := fun y => H₀ (fun k => y (Fin.cast (by norm_num) k))
    ∀ J : V 1 → V 1 →L[ℝ] V 1, IsCompatibleXiStructure H J → ∀ P : ReebOrbit H,
    (∀ (R : HryniewiczCriterion.PeriodicOrbit H₀)
      (Y : ℝ → (HryniewiczCriterion.R4 →L[ℝ] HryniewiczCriterion.R4)),
      HryniewiczCriterion.IsLinearizedFlow H₀ R.x Y →
      (∫ t in (0 : ℝ)..R.T, HryniewiczCriterion.liouvilleForm (R.x t) (deriv R.x t)) ≤ P.T →
      ∀ v : Fin 2 → ℝ, (HryniewiczCriterion.linearizedXiPath H₀ R Y 1).mulVec v = v → v = 0) →
    (∀ (R : HryniewiczCriterion.PeriodicOrbit H₀)
      (Y : ℝ → (HryniewiczCriterion.R4 →L[ℝ] HryniewiczCriterion.R4)),
      HryniewiczCriterion.IsLinearizedFlow H₀ R.x Y →
      (∫ t in (0 : ℝ)..R.T, HryniewiczCriterion.liouvilleForm (R.x t) (deriv R.x t)) ≤ P.T →
      3 ≤ HryniewiczCriterion.czIndexOfPath (HryniewiczCriterion.linearizedXiPath H₀ R Y)) →
    ∀ γ : ℝ, 0 < γ → (∀ Q : ReebOrbit H, Q.T ≤ P.T → γ < Q.T) →
    (∀ Q₁ Q₂ : ReebOrbit H, Q₁.T ≤ P.T → Q₂.T ≤ P.T → Q₁.T ≠ Q₂.T → γ < |Q₁.T - Q₂.T|) →
    ∀ K : Set (V 1), IsCompact K → (0 : V 1) ∉ K → (∀ y ∈ K, proj H y ∉ Set.range P.x) →
    IsSeqCompactCInftyLoc (fastPlaneSet H J P K γ) := 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, Theorem 2.2 (2); 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, Theorem 3.10
Read-back

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

Read-back: FiniteEnergyPlane.isSeqCompact_fastPlaneSet

Ambient notation. Work in V=R4V = \mathbb{R}^4V=R4 with coordinates y0,y1,y2,y3y_0, y_1, y_2, y_3y0​,y1​,y2​,y3​ (the dimension 2(n+1)2(n+1)2(n+1) with n=1n = 1n=1). Let ω0(u,v)=u0v1−u1v0+u2v3−u3v2\omega_0(u,v) = u_0 v_1 - u_1 v_0 + u_2 v_3 - u_3 v_2ω0​(u,v)=u0​v1​−u1​v0​+u2​v3​−u3​v2​, λx(v)=12ω0(x,v)\lambda_x(v) = \tfrac12 \omega_0(x, v)λx​(v)=21​ω0​(x,v), j0(v)=(−v1,v0,−v3,v2)j_0(v) = (-v_1, v_0, -v_3, v_2)j0​(v)=(−v1​,v0​,−v3​,v2​), (∇H(x))k=dHx(ek)(\nabla H(x))_k = dH_x(e_k)(∇H(x))k​=dHx​(ek​), and XH=j0∇H=(−∂1H,∂0H,−∂3H,∂2H)X_H = j_0 \nabla H = (-\partial_1 H, \partial_0 H, -\partial_3 H, \partial_2 H)XH​=j0​∇H=(−∂1​H,∂0​H,−∂3​H,∂2​H). The Reeb field is RH(x)=λx(XH(x))−1XH(x)R_H(x) = \lambda_x(X_H(x))^{-1} X_H(x)RH​(x)=λx​(XH​(x))−1XH​(x) (with 0−1=00^{-1} = 00−1=0). Write ξx={v:λx(v)=0, dHx(v)=0}\xi_x = \{ v : \lambda_x(v) = 0,\ dH_x(v) = 0\}ξx​={v:λx​(v)=0, dHx​(v)=0} and SH={H=1}S_H = \{H = 1\}SH​={H=1}.

  • Strictly star-shaped level HHH: HHH is C∞C^\inftyC∞; every u≠0u \ne 0u=0 has exactly one r>0r > 0r>0 with H(ru)=1H(ru) = 1H(ru)=1; dHx(x)>0dH_x(x) > 0dHx​(x)>0 whenever H(x)=1H(x) = 1H(x)=1.
  • Compatible ξ\xiξ-structure JJJ: J:V→End(V)J : V \to \mathrm{End}(V)J:V→End(V) is C∞C^\inftyC∞, and for every x∈SHx \in S_Hx∈SH​ and v,w∈ξxv, w \in \xi_xv,w∈ξx​: J(x)v∈ξxJ(x)v \in \xi_xJ(x)v∈ξx​, J(x)2v=−vJ(x)^2 v = -vJ(x)2v=−v, ω0(v,J(x)v)>0\omega_0(v, J(x)v) > 0ω0​(v,J(x)v)>0 if v≠0v \ne 0v=0, ω0(J(x)v,J(x)w)=ω0(v,w)\omega_0(J(x)v, J(x)w) = \omega_0(v,w)ω0​(J(x)v,J(x)w)=ω0​(v,w). Nothing is required off SHS_HSH​ or outside ξx\xi_xξx​.
  • Scaling, projection, aaa-coordinate. sH(y)s_H(y)sH​(y) is some r>0r > 0r>0 with H(ry)=1H(ry) = 1H(ry)=1 if one exists (chosen by choice), otherwise 111; πH(y)=sH(y) y\pi_H(y) = s_H(y)\, yπH​(y)=sH​(y)y; aH(y)=−12log⁡sH(y)a_H(y) = -\tfrac12 \log s_H(y)aH​(y)=−21​logsH​(y). As sH>0s_H > 0sH​>0 always, e−2aH(y)=sH(y)e^{-2a_H(y)} = s_H(y)e−2aH​(y)=sH​(y), so e−2aH(y)y=πH(y)e^{-2a_H(y)} y = \pi_H(y)e−2aH​(y)y=πH​(y).
  • J~\tilde JJ~: for y∈Vy \in Vy∈V, with x=πH(y)x = \pi_H(y)x=πH​(y), r=sH(y)r = s_H(y)r=sH​(y), α(v)=r dHx(v)2dHx(x)\alpha(v) = \frac{r\, dH_x(v)}{2 dH_x(x)}α(v)=2dHx​(x)rdHx​(v)​, β(v)=rλx(v)\beta(v) = r \lambda_x(v)β(v)=rλx​(v), w(v)=v−2α(v)y−β(v)r−1RH(x)w(v) = v - 2\alpha(v) y - \beta(v) r^{-1} R_H(x)w(v)=v−2α(v)y−β(v)r−1RH​(x):  J~(y)v=α(v)r−1RH(x)−2β(v)y+J(x)w(v)\ \tilde J(y) v = \alpha(v) r^{-1} R_H(x) - 2\beta(v) y + J(x) w(v) J~(y)v=α(v)r−1RH​(x)−2β(v)y+J(x)w(v).
  • Derivatives. For fff on C\mathbb{C}C: ∂sf(z)=Df(z)[1]\partial_s f(z) = Df(z)[1]∂s​f(z)=Df(z)[1], ∂tf(z)=Df(z)[i]\partial_t f(z) = Df(z)[i]∂t​f(z)=Df(z)[i] (real Fréchet derivative; 000 where not differentiable).
  • Energies. Admissible φ\varphiφ: C∞C^\inftyC∞, non-decreasing, values in [0,1][0,1][0,1]. With a=aH∘ua = a_H \circ ua=aH​∘u, w=πH∘uw = \pi_H \circ uw=πH​∘u and eφ=φ′(a)(∂sa λw(∂tw)−∂ta λw(∂sw))+φ(a) ω0(∂sw,∂tw)e_\varphi = \varphi'(a)(\partial_s a\, \lambda_w(\partial_t w) - \partial_t a\, \lambda_w(\partial_s w)) + \varphi(a)\, \omega_0(\partial_s w, \partial_t w)eφ​=φ′(a)(∂s​aλw​(∂t​w)−∂t​aλw​(∂s​w))+φ(a)ω0​(∂s​w,∂t​w), the energy is EH(U,u)=sup⁡φ∫Umax⁡(eφ,0)∈[0,∞]E_H(U,u) = \sup_\varphi \int_U \max(e_\varphi, 0) \in [0,\infty]EH​(U,u)=supφ​∫U​max(eφ​,0)∈[0,∞], and the dλd\lambdadλ-energy is EHdλ(U,u)=∫Umax⁡(ω0(∂sw,∂tw),0)∈[0,∞]E^{d\lambda}_H(U,u) = \int_U \max(\omega_0(\partial_s w, \partial_t w), 0) \in [0,\infty]EHdλ​(U,u)=∫U​max(ω0​(∂s​w,∂t​w),0)∈[0,∞] (Lebesgue measure; negative parts of the densities are cut off before integrating).
  • Finite-energy curve on UUU: u:C→Vu : \mathbb{C} \to Vu:C→V is C∞C^\inftyC∞ on UUU, u(z)≠0u(z) \ne 0u(z)=0 on UUU, at every z∈Uz \in Uz∈U it is differentiable with ∂su(z)+J~(u(z)) ∂tu(z)=0\partial_s u(z) + \tilde J(u(z))\, \partial_t u(z) = 0∂s​u(z)+J~(u(z))∂t​u(z)=0, and EH(U,u)<∞E_H(U,u) < \inftyEH​(U,u)<∞.
  • Reeb orbit QQQ: a map xQ:R→Vx_Q : \mathbb{R} \to VxQ​:R→V and a number TQ>0T_Q > 0TQ​>0 with xQ(τ)∈SHx_Q(\tau) \in S_HxQ​(τ)∈SH​, xQ′(τ)=RH(xQ(τ))x_Q'(\tau) = R_H(x_Q(\tau))xQ′​(τ)=RH​(xQ​(τ)), xQ(τ+TQ)=xQ(τ)x_Q(\tau + T_Q) = x_Q(\tau)xQ​(τ+TQ​)=xQ​(τ). TQT_QTQ​ is any period, not necessarily minimal, so multiple covers count as separate orbits. QQQ is prime if xQ(τ)≠xQ(0)x_Q(\tau) \ne x_Q(0)xQ​(τ)=xQ​(0) for 0<τ<TQ0 < \tau < T_Q0<τ<TQ​. QQQ is nondegenerate if for every Φ:R→End(V)\Phi : \mathbb{R} \to \mathrm{End}(V)Φ:R→End(V) with Φ(0)=id\Phi(0) = \mathrm{id}Φ(0)=id and Φ′(τ)=DRH(xQ(τ))∘Φ(τ)\Phi'(\tau) = DR_H(x_Q(\tau)) \circ \Phi(\tau)Φ′(τ)=DRH​(xQ​(τ))∘Φ(τ) for all τ\tauτ, every v∈ξxQ(0)v \in \xi_{x_Q(0)}v∈ξxQ​(0)​ with Φ(TQ)v=v\Phi(T_Q)v = vΦ(TQ​)v=v is 000.
  • Hamiltonian periodic orbits and the index μ\muμ. A Hamiltonian periodic orbit RRR of a function GGG on R4\mathbb{R}^4R4 is xR:R→R4x_R : \mathbb{R} \to \mathbb{R}^4xR​:R→R4, TR>0T_R > 0TR​>0 with xR′=XG(xR)x_R' = X_G(x_R)xR′​=XG​(xR​), G(xR)=1G(x_R) = 1G(xR​)=1, xR(t+TR)=xR(t)x_R(t + T_R) = x_R(t)xR​(t+TR​)=xR​(t). A linearized flow along xRx_RxR​ is Y:R→End(R4)Y : \mathbb{R} \to \mathrm{End}(\mathbb{R}^4)Y:R→End(R4) with Y(0)=idY(0) = \mathrm{id}Y(0)=id, Y′(t)=DXG(xR(t))∘Y(t)Y'(t) = DX_G(x_R(t)) \circ Y(t)Y′(t)=DXG​(xR​(t))∘Y(t). With Q1x=(−x2,x3,x0,−x1)Q_1 x = (-x_2, x_3, x_0, -x_1)Q1​x=(−x2​,x3​,x0​,−x1​), Q2x=(x3,x2,−x1,−x0)Q_2 x = (x_3, x_2, -x_1, -x_0)Q2​x=(x3​,x2​,−x1​,−x0​), ∣x∣|x|∣x∣ the Euclidean norm, set F1(x)=∣x∣−1(Q2x−dGx(Q2x)dGx(x)x)F_1(x) = |x|^{-1}\big(Q_2 x - \tfrac{dG_x(Q_2 x)}{dG_x(x)} x\big)F1​(x)=∣x∣−1(Q2​x−dGx​(x)dGx​(Q2​x)​x), F2(x)=∣x∣−1(Q1x−dGx(Q1x)dGx(x)x)F_2(x) = |x|^{-1}\big(Q_1 x - \tfrac{dG_x(Q_1 x)}{dG_x(x)} x\big)F2​(x)=∣x∣−1(Q1​x−dGx​(x)dGx​(Q1​x)​x) (division by 000 read as multiplication by 000), the coordinates cx(v)=(ω0(v,F2(x)), ω0(F1(x),v))∈R2c_x(v) = \big(\omega_0(v, F_2(x)),\ \omega_0(F_1(x), v)\big) \in \mathbb{R}^2cx​(v)=(ω0​(v,F2​(x)), ω0​(F1​(x),v))∈R2, and px(v)=v−λx(v)λx(XG(x))XG(x)p_x(v) = v - \frac{\lambda_x(v)}{\lambda_x(X_G(x))} X_G(x)px​(v)=v−λx​(XG​(x))λx​(v)​XG​(x). The linearized ξ\xiξ-path is the 2×22 \times 22×2 matrix path
ϕR,Y(τ)=[ cxR(TRτ)(pxR(TRτ)(Y(TRτ) Fj(xR(0)))) ]j=1,2(column j).\phi_{R,Y}(\tau) = \Big[\, c_{x_R(T_R\tau)}\big(p_{x_R(T_R\tau)}\big(Y(T_R\tau)\, F_j(x_R(0))\big)\big) \,\Big]_{j = 1,2} \quad (\text{column } j).ϕR,Y​(τ)=[cxR​(TR​τ)​(pxR​(TR​τ)​(Y(TR​τ)Fj​(xR​(0))))]j=1,2​(column j).

For a 2×22\times 22×2 matrix path ϕ\phiϕ, an angle lift from sss is θ:R→R\theta : \mathbb{R} \to \mathbb{R}θ:R→R, continuous on [0,1][0,1][0,1], with θ(0)=s\theta(0) = sθ(0)=s and, for each t∈[0,1]t \in [0,1]t∈[0,1], ϕ(t)(cos⁡s,sin⁡s)=r(cos⁡θ(t),sin⁡θ(t))\phi(t)(\cos s, \sin s) = r(\cos\theta(t), \sin\theta(t))ϕ(t)(coss,sins)=r(cosθ(t),sinθ(t)) for some r>0r > 0r>0. Let I(ϕ)={(θ(1)−s)/(2π):s∈[0,2π], θ an angle lift from s}I(\phi) = \{ (\theta(1) - s)/(2\pi) : s \in [0, 2\pi],\ \theta \text{ an angle lift from } s \}I(ϕ)={(θ(1)−s)/(2π):s∈[0,2π], θ an angle lift from s}, a=inf⁡I(ϕ)a = \inf I(\phi)a=infI(ϕ), b=sup⁡I(ϕ)b = \sup I(\phi)b=supI(ϕ) (real infimum/supremum, which take the value 000 when I(ϕ)I(\phi)I(ϕ) is empty or unbounded on that side), and

μ(ϕ)={2(⌈b⌉−1)if a≤⌈b⌉−1,2⌈b⌉−1otherwise.\mu(\phi) = \begin{cases} 2(\lceil b \rceil - 1) & \text{if } a \le \lceil b \rceil - 1, \\ 2\lceil b \rceil - 1 & \text{otherwise.} \end{cases}μ(ϕ)={2(⌈b⌉−1)2⌈b⌉−1​if a≤⌈b⌉−1,otherwise.​
  • "CZ index at least mmm" for a Reeb orbit QQQ of HHH: for every Hamiltonian periodic orbit RRR of G=HG = HG=H with xR(R)=xQ(R)x_R(\mathbb{R}) = x_Q(\mathbb{R})xR​(R)=xQ​(R) and TQ=∫0TRλxR(τ)(xR′(τ)) dτT_Q = \int_0^{T_R} \lambda_{x_R(\tau)}(x_R'(\tau))\, d\tauTQ​=∫0TR​​λxR​(τ)​(xR′​(τ))dτ, and every linearized flow YYY along xRx_RxR​, m≤μ(ϕR,Y)m \le \mu(\phi_{R,Y})m≤μ(ϕR,Y​). (Vacuous if no such RRR exists.)
  • Cylindrical end at infinity e∞(s,t)=e2πse2πite_\infty(s,t) = e^{2\pi s} e^{2\pi i t}e∞​(s,t)=e2πse2πit, with W(s,t)=πH(u(e∞(s,t)))W(s,t) = \pi_H(u(e_\infty(s,t)))W(s,t)=πH​(u(e∞​(s,t))), A(s,t)=aH(u(e∞(s,t)))A(s,t) = a_H(u(e_\infty(s,t)))A(s,t)=aH​(u(e∞​(s,t))). uuu has a nondegenerate end at ∞\infty∞ asymptotic to QQQ if there are d,c∈Rd, c \in \mathbb{R}d,c∈R, b>0b > 0b>0 with sup⁡t∣A(s,t)−TQs−d∣→0\sup_t |A(s,t) - T_Q s - d| \to 0supt​∣A(s,t)−TQ​s−d∣→0 and sup⁡tebs∣W(s,t)−xQ(TQt+c)∣→0\sup_t e^{bs} |W(s,t) - x_Q(T_Q t + c)| \to 0supt​ebs∣W(s,t)−xQ​(TQ​t+c)∣→0 as s→+∞s \to +\inftys→+∞.
  • Winding and zero index. A loop f:R→Cf : \mathbb{R} \to \mathbb{C}f:R→C has winding k∈Zk \in \mathbb{Z}k∈Z if it is continuous, 111-periodic, never 000, and f(t)=∣f(t)∣eiθ(t)f(t) = |f(t)| e^{i\theta(t)}f(t)=∣f(t)∣eiθ(t) for some continuous θ\thetaθ with θ(1)−θ(0)=2πk\theta(1) - \theta(0) = 2\pi kθ(1)−θ(0)=2πk. f:C→Cf : \mathbb{C} \to \mathbb{C}f:C→C has zero index mmm at z0z_0z0​ if f(z0)=0f(z_0) = 0f(z0​)=0 and for some r>0r > 0r>0, f≠0f \ne 0f=0 on 0<∣z−z0∣≤r0 < |z - z_0| \le r0<∣z−z0​∣≤r and every loop t↦f(z0+ρe2πit)t \mapsto f(z_0 + \rho e^{2\pi i t})t↦f(z0​+ρe2πit), ρ∈(0,r)\rho \in (0, r)ρ∈(0,r), has winding mmm.
  • Πu\Pi_uΠu​: with ζx(v)=ω0(v,F2(x))+i ω0(F1(x),v)\zeta_x(v) = \omega_0(v, F_2(x)) + i\, \omega_0(F_1(x), v)ζx​(v)=ω0​(v,F2​(x))+iω0​(F1​(x),v) (the frame FjF_jFj​ built from G=HG = HG=H) and πxξ(v)=v−λx(v)RH(x)\pi^\xi_x(v) = v - \lambda_x(v) R_H(x)πxξ​(v)=v−λx​(v)RH​(x), put Πu(z)=ζp(πpξ(∂s(πH∘u)(z)))\Pi_u(z) = \zeta_p\big(\pi^\xi_p(\partial_s(\pi_H \circ u)(z))\big)Πu​(z)=ζp​(πpξ​(∂s​(πH​∘u)(z))) with p=πH(u(z))p = \pi_H(u(z))p=πH​(u(z)).
  • Fast plane: uuu is a finite-energy curve on all of C\mathbb{C}C; there is a prime Reeb orbit QQQ such that uuu has a nondegenerate end at ∞\infty∞ asymptotic to QQQ; and the zero set of Πu\Pi_uΠu​ in C\mathbb{C}C is a finite set ZZZ for which there are integers idx(z)\mathrm{idx}(z)idx(z), each the zero index of Πu\Pi_uΠu​ at zzz, with ∑z∈Zidx(z)=0\sum_{z \in Z} \mathrm{idx}(z) = 0∑z∈Z​idx(z)=0.
  • The set F(P,K,γ)\mathcal{F}(P, K, \gamma)F(P,K,γ) (for a Reeb orbit PPP, K⊆VK \subseteq VK⊆V, γ∈R\gamma \in \mathbb{R}γ∈R): all u:C→Vu : \mathbb{C} \to Vu:C→V that are fast planes, have a nondegenerate end at ∞\infty∞ asymptotic to PPP, satisfy u(0)∈Ku(0) \in Ku(0)∈K, and satisfy EHdλ({∣z∣>1},u)=max⁡(γ,0)E^{d\lambda}_H(\{|z| > 1\}, u) = \max(\gamma, 0)EHdλ​({∣z∣>1},u)=max(γ,0).
  • Cloc∞C^\infty_{\mathrm{loc}}Cloc∞​ convergence on O⊆CO \subseteq \mathbb{C}O⊆C: fk→gf_k \to gfk​→g means that for every compact K′⊆OK' \subseteq OK′⊆O and every m∈Nm \in \mathbb{N}m∈N, the mmm-th iterated real Fréchet derivatives DmfkD^m f_kDmfk​ converge to DmgD^m gDmg uniformly on K′K'K′ (the iterated derivatives are total functions, defined at every point).
  • Sequential Cloc∞C^\infty_{\mathrm{loc}}Cloc∞​-compactness of a set A\mathcal{A}A of maps C→V\mathbb{C} \to VC→V: for every sequence (uk)(u_k)(uk​) in A\mathcal{A}A there are a strictly increasing φ:N→N\varphi : \mathbb{N} \to \mathbb{N}φ:N→N and v∈Av \in \mathcal{A}v∈A with uφ(k)→vu_{\varphi(k)} \to vuφ(k)​→v in Cloc∞C^\infty_{\mathrm{loc}}Cloc∞​ on all of C\mathbb{C}C.

Statement. Let H0:R4→RH_0 : \mathbb{R}^4 \to \mathbb{R}H0​:R4→R be a strictly star-shaped level function (same definition as above: C∞C^\inftyC∞, unique positive radial solution of H0(ru)=1H_0(ru) = 1H0​(ru)=1 for each u≠0u \ne 0u=0, dH0∣x(x)>0dH_0|_x(x) > 0dH0​∣x​(x)>0 on {H0=1}\{H_0 = 1\}{H0​=1}). Let H:V→RH : V \to \mathbb{R}H:V→R be H0H_0H0​ read on V=R4V = \mathbb{R}^4V=R4 through the coordinate identification V≅R4V \cong \mathbb{R}^4V≅R4 that matches coordinate kkk with coordinate kkk (so HHH and H0H_0H0​ are the same function of (y0,y1,y2,y3)(y_0, y_1, y_2, y_3)(y0​,y1​,y2​,y3​)). Then for every compatible ξ\xiξ-structure JJJ for HHH and every Reeb orbit PPP of HHH, the following holds.

Assume, for every Hamiltonian periodic orbit RRR of G=H0G = H_0G=H0​ (any period TR>0T_R > 0TR​>0, not necessarily prime, not required to be related to PPP) and every linearized flow YYY along xRx_RxR​, whenever the action satisfies

∫0TRλxR(t)(xR′(t)) dt  ≤  TP,\int_0^{T_R} \lambda_{x_R(t)}\big(x_R'(t)\big)\, dt \;\le\; T_P,∫0TR​​λxR​(t)​(xR′​(t))dt≤TP​,

(here λx(v)=12(x0v1−x1v0+x2v3−x3v2)\lambda_x(v) = \tfrac12(x_0 v_1 - x_1 v_0 + x_2 v_3 - x_3 v_2)λx​(v)=21​(x0​v1​−x1​v0​+x2​v3​−x3​v2​)):

  • (i) every v∈R2v \in \mathbb{R}^2v∈R2 with ϕR,Y(1) v=v\phi_{R,Y}(1)\, v = vϕR,Y​(1)v=v is v=0v = 0v=0 (i.e. 111 is not an eigenvalue of ϕR,Y(1)\phi_{R,Y}(1)ϕR,Y​(1)); and
  • (ii) 3≤μ(ϕR,Y)3 \le \mu(\phi_{R,Y})3≤μ(ϕR,Y​).

Let γ∈R\gamma \in \mathbb{R}γ∈R with γ>0\gamma > 0γ>0, γ<TQ\gamma < T_Qγ<TQ​ for every Reeb orbit QQQ of HHH with TQ≤TPT_Q \le T_PTQ​≤TP​, and γ<∣TQ1−TQ2∣\gamma < |T_{Q_1} - T_{Q_2}|γ<∣TQ1​​−TQ2​​∣ for all Reeb orbits Q1,Q2Q_1, Q_2Q1​,Q2​ of HHH with TQ1,TQ2≤TPT_{Q_1}, T_{Q_2} \le T_PTQ1​​,TQ2​​≤TP​ and TQ1≠TQ2T_{Q_1} \ne T_{Q_2}TQ1​​=TQ2​​. Let K⊆R4K \subseteq \mathbb{R}^4K⊆R4 be compact with 0∉K0 \notin K0∈/K and with πH(y)∉xP(R)\pi_H(y) \notin x_P(\mathbb{R})πH​(y)∈/xP​(R) for every y∈Ky \in Ky∈K.

Then F(P,K,γ)\mathcal{F}(P, K, \gamma)F(P,K,γ) is sequentially Cloc∞C^\infty_{\mathrm{loc}}Cloc∞​-compact: every sequence in F(P,K,γ)\mathcal{F}(P, K, \gamma)F(P,K,γ) has a strictly increasing subsequence converging in Cloc∞C^\infty_{\mathrm{loc}}Cloc∞​ on all of C\mathbb{C}C to an element of F(P,K,γ)\mathcal{F}(P, K, \gamma)F(P,K,γ).

Remarks on the literal content. Hypotheses (i) and (ii) are stated for Hamiltonian periodic orbits of H0H_0H0​ parametrized by the Hamiltonian vector field XH0X_{H_0}XH0​​ (not the Reeb field), selected by an action bound ≤TP\le T_P≤TP​, and for every linearized flow YYY along them; they are not stated in terms of Reeb orbits of HHH or their nondegeneracy as defined above. In (i), ϕR,Y(1)\phi_{R,Y}(1)ϕR,Y​(1) is the matrix built from Y(TR)Y(T_R)Y(TR​). JJJ and PPP are universally quantified before the hypotheses, so (i), (ii), the conditions on γ\gammaγ and the condition on KKK all refer to the given PPP. If F(P,K,γ)\mathcal{F}(P, K, \gamma)F(P,K,γ) is empty (for instance K=∅K = \emptysetK=∅), the conclusion holds vacuously.

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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paperProve2Me Team
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me