Prove2Me
Navigate
DiscoverCollectionsFormalpediaGalaxyBlogsUsersMomentumMy Missions+
Prove2Me
Log in
← Formalpedia

Fast planes project to immersions transverse to the Reeb field

Proved
FiniteEnergyPlane.isFastPlane_immersion_transverse

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

conley-zehnder-indexpseudoholomorphic-curvesreeb-dynamicssymplectic-geometrysymplectizationwinding-numbers

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ξ. If uuu is a fast finite-energy plane, then w=proj∘u:C→Sw=\mathrm{proj}\circ u:\mathbb{C}\to Sw=proj∘u:C→S is an immersion transverse to the Reeb field: for every zzz and every nonzero v∈Cv\in\mathbb{C}v∈C, dw(z)vdw(z)vdw(z)v is not a real multiple of R(w(z))R(w(z))R(w(z)).

Preamble
import Definitions.Def_FiniteEnergyPlane_Winding
Formal statement
namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- Hryniewicz (Trans. AMS 2012), § 1: if `u` is a fast finite-energy plane, then `w = proj ∘ u :
ℂ → S` is an immersion transverse to the Reeb field: no nonzero tangent vector is mapped to a
multiple of `R`. -/
theorem isFastPlane_immersion_transverse (H : V 1 → ℝ) (hH : IsStrictlyStarShapedLevel H)
    (J : V 1 → V 1 →L[ℝ] V 1) (hJ : IsCompatibleXiStructure H J) (u : ℂ → V 1)
    (hfast : IsFastPlane H J u) :
    ∀ z v : ℂ, v ≠ 0 → ∀ c : ℝ,
      fderiv ℝ (fun z => proj H (u z)) z v ≠ c • reeb H (proj H (u 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, Section 1
Read-back

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

Read-back: FiniteEnergyPlane.isFastPlane_immersion_transverse

Setting. Here V=R4V = \mathbb{R}^4V=R4 with coordinates (v0,v1,v2,v3)(v_0,v_1,v_2,v_3)(v0​,v1​,v2​,v3​), and

j0(v)=(−v1,v0,−v3,v2),ω0(u,v)=⟨j0u,v⟩=u0v1−u1v0+u2v3−u3v2,λx(v)=12 ω0(x,v).j_0(v) = (-v_1, v_0, -v_3, v_2),\qquad \omega_0(u,v) = \langle j_0 u, v\rangle = u_0v_1 - u_1v_0 + u_2v_3 - u_3v_2,\qquad \lambda_x(v) = \tfrac12\,\omega_0(x,v).j0​(v)=(−v1​,v0​,−v3​,v2​),ω0​(u,v)=⟨j0​u,v⟩=u0​v1​−u1​v0​+u2​v3​−u3​v2​,λx​(v)=21​ω0​(x,v).

The gradient of HHH is taken coordinatewise, XH(x)=j0(∇H(x))X_H(x) = j_0(\nabla H(x))XH​(x)=j0​(∇H(x)), and the Reeb field is R(x)=λx(XH(x))−1XH(x)R(x) = \lambda_x(X_H(x))^{-1} X_H(x)R(x)=λx​(XH​(x))−1XH​(x). If λx(XH(x))=0\lambda_x(X_H(x)) = 0λx​(XH​(x))=0, the inverse is 000 by convention, so R(x)=0R(x) = 0R(x)=0. The energy surface is S={H=1}S = \{H = 1\}S={H=1}. The condition "v∈ξxv \in \xi_xv∈ξx​" means λx(v)=0\lambda_x(v) = 0λx​(v)=0 and dHx(v)=0dH_x(v) = 0dHx​(v)=0.

  • Strictly star-shaped HHH: HHH is C∞C^\inftyC∞; for every u≠0u \neq 0u=0 there is exactly one r>0r>0r>0 with H(ru)=1H(ru)=1H(ru)=1; and dHx(x)>0dH_x(x)>0dHx​(x)>0 whenever H(x)=1H(x)=1H(x)=1.
  • Compatible ξ\xiξ-structure J:R4→L(R4,R4)J : \mathbb{R}^4 \to L(\mathbb{R}^4,\mathbb{R}^4)J:R4→L(R4,R4): JJJ is C∞C^\inftyC∞, and for every x∈Sx\in Sx∈S and v,w∈ξxv,w\in\xi_xv,w∈ξx​ we have Jxv∈ξxJ_xv\in\xi_xJx​v∈ξx​, JxJxv=−vJ_xJ_xv=-vJx​Jx​v=−v, ω0(v,Jxv)>0\omega_0(v,J_xv)>0ω0​(v,Jx​v)>0 if v≠0v\ne0v=0, and ω0(Jxv,Jxw)=ω0(v,w)\omega_0(J_xv,J_xw)=\omega_0(v,w)ω0​(Jx​v,Jx​w)=ω0​(v,w). Nothing is required of JxJ_xJx​ off ξx\xi_xξx​ or for x∉Sx\notin Sx∈/S.
  • Reeb orbit P=(x,T)P = (x, T)P=(x,T): a map x:R→R4x:\mathbb{R}\to\mathbb{R}^4x:R→R4 and a number T>0T>0T>0 with x(τ)∈Sx(\tau)\in Sx(τ)∈S, x′(τ)=R(x(τ))x'(\tau)=R(x(\tau))x′(τ)=R(x(τ)) and x(τ+T)=x(τ)x(\tau+T)=x(\tau)x(τ+T)=x(τ) for all τ\tauτ. The period TTT need not be minimal. PPP is called prime if x(τ)≠x(0)x(\tau)\ne x(0)x(τ)=x(0) for all 0<τ<T0<\tau<T0<τ<T.
  • Rescaling: σ(y)\sigma(y)σ(y) is a chosen r>0r>0r>0 with H(ry)=1H(ry)=1H(ry)=1 if one exists, and σ(y)=1\sigma(y)=1σ(y)=1 otherwise. For y≠0y\ne0y=0 this rrr is unique; for y=0y=0y=0 with H(0)=1H(0)=1H(0)=1 it is an arbitrary positive choice. Then proj⁡(y)=σ(y) y\operatorname{proj}(y)=\sigma(y)\,yproj(y)=σ(y)y and a(y)=−12log⁡σ(y)a(y)=-\tfrac12\log\sigma(y)a(y)=−21​logσ(y).
  • Extended structure J~\tilde JJ~: put x=proj⁡(y)x=\operatorname{proj}(y)x=proj(y), r=σ(y)r=\sigma(y)r=σ(y), α(v)=r dHx(v)/(2 dHx(x))\alpha(v)=r\,dH_x(v)/(2\,dH_x(x))α(v)=rdHx​(v)/(2dHx​(x)), β(v)=rλx(v)\beta(v)=r\lambda_x(v)β(v)=rλx​(v) and w(v)=v−α(v) 2y−β(v) r−1R(x)w(v)=v-\alpha(v)\,2y-\beta(v)\,r^{-1}R(x)w(v)=v−α(v)2y−β(v)r−1R(x). Then
J~(y)v=α(v) r−1R(x)−β(v) 2y+Jx(w(v)).\tilde J(y)v=\alpha(v)\,r^{-1}R(x)-\beta(v)\,2y+J_x(w(v)).J~(y)v=α(v)r−1R(x)−β(v)2y+Jx​(w(v)).
  • Finite-energy curve on C\mathbb{C}C: a map u:C→R4u:\mathbb{C}\to\mathbb{R}^4u:C→R4 such that

    • uuu is C∞C^\inftyC∞ on C\mathbb{C}C and u(z)≠0u(z)\ne0u(z)=0 for every zzz;
    • at every zzz, uuu is differentiable and ∂su+J~(u) ∂tu=0\partial_su+\tilde J(u)\,\partial_tu=0∂s​u+J~(u)∂t​u=0, where ∂s\partial_s∂s​ and ∂t\partial_t∂t​ are the derivatives in the directions 111 and iii;
    • E(u)<∞E(u)<\inftyE(u)<∞.

    Here, with au=a∘ua_u=a\circ uau​=a∘u and wu=proj⁡∘uw_u=\operatorname{proj}\circ uwu​=proj∘u,

E(u)=sup⁡φ∫Cmax⁡(0, φ′(au)(∂sau λwu(∂twu)−∂tau λwu(∂swu))+φ(au) ω0(∂swu,∂twu)) dz.E(u)=\sup_\varphi\int_{\mathbb{C}}\max\bigl(0,\ \varphi'(a_u)\bigl(\partial_sa_u\,\lambda_{w_u}(\partial_tw_u)-\partial_ta_u\,\lambda_{w_u}(\partial_sw_u)\bigr)+\varphi(a_u)\,\omega_0(\partial_sw_u,\partial_tw_u)\bigr)\,dz.E(u)=φsup​∫C​max(0, φ′(au​)(∂s​au​λwu​​(∂t​wu​)−∂t​au​λwu​​(∂s​wu​))+φ(au​)ω0​(∂s​wu​,∂t​wu​))dz.

The supremum runs over C∞C^\inftyC∞ monotone φ:R→[0,1]\varphi:\mathbb{R}\to[0,1]φ:R→[0,1], and the integral is a lower Lebesgue integral with values in [0,∞][0,\infty][0,∞].

  • "Nondegenerate end" at ∞\infty∞ asymptotic to PPP with ε=1\varepsilon=1ε=1: let e(s,t)=e2πse2πite(s,t)=e^{2\pi s}e^{2\pi it}e(s,t)=e2πse2πit and W(s,t)=proj⁡(u(e(s,t)))W(s,t)=\operatorname{proj}(u(e(s,t)))W(s,t)=proj(u(e(s,t))). There are d,c,b∈Rd,c,b\in\mathbb{R}d,c,b∈R with b>0b>0b>0 such that, uniformly in t∈Rt\in\mathbb{R}t∈R as s→+∞s\to+\inftys→+∞,
a(u(e(s,t)))−Ts−d→0andebs(W(s,t)−x(Tt+c))→0.a(u(e(s,t)))-Ts-d\to0\qquad\text{and}\qquad e^{bs}\bigl(W(s,t)-x(Tt+c)\bigr)\to0.a(u(e(s,t)))−Ts−d→0andebs(W(s,t)−x(Tt+c))→0.

This condition is only exponential uniform convergence of the end. It says nothing about the linearized return map of PPP.

  • Loop winding: a function f:R→Cf:\mathbb{R}\to\mathbb{C}f:R→C has loop winding k∈Zk\in\mathbb{Z}k∈Z if
    • fff is continuous, 111-periodic and never zero;
    • there is a continuous θ:R→R\theta:\mathbb{R}\to\mathbb{R}θ:R→R with f(t)=∣f(t)∣eiθ(t)f(t)=|f(t)|e^{i\theta(t)}f(t)=∣f(t)∣eiθ(t) for all ttt;
    • θ(1)−θ(0)=2πk\theta(1)-\theta(0)=2\pi kθ(1)−θ(0)=2πk.
  • ξ\xiξ-coordinates: ξC(x,v)=ω0(v,f2(x))+i ω0(f1(x),v)∈C\xi C(x,v)=\omega_0(v,f_2(x))+i\,\omega_0(f_1(x),v)\in\mathbb{C}ξC(x,v)=ω0​(v,f2​(x))+iω0​(f1​(x),v)∈C, with frames
f1(x)=∣x∣−1(Q2x−dHx(Q2x)dHx(x)x),f2(x)=∣x∣−1(Q1x−dHx(Q1x)dHx(x)x),f_1(x)=|x|^{-1}\Bigl(Q_2x-\tfrac{dH_x(Q_2x)}{dH_x(x)}x\Bigr),\qquad f_2(x)=|x|^{-1}\Bigl(Q_1x-\tfrac{dH_x(Q_1x)}{dH_x(x)}x\Bigr),f1​(x)=∣x∣−1(Q2​x−dHx​(x)dHx​(Q2​x)​x),f2​(x)=∣x∣−1(Q1​x−dHx​(x)dHx​(Q1​x)​x),

where Q1x=(−x2,x3,x0,−x1)Q_1x=(-x_2,x_3,x_0,-x_1)Q1​x=(−x2​,x3​,x0​,−x1​) and Q2x=(x3,x2,−x1,−x0)Q_2x=(x_3,x_2,-x_1,-x_0)Q2​x=(x3​,x2​,−x1​,−x0​). Division by 000 gives 000. The Reeb-removing map is πξ(x,v)=v−λx(v)R(x)\pi_\xi(x,v)=v-\lambda_x(v)R(x)πξ​(x,v)=v−λx​(v)R(x).

  • Winding kkk at ∞\infty∞: there is s0s_0s0​ such that, for every s≥s0s\ge s_0s≥s0​, the loop t↦ξC(W(s,t), πξ(W(s,t),∂sW(s,t)))t\mapsto\xi C\bigl(W(s,t),\ \pi_\xi(W(s,t),\partial_sW(s,t))\bigr)t↦ξC(W(s,t), πξ​(W(s,t),∂s​W(s,t))) has loop winding kkk. Here ∂sW\partial_sW∂s​W is the Fréchet derivative of WWW on R2\mathbb{R}^2R2 applied to (1,0)(1,0)(1,0), which is 000 by convention wherever WWW is not differentiable.

  • π\piπ-winding kkk (with no punctures): let wu=proj⁡∘uw_u=\operatorname{proj}\circ uwu​=proj∘u and D(z)=ξC(wu(z), πξ(wu(z),∂swu(z)))D(z)=\xi C\bigl(w_u(z),\ \pi_\xi(w_u(z),\partial_sw_u(z))\bigr)D(z)=ξC(wu​(z), πξ​(wu​(z),∂s​wu​(z))). The condition says the zero set of DDD on C\mathbb{C}C is a finite set ZZZ, and there are integers idx⁡(z)\operatorname{idx}(z)idx(z), for z∈Zz\in Zz∈Z, with ∑z∈Zidx⁡(z)=k\sum_{z\in Z}\operatorname{idx}(z)=k∑z∈Z​idx(z)=k. Each zero z0∈Zz_0\in Zz0​∈Z must have local index idx⁡(z0)\operatorname{idx}(z_0)idx(z0​), meaning:

    • there is r>0r>0r>0 such that z0z_0z0​ is the only zero of DDD in the closed disc Bˉ(z0,r)\bar B(z_0,r)Bˉ(z0​,r);
    • for every ρ∈(0,r)\rho\in(0,r)ρ∈(0,r), the loop t↦D(z0+ρe2πit)t\mapsto D(z_0+\rho e^{2\pi it})t↦D(z0​+ρe2πit) has loop winding idx⁡(z0)\operatorname{idx}(z_0)idx(z0​).

    When k=0k=0k=0, ZZZ need not be empty: only the sum of the indices is 000.

  • Fast plane uuu: uuu is a finite-energy curve on C\mathbb{C}C; there is some prime Reeb orbit P′P'P′ such that uuu has a nondegenerate end at ∞\infty∞ asymptotic to P′P'P′ with ε=1\varepsilon=1ε=1 (in the sense above); and uuu has π\piπ-winding 000 with no punctures.

Statement. Let:

  • H:R4→RH:\mathbb{R}^4\to\mathbb{R}H:R4→R be strictly star-shaped;
  • JJJ be a compatible ξ\xiξ-structure for HHH;
  • u:C→R4u:\mathbb{C}\to\mathbb{R}^4u:C→R4 be a fast plane (as defined above).

No Reeb orbit is fixed in the hypotheses; the fast-plane condition only asserts that one exists.

Write wu=proj⁡∘u:C→R4w_u=\operatorname{proj}\circ u:\mathbb{C}\to\mathbb{R}^4wu​=proj∘u:C→R4, and let Dwu(z):R2→R4Dw_u(z):\mathbb{R}^2\to\mathbb{R}^4Dwu​(z):R2→R4 be its Fréchet derivative over R\mathbb{R}R (taken to be 000 where wuw_uwu​ is not differentiable). Then for every z∈Cz\in\mathbb{C}z∈C, every nonzero v∈Cv\in\mathbb{C}v∈C and every real ccc,

Dwu(z) v ≠ c R(wu(z)).Dw_u(z)\,v\ \ne\ c\,R\bigl(w_u(z)\bigr).Dwu​(z)v = cR(wu​(z)).

The case c=0c=0c=0 is included, so the statement in particular asserts Dwu(z)v≠0Dw_u(z)v\ne0Dwu​(z)v=0 for all v≠0v\ne0v=0, i.e. Dwu(z)Dw_u(z)Dwu​(z) is injective at every zzz. The general case says that no nonzero tangent vector is mapped to a real multiple of the Reeb vector RRR at wu(z)w_u(z)wu​(z) (with RRR as defined above, including the convention R=0R=0R=0 where λx(XH(x))=0\lambda_x(X_H(x))=0λx​(XH​(x))=0).

Human review
  • Endorsed by Shuze Chen · Nov 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Mazecto · Nov 1, 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