Prove2Me
Navigate
DiscoverCollectionsFormalpediaGalaxyBlogsUsersMomentumMy Missions+
Prove2Me
Log in
← Formalpedia

Limits of sequences of fast planes

Proved
FiniteEnergyPlane.exists_subseq_tendsto_of_fastPlaneSet

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

compactnessfast-planespseudoholomorphic-curvesreeb-dynamicssymplectic-geometrysymplectization

Let S=H−1(1)⊂R4S=H^{-1}(1)\subset\mathbb{R}^4S=H−1(1)⊂R4 be a strictly star-shaped level and JJJ a smooth dλ0d\lambda_0dλ0​-compatible complex structure on ξ\xiξ. Let PPP be a periodic Reeb orbit such that every periodic Reeb orbit of period at most TPT_PTP​ is nondegenerate with μCZ≥3\mu_{CZ}\ge3μCZ​≥3, let γ>0\gamma>0γ>0 be smaller than every such period 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. Let (uk)(u_k)(uk​) be a sequence in Θ(K,P)\Theta(K,P)Θ(K,P) and write ak=a∘uka_k=a\circ u_kak​=a∘uk​. Then there are a subsequence (ukj)(u_{k_j})(ukj​​), a finite set Γ\GammaΓ in the closed unit disk and a finite-energy J~\tilde JJ~-holomorphic curve www on C∖Γ\mathbb{C}\setminus\GammaC∖Γ with 0<E(w)≤TP0<E(w)\le T_P0<E(w)≤TP​ such that the shifted planes e−2akj(2)ukje^{-2a_{k_j}(2)}u_{k_j}e−2akj​​(2)ukj​​ (the R\mathbb{R}R-coordinate shifted by −akj(2)-a_{k_j}(2)−akj​​(2)) converge to www in Cloc∞(C∖Γ)C^\infty_{loc}(\mathbb{C}\setminus\Gamma)Cloc∞​(C∖Γ), and one of the following holds:

  1. inf⁡akj→−∞\inf a_{k_j}\to-\inftyinfakj​​→−∞, #Γ=1\#\Gamma=1#Γ=1, π dw≡0\pi\,dw\equiv0πdw≡0, and KKK meets the cylinder R×x(R)\mathbb{R}\times x(\mathbb{R})R×x(R) over P=(x,TP)P=(x,T_P)P=(x,TP​);
  2. inf⁡akj→A∈R\inf a_{k_j}\to A\in\mathbb{R}infakj​​→A∈R, Γ=∅\Gamma=\emptysetΓ=∅, akj(2)→c∈Ra_{k_j}(2)\to c\in\mathbb{R}akj​​(2)→c∈R, and ukj→e2cwu_{k_j}\to e^{2c}wukj​​→e2cw in Cloc∞(C)C^\infty_{loc}(\mathbb{C})Cloc∞​(C), where e2cw∈Θ(K,P)e^{2c}w\in\Theta(K,P)e2cw∈Θ(K,P) and a∘(e2cw)≥Aa\circ(e^{2c}w)\ge Aa∘(e2cw)≥A.

Formalization Note Periods are those of ReebOrbit H (not necessarily minimal, so multiple covers count); μCZ≥3\mu_{CZ}\ge3μCZ​≥3 is Q.IsCZAtLeast 3. "inf⁡akj→−∞\inf a_{k_j}\to-\inftyinfakj​​→−∞" is: for every MMM, eventually some zzz has akj(z)≤Ma_{k_j}(z)\le Makj​​(z)≤M. "inf⁡akj→A\inf a_{k_j}\to Ainfakj​​→A" is: for every ε>0\varepsilon>0ε>0, eventually akj≥A−εa_{k_j}\ge A-\varepsilonakj​​≥A−ε everywhere and akj(z)≤A+εa_{k_j}(z)\le A+\varepsilonakj​​(z)≤A+ε somewhere. "π dw≡0\pi\,dw\equiv0πdw≡0" is piDs H w z = 0 for all z∉Γz\notin\Gammaz∈/Γ.

