The Hofer–Wysocki–Zehnder identity
ProvedFiniteEnergyPlane.windPi_eq_windInf_sub_cardLet be a strictly star-shaped level and a smooth -compatible complex structure on . Let be finite and a finite-energy -holomorphic curve on such that is a positive puncture and every a negative puncture, all nondegenerate in the sense of Hryniewicz, Definition 2.9, and suppose does not vanish identically. Then , and for are defined, and
Formalization Note The punctures are IsNondegenerateEnd H u cylInf P∞ 1 and IsNondegenerateEnd H u (cylEndAt z) P_z (-1) for ; "" is ∃ z ∉ Γ, piDs H u z ≠ 0. In Lean the right-hand side is kinf - ∑ z ∈ Γ, kz z - 2 + (Γ.card + 1).
import Definitions.Def_FiniteEnergyPlane_Winding
namespace FiniteEnergyPlane
open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real
/-- Hofer–Wysocki–Zehnder: Hryniewicz, Lemma 2.15 (Hryniewicz, Trans. AMS 2012, Lemma 3.19), for
`S = ℂ ∪ {∞}`. Let `u` be a finite-energy `J̃`-holomorphic curve on `ℂ \ Γ`, `Γ` finite, with a
positive puncture at `∞`, negative punctures at the points of `Γ`, all nondegenerate in the sense of
Definition 2.9, and with `π du` not identically zero. Then `wind_π(u)` and the asymptotic windings
are defined, and `wind_π(u) = wind_∞(u, ∞) - Σ_{z ∈ Γ} wind_∞(u, z) - χ(S²) + #(Γ ∪ {∞})`. -/
theorem windPi_eq_windInf_sub_card (H : V 1 → ℝ) (hH : IsStrictlyStarShapedLevel H)
(J : V 1 → V 1 →L[ℝ] V 1) (hJ : IsCompatibleXiStructure H J)
(Γ : Finset ℂ) (u : ℂ → V 1)
(hu : IsFiniteEnergyCurve H J (↑Γ)ᶜ u) (Pinf : ReebOrbit H)
(hinf : IsNondegenerateEnd H u cylInf Pinf 1)
(hΓ : ∀ z ∈ Γ, ∃ Pz : ReebOrbit H, IsNondegenerateEnd H u (cylEndAt z) Pz (-1))
(hne : ∃ z ∉ Γ, piDs H u z ≠ 0) :
∃ (kinf : ℤ) (kz : ℂ → ℤ) (kπ : ℤ), HasWindInfAt H u cylInf 1 kinf ∧
(∀ z ∈ Γ, HasWindInfAt H u (cylEndAt z) (-1) (kz z)) ∧ HasWindPi H u Γ kπ ∧
kπ = kinf - ∑ z ∈ Γ, kz z - 2 + (Γ.card + 1) := by
sorry
end FiniteEnergyPlane
Read-back
What the Lean code literally says, in plain math · claude-opus-5-5
FiniteEnergyPlane.windPi_eq_windInf_sub_card
Data and hypotheses. Exactly the same as in exists_hasWindPi_of_nondegenerate: has a strictly star-shaped level; is a compatible -structure for ; is a finite set (possibly empty); is a finite-energy curve on ; is a Reeb orbit with ; for every some Reeb orbit satisfies ; and there is with , where
Conclusion. There exist integers , and a function such that
- ;
- for every : ;
- ;
- the integer identity
holds (equivalently ), where is the number of points of .
Here:
- "" means: there is such that for every the loop
has , where is the derivative of at in the direction . For the loop is traversed with reversed.
- " is a zero of of index " means: , there is with for , and for every the loop has .
- "" means: there is a finite set with and , and a function such that each is a zero of of index and .
The values for are irrelevant. The orbits , are not required to be prime or distinct.
Meaning of the notions used
Throughout, the ambient space is with coordinates (the code's space of functions on a 4-element index set), and is identified with via .
Linear algebra. and
Star-shaped level. " has a strictly star-shaped level" means: is ; for every there is exactly one with ; and at every with . Write .
Reeb field and contact plane. , and (with the convention ). The plane is (defined for every , not only on ). The projection is .
Compatible . " is a compatible -structure for " means: is , and for every and all : , , if , and . Nothing is required of off or off .
Radial projection. For let be the unique with if such exists, and otherwise (in particular ). Then and .
Almost complex structure . For put , , , , , and
Finite-energy curve. For , " is a finite-energy curve on " means: is on ; for ; at every , is (real-)differentiable and ; and
where , , and ranges over nondecreasing functions . Values of outside are unconstrained. Derivatives here and below are Fréchet derivatives, with the convention that the derivative at a point of non-differentiability is .
Reeb orbit. A Reeb orbit of is a pair with and such that , and for all . is any positive period (not necessarily the minimal one).
End parametrizations. (large circles, counterclockwise in ), and for , (small circles around , clockwise in ). For such a map write and . Note that only large enters the conditions below; for small these maps may leave the region where is constrained.
"Nondegenerate end". For , means: there are and such that, uniformly in , as ,
(This is an exponential convergence condition on along the end; it contains no hypothesis on the linearized Reeb flow of .)
-coordinates. For , with the Euclidean norm, define , ,
(with and division by giving ), and
Winding of a loop. For and , means: is continuous, -periodic, never , and there is a continuous with for all and .
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.