Let S=H−1(1)⊂R4 be a strictly star-shaped level and J a smooth dλ0-compatible complex structure on ξ. Let P=(x,T) be a periodic Reeb orbit with μCZ(P)≥3 (P may be degenerate) and u an embedded fast finite-energy plane asymptotic to P at ∞. Then u(C) does not meet the cylinder R×x(R).
Formalization Note The puncture at ∞ is IsNondegenerateEnd H u cylInf P 1 (nondegenerate in the sense of Hryniewicz 2014, Definition 2.9); "fast" is IsFastPlane, "embedded" is IsEmbeddedPlane. μCZ(P)≥3 is P.IsCZAtLeast 3, the index of the linearized flow along P in the global frame of ξ; P itself need not be nondegenerate. Hryniewicz writes the hypothesis as μ(u~)≥3, where μ(u~) is the index of P in the class of trivializations of ξ along P that extend over the capping disk u. On a strictly star-shaped level ξ has a global frame, which extends over every capping disk, so μ(u~) is determined by P and equals the index in that frame. The conclusion is proj(u(z))∈/x(R) for every z, the cylinder being the cone {y=0:proj(y)∈x(R)}.
Preamble
import Definitions.Def_FiniteEnergyPlane_Fredholm
Formal statement
namespace FiniteEnergyPlane
open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real
/-- Hryniewicz (Trans. AMS 2012), Lemma 6.24. Let `u` be an embedded fast finite-energy plane
asymptotic to `P` at `∞`, where the Conley–Zehnder index of `P` is at least `3`. Then `u` does not
meet the cone `ℝ × x(ℝ)`: `proj H (u z) ∉ x(ℝ)` for every `z`. -/
theorem proj_not_mem_range_of_isFastPlane (H : V 1 → ℝ) (hH : IsStrictlyStarShapedLevel H)
(J : V 1 → V 1 →L[ℝ] V 1) (hJ : IsCompatibleXiStructure H J)
(P : ReebOrbit H) (hcz : P.IsCZAtLeast 3) (u : ℂ → V 1)
(hu : IsFastPlane H J u) (huP : IsNondegenerateEnd H u cylInf P 1)
(hue : IsEmbeddedPlane u) :
∀ z, proj H (u z) ∉ Set.range P.x := 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 6.24; H. Hofer, K. Wysocki, E. Zehnder, Properties of pseudoholomorphic curves in symplectizations III: Fredholm theory, in Topics in Nonlinear Analysis, Progr. Nonlinear Differential Equations Appl. 35, Birkhäuser 1999, 381–475, doi:10.1007/978-3-0348-8765-6_18, Lemma 8.1
Read-back
What the Lean code literally says, in plain math · claude-opus-5-5
Statement. Let H:R4→R be a Hamiltonian with strictly star-shaped level S={H=1}, let J be a compatible structure on ξ, let P be a Reeb orbit of H with image P satisfying the Conley–Zehnder bound CZ(P)≥3, and let u:C→R4 be a map such that
u is a fast plane for (H,J);
u has a nondegenerate end at infinity at P, i.e. NE(u,P);
u is embedded.
Then, for every z∈C,
pr(u(z))∈/P.
P is not assumed prime. The prime orbit in the definition of "fast plane" is existentially quantified and is not stated to equal P. The Conley–Zehnder bound is a statement about P only, not about other orbits of H, and it may hold vacuously as described below.
Meaning of every symbol used above
Ambient space and linear structures.R4 has coordinates y=(y0,y1,y2,y3). The fixed linear maps and forms are
The Hamiltonian H (hypothesis "strictly star-shaped level"). H:R4→R is C∞; for every y=0 there is exactly one r>0 with H(ry)=1; and dHx(x)>0 at every x with H(x)=1. Write S={H=1}. Nothing is assumed about H(0). Further notation:
∇H(x) is the vector of partial derivatives, XH(x)=j0∇H(x);
the Reeb field is R(x)=λx(XH(x))−1XH(x), with the convention 0−1=0 (so R(x)=0 wherever λx(XH(x))=0);
ξx={v∈R4:λx(v)=0 and dHx(v)=0}.
The structure J (hypothesis "compatible on ξ"). J:R4→EndR(R4) is C∞, and for every x∈S and all v,w∈ξx:
No condition is imposed on Jx outside ξx, nor for x∈/S.
Radial coordinates. For y∈R4 let σ(y) be a (chosen) r>0 with H(ry)=1 if such an r exists, and σ(y)=1 otherwise; for y=0 this r is the unique one from the star-shapedness hypothesis. Put
pr(y)=σ(y)y,a(y)=−21logσ(y).
For y=0, pr(y) is the point of S on the ray through y and y=e2a(y)pr(y); always pr(0)=0.
The Reeb orbit P.P consists of a map xP:R→R4 and a number TP>0 such that xP(τ)∈S, xP′(τ)=R(xP(τ)) and xP(τ+TP)=xP(τ) for all τ. The period TP is not required to be the minimal period. Its image is P=xP(R)⊂R4. A Reeb orbit Q is called prime if xQ(τ)=xQ(0) for all 0<τ<TQ.
The almost complex structure J~ on R4. For y∈R4 let x=pr(y), r=σ(y), and define the linear forms α(v)=2dHx(x)rdHx(v) and β(v)=rλx(v) (division by 0 gives 0). Then
Plane coordinates. For f:C→F and z=s+it, ∂sf(z)=Df(z)1 and ∂tf(z)=Df(z)i, where Df(z) is the real derivative (taken to be 0 where f is not differentiable). For a map u:C→R4 write au=a∘u and wu=pr∘u.
Finite-energy curve on C.u is C∞ on C; u(z)=0 for every z; at every z, u is differentiable and ∂su(z)+J~(u(z))∂tu(z)=0; and E(u)<∞, where
the supremum ranging over all C∞, nondecreasing φ:R→[0,1] (the integral is the Lebesgue integral of the nonnegative part).
Nondegenerate end at infinity at an orbit Q (written NE(u,Q)). With c∞(s,t)=e2πse2πit, there exist d,c∈R and b>0 such that, as s→+∞, uniformly in t∈R,
("Uniformly" means: for every ε>0 there is s0 with the quantity at most ε in absolute value/norm for all s≥s0 and all t.)
The function π∂s. For x∈R4 define e1(x)=∣x∣−1(q2(x)−dHx(x)dHx(q2(x))x) and e2(x)=∣x∣−1(q1(x)−dHx(x)dHx(q1(x))x) with q1(x)=(−x2,x3,x0,−x1), q2(x)=(x3,x2,−x1,−x0) and ∣x∣ the Euclidean norm (again 0−1=0), and the complex coordinate ζx(v)=ω0(v,e2(x))+iω0(e1(x),v)∈C. Then
Winding of a loop. A map f:R→C has winding k∈Z if f is continuous, 1-periodic, nowhere zero, and there is a continuous θ:R→R with f(t)=∣f(t)∣eiθ(t) for all t and θ(1)−θ(0)=2πk.
Fast plane.u:C→R4 is a fast plane if all three hold:
u is a finite-energy curve on C;
there exists some prime Reeb orbit Q (not necessarily equal to P) with NE(u,Q);
the zero set Z={z∈C:π∂su(z)=0} is finite, and there are integers kz (z∈Z) with ∑z∈Zkz=0 such that for each z∈Z there is r>0 with π∂su=0 on the closed disc B(z,r) minus z, and for every ρ∈(0,r) the loop t↦π∂su(z+ρe2πit) has winding kz. (If Z is empty this condition holds automatically.)
Embedded plane.u:C→R4 is called embedded if u is injective and, for every z∈C, the real-linear map Du(z):C≅R2→R4 is injective. (This is a condition on u itself, not on pr∘u.)
Conley–Zehnder bound CZ(P)≥3. This hypothesis says: 3≤μ(γ,Y) for all of the following data:
every γ:R→R4 and Tγ>0 with γ′(t)=XH(γ(t)), H(γ(t))=1 and γ(t+Tγ)=γ(t) for all t (Tγ not necessarily minimal),
such that γ(R)=P and TP=∫0Tγλγ(τ)(γ′(τ))dτ,
and every Y:R→End(R4) with Y(0)=id and Y′(t)=DXH(γ(t))∘Y(t) for all t.
If no such γ exists, the hypothesis holds vacuously. The quantity μ(γ,Y)∈Z is computed from the 2×2 real matrix path
where ζxR2(v)=(ω0(v,e2(x)),ω0(e1(x),v)) and Πxv=v−λx(XH(x))λx(v)XH(x) (division by 0 gives 0). Let W⊂R be the set of numbers (θ(1)−s)/(2π) over all s∈[0,2π] and all θ continuous on [0,1] with θ(0)=s such that for each t∈[0,1], Φ(t)(coss,sins)T is a positive multiple of (cosθ(t),sinθ(t))T. With α=infW, β=supW (both taken to be 0 if W is empty or unbounded on that side),
Confirmed by the moderator at approval.