Preamble
import Definitions.Def_FiniteEnergyPlane_Compactness
Formal statement
namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- Hryniewicz (Trans. AMS 2012), Lemma 4.17. Let `P` be a periodic Reeb orbit on `S ⊂ ℝ⁴` such
that every periodic orbit of period at most `P.T` is nondegenerate with Conley–Zehnder index at
least `3`, let `0 < γ` be smaller than every such period and every difference of two distinct such
periods, and let `K ⊂ V 1 \ {0}` be compact. For every sequence `uₖ` in `fastPlaneSet H J P K γ`
there are a subsequence, a finite set `Γ` in the closed unit disk and a finite-energy
`J̃`-holomorphic curve `w` on `ℂ \ Γ` with `0 < E(w) ≤ P.T` such that the shifted planes
`e^{-2aₖ(2)} • uₖ` (`aₖ = aCoord H ∘ uₖ`) converge to `w` in `C^∞_loc(ℂ \ Γ)`, and one of the
following holds:
* `inf aₖ → -∞`, `Γ` has one point, `π dw ≡ 0`, and `K` meets the cone over the image of `P`;
* `inf aₖ → A ∈ ℝ`, `Γ = ∅`, `aₖ(2) → c`, and `uₖ → e^{2c} • w` in `C^∞_loc(ℂ)`, where
  `e^{2c} • w` belongs to `fastPlaneSet H J P K γ` and its coordinate `a` is at least `A`. -/
theorem exists_subseq_tendsto_of_fastPlaneSet (H : V 1 → ℝ) (hH : IsStrictlyStarShapedLevel H)
    (J : V 1 → V 1 →L[ℝ] V 1) (hJ : IsCompatibleXiStructure H J)
    (P : ReebOrbit H)
    (hP : ∀ Q : ReebOrbit H, Q.T ≤ P.T → Q.IsNondegenerate ∧ Q.IsCZAtLeast 3)
    (γ : ℝ) (hγ : 0 < γ) (hγ₁ : ∀ Q : ReebOrbit H, Q.T ≤ P.T → γ < Q.T)
    (hγ₂ : ∀ Q₁ Q₂ : ReebOrbit H, Q₁.T ≤ P.T → Q₂.T ≤ P.T → Q₁.T ≠ Q₂.T → γ < |Q₁.T - Q₂.T|)
    (K : Set (V 1)) (hK : IsCompact K) (hK0 : (0 : V 1) ∉ K)
    (u : ℕ → ℂ → V 1) (hu : ∀ k, u k ∈ fastPlaneSet H J P K γ) :
    ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∃ Γ : Finset ℂ, (∀ z ∈ Γ, ‖z‖ ≤ 1) ∧ ∃ w : ℂ → V 1,
      IsFiniteEnergyCurve H J (↑Γ)ᶜ w ∧ energy H (↑Γ)ᶜ w ≠ 0 ∧
      energy H (↑Γ)ᶜ w ≤ ENNReal.ofReal P.T ∧
      JHolomorphic.TendstoCInftyLocOn
        (fun k z => Real.exp (-(2 * aCoord H (u (φ k) 2))) • u (φ k) z) w (↑Γ)ᶜ ∧
      (((∀ M : ℝ, ∀ᶠ k in atTop, ∃ z, aCoord H (u (φ k) z) ≤ M) ∧ Γ.card = 1 ∧
          (∀ z ∉ Γ, piDs H w z = 0) ∧ ∃ y ∈ K, proj H y ∈ Set.range P.x) ∨
        ∃ A : ℝ, (∀ ε > 0, ∀ᶠ k in atTop, ∀ z, A - ε ≤ aCoord H (u (φ k) z)) ∧
          (∀ ε > 0, ∀ᶠ k in atTop, ∃ z, aCoord H (u (φ k) z) ≤ A + ε) ∧ Γ = ∅ ∧
          ∃ c : ℝ, Tendsto (fun k => aCoord H (u (φ k) 2)) atTop (𝓝 c) ∧
            JHolomorphic.TendstoCInftyLocOn (fun k => u (φ k))
              (fun z => Real.exp (2 * c) • w z) Set.univ ∧
            (fun z => Real.exp (2 * c) • w z) ∈ fastPlaneSet H J P K γ ∧
            ∀ z, A ≤ aCoord H (Real.exp (2 * c) • w z)) := 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, Lemma 4.17
Read-back

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

Read-back: FiniteEnergyPlane.exists_subseq_tendsto_of_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.

Common hypotheses. H:R4→RH : \mathbb{R}^4 \to \mathbb{R}H:R4→R is a strictly star-shaped level function and JJJ is a compatible ξ\xiξ-structure. PPP is a Reeb orbit of HHH such that every Reeb orbit QQQ with TQ≤TPT_Q \le T_PTQ​≤TP​ (including PPP itself and all multiple covers with period ≤TP\le T_P≤TP​) is nondegenerate and has CZ index at least 333 in the sense above. γ∈R\gamma \in \mathbb{R}γ∈R satisfies γ>0\gamma > 0γ>0, γ<TQ\gamma < T_Qγ<TQ​ for every Reeb orbit QQQ 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​ 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​​. K⊆R4K \subseteq \mathbb{R}^4K⊆R4 is compact with 0∉K0 \notin K0∈/K (K=∅K = \emptysetK=∅ is allowed).

