Finite-energy curves with vanishing -energy and negative punctures are trivial cylinders composed with polynomials
ProvedFiniteEnergyPlane.eq_trivialCylinder_comp_polynomialLet be a strictly star-shaped level, a smooth -compatible complex structure on , finite, and a nonconstant finite-energy -holomorphic curve on such that as for every . If , then there are a polynomial of degree with zero set exactly and a periodic Reeb orbit such that on .
Formalization Note Hryniewicz writes in ; in the coordinate this is trivialCylinder P, . "Nonconstant" is an explicit hypothesis; Hryniewicz's finite-energy surfaces are nonconstant by convention. The punctures are approached along 𝓝[≠] z₀.
import Definitions.Def_FiniteEnergyPlane_Setting
namespace FiniteEnergyPlane
open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real
/-- Hofer–Wysocki–Zehnder: Hryniewicz 2014, Theorem 2.18. Let `Γ ⊆ ℂ` be finite and `u` a
nonconstant finite-energy `J̃`-holomorphic curve on `ℂ \ Γ` all of whose punctures in `Γ` are
negative (`a → -∞`). If its `dλ`-energy vanishes, there are a nonconstant polynomial `p` with zero
set `Γ` and a periodic Reeb orbit `P` such that `u = F_P ∘ p` on `ℂ \ Γ`, where `F_P` is the trivial
cylinder over `P`. (Hryniewicz's `F_P(e^{2π(s+it)}) = (Ts, x(Tt))` reads `F_P(w) = |w|^{T/π} x(T arg w / 2π)`
in the coordinate `y = e^{2a} x`. "Nonconstant" is explicit here; it is implicit in his
"finite-energy surface".) -/
theorem eq_trivialCylinder_comp_polynomial {n : ℕ} (H : V n → ℝ) (hH : IsStrictlyStarShapedLevel H)
(J : V n → V n →L[ℝ] V n) (hJ : IsCompatibleXiStructure H J) (Γ : Finset ℂ) (u : ℂ → V n)
(hu : IsFiniteEnergyCurve H J (↑Γ)ᶜ u)
(hnc : ∃ z₁ ∉ Γ, ∃ z₂ ∉ Γ, u z₁ ≠ u z₂)
(hneg : ∀ z₀ ∈ Γ, Tendsto (fun z => aCoord H (u z)) (𝓝[≠] z₀) atBot)
(hzero : dlambdaEnergy H (↑Γ)ᶜ u = 0) :
∃ p : Polynomial ℂ, 0 < p.natDegree ∧ {z | p.eval z = 0} = ↑Γ ∧
∃ P : ReebOrbit H, ∀ z ∉ Γ, u z = trivialCylinder P (p.eval z) := by
sorry
end FiniteEnergyPlane
Read-back
What the Lean code literally says, in plain math · claude-opus-5-5
FiniteEnergyPlane.eq_trivialCylinder_comp_polynomial
Statement. Let , satisfying the star-shaped level conditions, and a compatible structure (both defined below). Let be a finite set (possibly empty) and a map such that:
- is a finite-energy curve on (as defined below, with respect to and );
- is non-constant on : there are with ;
- for every , as with ;
- .
Then there exist a complex polynomial of degree whose zero set is exactly (no condition on the multiplicities of the zeros), and a Reeb orbit (with no condition on its period ), such that
Nothing is asserted about the values for .
Edge cases. Hypothesis 3 only involves values of at points of near (since is finite). When , hypothesis 3 is vacuous, and the conclusion requires a polynomial of positive degree with no complex zero, which does not exist; so for the statement asserts that hypotheses 1, 2 and 4 cannot hold simultaneously on all of .
Setting and notation (all definitions unfolded)
Throughout, is arbitrary (including ) and , with coordinates indexed .
- Standard structure. is for even and for odd. With the Euclidean dot product , set and .
- Hamiltonian data. For : is the vector of partial derivatives ; ; ; the "Reeb field" is , where the inverse of is taken to be . Derivatives are Fréchet derivatives, with the convention that the derivative of a non-differentiable map at a point is .
- Star-shaped level (hypothesis ): is ; for every there is a unique with ; and for every with .
- Compatible structure (hypothesis ): is , and for every and all in : , , if , and . Nothing is required of off or for .
- Radial coordinates. is a chosen with if one exists, and otherwise (under , for it is the unique such ). Then and , so when is that .
- Almost complex structure . For put , , , , , and
- Derivatives of maps on . , (each where is not differentiable).
- Finite-energy curve on for : (1) is on ; (2) for ; (3) for every , is differentiable at and ; (4) , where, writing and ,
the supremum being over nondecreasing , , and the integral a Lebesgue integral of a nonnegative function with respect to area measure (value in ).
- -energy. .
- Reeb orbits. A Reeb orbit consists of a map and a number such that for all , is differentiable with , and for all . ( is a period, not required to be the minimal one.)
- Trivial cylinder over . For ,
with the principal argument (); since , .
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.