Statement. Under the common hypotheses, let (uk)k∈N(u_k)_{k \in \mathbb{N}}(uk​)k∈N​ be a sequence with uk∈F(P,K,γ)u_k \in \mathcal{F}(P, K, \gamma)uk​∈F(P,K,γ) for every kkk. Then there exist a strictly increasing φ:N→N\varphi : \mathbb{N} \to \mathbb{N}φ:N→N, a finite set Γ⊂C\Gamma \subset \mathbb{C}Γ⊂C with ∣z∣≤1|z| \le 1∣z∣≤1 for every z∈Γz \in \Gammaz∈Γ, and a map w:C→R4w : \mathbb{C} \to \mathbb{R}^4w:C→R4 such that:

  1. www is a finite-energy curve on C∖Γ\mathbb{C} \setminus \GammaC∖Γ;
  2. 0<EH(C∖Γ,w)≤TP0 < E_H(\mathbb{C} \setminus \Gamma, w) \le T_P0<EH​(C∖Γ,w)≤TP​;
  3. the rescaled maps
u~k(z)=e−2aH(uφ(k)(2)) uφ(k)(z)=sH(uφ(k)(2)) uφ(k)(z)\tilde u_k(z) = e^{-2 a_H(u_{\varphi(k)}(2))}\, u_{\varphi(k)}(z) = s_H\big(u_{\varphi(k)}(2)\big)\, u_{\varphi(k)}(z)u~k​(z)=e−2aH​(uφ(k)​(2))uφ(k)​(z)=sH​(uφ(k)​(2))uφ(k)​(z)

(rescaling by the constant attached to the value at the point z=2∈Cz = 2 \in \mathbb{C}z=2∈C) converge to www in Cloc∞C^\infty_{\mathrm{loc}}Cloc∞​ on C∖Γ\mathbb{C} \setminus \GammaC∖Γ;

and at least one of the following two alternatives holds (inclusive "or"):

(a) for every M∈RM \in \mathbb{R}M∈R, for all sufficiently large kkk there is z∈Cz \in \mathbb{C}z∈C with aH(uφ(k)(z))≤Ma_H(u_{\varphi(k)}(z)) \le MaH​(uφ(k)​(z))≤M; Γ\GammaΓ has exactly one element; Πw(z)=0\Pi_w(z) = 0Πw​(z)=0 for every z∉Γz \notin \Gammaz∈/Γ; and there is y∈Ky \in Ky∈K with πH(y)∈xP(R)\pi_H(y) \in x_P(\mathbb{R})πH​(y)∈xP​(R).

(b) there is A∈RA \in \mathbb{R}A∈R such that

  • for every ε>0\varepsilon > 0ε>0, for all sufficiently large kkk: aH(uφ(k)(z))≥A−εa_H(u_{\varphi(k)}(z)) \ge A - \varepsilonaH​(uφ(k)​(z))≥A−ε for all z∈Cz \in \mathbb{C}z∈C;
  • for every ε>0\varepsilon > 0ε>0, for all sufficiently large kkk: there is zzz with aH(uφ(k)(z))≤A+εa_H(u_{\varphi(k)}(z)) \le A + \varepsilonaH​(uφ(k)​(z))≤A+ε;
  • Γ=∅\Gamma = \emptysetΓ=∅;

and there is c∈Rc \in \mathbb{R}c∈R such that aH(uφ(k)(2))→ca_H(u_{\varphi(k)}(2)) \to caH​(uφ(k)​(2))→c, the unrescaled subsequence uφ(k)u_{\varphi(k)}uφ(k)​ converges in Cloc∞C^\infty_{\mathrm{loc}}Cloc∞​ on all of C\mathbb{C}C to e2cwe^{2c} we2cw, the map e2cwe^{2c} we2cw belongs to F(P,K,γ)\mathcal{F}(P, K, \gamma)F(P,K,γ), and aH(e2cw(z))≥Aa_H(e^{2c} w(z)) \ge AaH​(e2cw(z))≥A for every z∈Cz \in \mathbb{C}z∈C.

Remarks on the literal content. The energy bound in 2 compares an element of [0,∞][0, \infty][0,∞] with the real number TP>0T_P > 0TP​>0. In (a), the first clause says inf⁡zaH(uφ(k)(z))\inf_z a_H(u_{\varphi(k)}(z))infz​aH​(uφ(k)​(z)) eventually drops below every bound; nothing is said there about convergence of uφ(k)u_{\varphi(k)}uφ(k)​ itself. In (a), "Πw(z)=0\Pi_w(z) = 0Πw​(z)=0 off Γ\GammaΓ" is computed from the total-function definition of Πw\Pi_wΠw​. The common hypotheses on Reeb orbits only concern orbits with period ≤TP\le T_P≤TP​.

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