Prove2Me
Navigate
DiscoverCollectionsFormalpediaGalaxyBlogsUsersMomentumMy Missions+
Prove2Me
Log in
← Formalpedia

The Hofer–Wysocki–Zehnder identity windπ=wind∞−χ+#Γ\mathrm{wind}_\pi=\mathrm{wind}_\infty-\chi+\#\Gammawindπ​=wind∞​−χ+#Γ

Proved
FiniteEnergyPlane.windPi_eq_windInf_sub_card

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ξ. Let Γ⊂C\Gamma\subset\mathbb{C}Γ⊂C be finite and uuu a finite-energy J~\tilde JJ~-holomorphic curve on C∖Γ\mathbb{C}\setminus\GammaC∖Γ such that ∞\infty∞ is a positive puncture and every z∈Γz\in\Gammaz∈Γ a negative puncture, all nondegenerate in the sense of Hryniewicz, Definition 2.9, and suppose π du\pi\,duπdu does not vanish identically. Then windπ(u)\mathrm{wind}_\pi(u)windπ​(u), wind∞(u,∞)\mathrm{wind}_\infty(u,\infty)wind∞​(u,∞) and wind∞(u,z)\mathrm{wind}_\infty(u,z)wind∞​(u,z) for z∈Γz\in\Gammaz∈Γ are defined, and

windπ(u)=wind∞(u,∞)−∑z∈Γwind∞(u,z)−χ(S2)+#(Γ∪{∞}).\mathrm{wind}_\pi(u)=\mathrm{wind}_\infty(u,\infty)-\sum_{z\in\Gamma}\mathrm{wind}_\infty(u,z)-\chi(S^2)+\#(\Gamma\cup\{\infty\}).windπ​(u)=wind∞​(u,∞)−z∈Γ∑​wind∞​(u,z)−χ(S2)+#(Γ∪{∞}).

Formalization Note The punctures are IsNondegenerateEnd H u cylInf P∞ 1 and IsNondegenerateEnd H u (cylEndAt z) P_z (-1) for z∈Γz\in\Gammaz∈Γ; "π du≢0\pi\,du\not\equiv0πdu≡0" is ∃ z ∉ Γ, piDs H u z ≠ 0. In Lean the right-hand side is kinf - ∑ z ∈ Γ, kz z - 2 + (Γ.card + 1).

Preamble
import Definitions.Def_FiniteEnergyPlane_Winding
Formal statement
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
Source
U. Hryniewicz, Systems of global surfaces of section for dynamically convex Reeb flows on the 3-sphere, J. Symplectic Geom. 12 (2014), arXiv:1105.2077, Lemma 2.15; U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. Amer. Math. Soc. 364 (2012), 1859–1931, arXiv:0812.4076, Lemma 3.19; H. Hofer, K. Wysocki, E. Zehnder, Properties of pseudoholomorphic curves in symplectisations II: Embedding controls and algebraic invariants, Geom. Funct. Anal. 5 (1995), 270–328
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: H:R4→RH:\mathbb{R}^4\to\mathbb{R}H:R4→R has a strictly star-shaped level; JJJ is a compatible ξ\xiξ-structure for HHH; Γ⊂C\Gamma\subset\mathbb{C}Γ⊂C is a finite set (possibly empty); u:C→R4u:\mathbb{C}\to\mathbb{R}^4u:C→R4 is a finite-energy curve on C∖Γ\mathbb{C}\setminus\GammaC∖Γ; P∞P_\inftyP∞​ is a Reeb orbit with NdEnd(u,cyl∞,P∞,+1)\mathrm{NdEnd}(u, \mathrm{cyl}_\infty, P_\infty, +1)NdEnd(u,cyl∞​,P∞​,+1); for every z∈Γz\in\Gammaz∈Γ some Reeb orbit PzP_zPz​ satisfies NdEnd(u,cylz,Pz,−1)\mathrm{NdEnd}(u, \mathrm{cyl}_z, P_z, -1)NdEnd(u,cylz​,Pz​,−1); and there is z∉Γz\notin\Gammaz∈/Γ with Π(z)≠0\Pi(z)\neq0Π(z)=0, where

Π(z)=Ξw(z)(πξ(w(z)) ∂sw(z))∈C,w=pr∘u.\Pi(z) = \Xi_{w(z)}\big(\pi_\xi(w(z))\,\partial_s w(z)\big)\in\mathbb{C},\qquad w = \mathrm{pr}\circ u.Π(z)=Ξw(z)​(πξ​(w(z))∂s​w(z))∈C,w=pr∘u.

Conclusion. There exist integers k∞k_\inftyk∞​, kπk_\pikπ​ and a function k:C→Zk:\mathbb{C}\to\mathbb{Z}k:C→Z such that

  1. wind∞(u,cyl∞,+1)=k∞\mathrm{wind}_\infty(u, \mathrm{cyl}_\infty, +1) = k_\inftywind∞​(u,cyl∞​,+1)=k∞​;
  2. for every z∈Γz\in\Gammaz∈Γ: wind∞(u,cylz,−1)=k(z)\mathrm{wind}_\infty(u, \mathrm{cyl}_z, -1) = k(z)wind∞​(u,cylz​,−1)=k(z);
  3. windπ(u,Γ)=kπ\mathrm{wind}_\pi(u,\Gamma) = k_\piwindπ​(u,Γ)=kπ​;
  4. the integer identity
kπ=k∞−∑z∈Γk(z)−2+(#Γ+1)k_\pi = k_\infty - \sum_{z\in\Gamma} k(z) - 2 + (\#\Gamma + 1)kπ​=k∞​−z∈Γ∑​k(z)−2+(#Γ+1)

holds (equivalently kπ=k∞−∑z∈Γk(z)+#Γ−1k_\pi = k_\infty - \sum_{z\in\Gamma}k(z) + \#\Gamma - 1kπ​=k∞​−∑z∈Γ​k(z)+#Γ−1), where #Γ\#\Gamma#Γ is the number of points of Γ\GammaΓ.

Here:

  • "wind∞(u,e,ε)=k\mathrm{wind}_\infty(u, e, \varepsilon) = kwind∞​(u,e,ε)=k" means: there is s0s_0s0​ such that for every s≥s0s\ge s_0s≥s0​ the loop
t↦ΞWe(s,εt)(πξ(We(s,εt)) ∂sWe(s,εt))t\mapsto \Xi_{W_e(s,\varepsilon t)}\Big(\pi_\xi\big(W_e(s,\varepsilon t)\big)\,\partial_s W_e(s,\varepsilon t)\Big)t↦ΞWe​(s,εt)​(πξ​(We​(s,εt))∂s​We​(s,εt))

has wind=k\mathrm{wind} = kwind=k, where ∂sWe(s,t′)\partial_s W_e(s,t')∂s​We​(s,t′) is the derivative of (s,t)↦We(s,t)(s,t)\mapsto W_e(s,t)(s,t)↦We​(s,t) at (s,t′)(s,t')(s,t′) in the direction (1,0)(1,0)(1,0). For ε=−1\varepsilon = -1ε=−1 the loop is traversed with ttt reversed.

  • "z0z_0z0​ is a zero of fff of index mmm" means: f(z0)=0f(z_0)=0f(z0​)=0, there is r>0r>0r>0 with f(z)≠0f(z)\neq0f(z)=0 for 0<∣z−z0∣≤r0<|z-z_0|\le r0<∣z−z0​∣≤r, and for every ρ∈(0,r)\rho\in(0,r)ρ∈(0,r) the loop t↦f(z0+ρe2πit)t\mapsto f(z_0+\rho e^{2\pi it})t↦f(z0​+ρe2πit) has wind=m\mathrm{wind}=mwind=m.
  • "windπ(u,Γ)=k\mathrm{wind}_\pi(u,\Gamma) = kwindπ​(u,Γ)=k" means: there is a finite set ZZZ with z∈Z  ⟺  (z∉Γz\in Z\iff(z\notin\Gammaz∈Z⟺(z∈/Γ and Π(z)=0)\Pi(z)=0)Π(z)=0), and a function idx:C→Z\mathrm{idx}:\mathbb{C}\to\mathbb{Z}idx:C→Z such that each z∈Zz\in Zz∈Z is a zero of Π\PiΠ of index idx(z)\mathrm{idx}(z)idx(z) and ∑z∈Zidx(z)=k\sum_{z\in Z}\mathrm{idx}(z) = k∑z∈Z​idx(z)=k.

The values k(z)k(z)k(z) for z∉Γz\notin\Gammaz∈/Γ are irrelevant. The orbits P∞P_\inftyP∞​, PzP_zPz​ are not required to be prime or distinct.

Meaning of the notions used

Throughout, the ambient space is R4\mathbb{R}^4R4 with coordinates (y0,y1,y2,y3)(y_0,y_1,y_2,y_3)(y0​,y1​,y2​,y3​) (the code's space of functions on a 4-element index set), and C\mathbb{C}C is identified with R2\mathbb{R}^2R2 via z=s+itz = s + itz=s+it.

Linear algebra. j0(v)=(−v1,v0,−v3,v2)j_0(v) = (-v_1, v_0, -v_3, v_2)j0​(v)=(−v1​,v0​,−v3​,v2​) and

ω0(u,v)=u0v1−u1v0+u2v3−u3v2,λx(v)=12 ω0(x,v).\omega_0(u,v) = u_0v_1 - u_1v_0 + u_2v_3 - u_3v_2, \qquad \lambda_x(v) = \tfrac12\,\omega_0(x,v).ω0​(u,v)=u0​v1​−u1​v0​+u2​v3​−u3​v2​,λx​(v)=21​ω0​(x,v).

Star-shaped level. "HHH has a strictly star-shaped level" means: H:R4→RH:\mathbb{R}^4\to\mathbb{R}H:R4→R 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 at every xxx with H(x)=1H(x)=1H(x)=1. Write S={H=1}S = \{H = 1\}S={H=1}.

Reeb field and contact plane. XH(x)=j0(∇H(x))X_H(x) = j_0(\nabla H(x))XH​(x)=j0​(∇H(x)), and 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) (with the convention 0−1=00^{-1} = 00−1=0). The plane ξx\xi_xξx​ is {v:λx(v)=0 and dHx(v)=0}\{v : \lambda_x(v) = 0 \text{ and } dH_x(v) = 0\}{v:λx​(v)=0 and dHx​(v)=0} (defined for every xxx, not only on SSS). The projection πξ\pi_\xiπξ​ 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).

Compatible JJJ. "JJJ is a compatible ξ\xiξ-structure for HHH" means: J:R4→L(R4,R4)J:\mathbb{R}^4\to \mathrm{L}(\mathbb{R}^4,\mathbb{R}^4)J:R4→L(R4,R4) is C∞C^\inftyC∞, and for every x∈Sx\in Sx∈S and all 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\neq 0v=0, and ω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 of J(x)J(x)J(x) off ξx\xi_xξx​ or off SSS.

Radial projection. For y∈R4y\in\mathbb{R}^4y∈R4 let σ(y)\sigma(y)σ(y) be the unique r>0r>0r>0 with H(ry)=1H(ry)=1H(ry)=1 if such rrr exists, and σ(y)=1\sigma(y)=1σ(y)=1 otherwise (in particular σ(0)=1\sigma(0)=1σ(0)=1). Then pr(y)=σ(y) y\mathrm{pr}(y) = \sigma(y)\,ypr(y)=σ(y)y and a(y)=−12log⁡σ(y)a(y) = -\tfrac12\log\sigma(y)a(y)=−21​logσ(y).

Almost complex structure J~\tilde JJ~. For y∈R4y\in\mathbb{R}^4y∈R4 put x=pr(y)x = \mathrm{pr}(y)x=pr(y), r=σ(y)r=\sigma(y)r=σ(y), α(v)=r2 dHx(x) dHx(v)\alpha(v) = \frac{r}{2\,dH_x(x)}\,dH_x(v)α(v)=2dHx​(x)r​dHx​(v), β(v)=r λx(v)\beta(v) = r\,\lambda_x(v)β(v)=rλx​(v), w(v)=v−2α(v) y−β(v) r−1R(x)w(v) = v - 2\alpha(v)\,y - \beta(v)\,r^{-1}R(x)w(v)=v−2α(v)y−β(v)r−1R(x), and

J~(y)v=α(v) r−1R(x)−2β(v) y+J(x) w(v).\tilde J(y)v = \alpha(v)\,r^{-1}R(x) - 2\beta(v)\,y + J(x)\,w(v).J~(y)v=α(v)r−1R(x)−2β(v)y+J(x)w(v).

Finite-energy curve. For U⊆CU\subseteq\mathbb{C}U⊆C, "uuu is a finite-energy curve on UUU" means: u:C→R4u:\mathbb{C}\to\mathbb{R}^4u:C→R4 is C∞C^\inftyC∞ on UUU; u(z)≠0u(z)\neq 0u(z)=0 for z∈Uz\in Uz∈U; at every z∈Uz\in Uz∈U, uuu is (real-)differentiable and ∂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

E(u)=sup⁡φ∫Umax⁡(0, φ′(a)(∂sa λw(∂tw)−∂ta λw(∂sw))+φ(a) ω0(∂sw,∂tw)) dz<∞,E(u) = \sup_{\varphi}\int_U \max\Big(0,\ \varphi'(a)\big(\partial_s a\,\lambda_w(\partial_t w) - \partial_t a\,\lambda_w(\partial_s w)\big) + \varphi(a)\,\omega_0(\partial_s w,\partial_t w)\Big)\,dz < \infty,E(u)=φsup​∫U​max(0, φ′(a)(∂s​aλw​(∂t​w)−∂t​aλw​(∂s​w))+φ(a)ω0​(∂s​w,∂t​w))dz<∞,

where a=a∘ua = a\circ ua=a∘u, w=pr∘uw = \mathrm{pr}\circ uw=pr∘u, and φ\varphiφ ranges over C∞C^\inftyC∞ nondecreasing functions R→[0,1]\mathbb{R}\to[0,1]R→[0,1]. Values of uuu outside UUU are unconstrained. Derivatives here and below are Fréchet derivatives, with the convention that the derivative at a point of non-differentiability is 000.

Reeb orbit. A Reeb orbit PPP of HHH is a pair (x,T)(x,T)(x,T) with T>0T>0T>0 and x:R→R4x:\mathbb{R}\to\mathbb{R}^4x:R→R4 such that H(x(τ))=1H(x(\tau)) = 1H(x(τ))=1, 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τ. TTT is any positive period (not necessarily the minimal one).

End parametrizations. cyl∞(s,t)=e2πse2πit\mathrm{cyl}_\infty(s,t) = e^{2\pi s}e^{2\pi i t}cyl∞​(s,t)=e2πse2πit (large circles, counterclockwise in ttt), and for z0∈Cz_0\in\mathbb{C}z0​∈C, cylz0(s,t)=z0+e−2πse−2πit\mathrm{cyl}_{z_0}(s,t) = z_0 + e^{-2\pi s}e^{-2\pi i t}cylz0​​(s,t)=z0​+e−2πse−2πit (small circles around z0z_0z0​, clockwise in ttt). For such a map eee write We(s,t)=pr(u(e(s,t)))W_e(s,t) = \mathrm{pr}(u(e(s,t)))We​(s,t)=pr(u(e(s,t))) and Ae(s,t)=a(u(e(s,t)))A_e(s,t) = a(u(e(s,t)))Ae​(s,t)=a(u(e(s,t))). Note that only large sss enters the conditions below; for small sss these maps may leave the region where uuu is constrained.

"Nondegenerate end". For ε∈R\varepsilon\in\mathbb{R}ε∈R, NdEnd(u,e,P,ε)\mathrm{NdEnd}(u, e, P, \varepsilon)NdEnd(u,e,P,ε) means: there are d,c∈Rd, c\in\mathbb{R}d,c∈R and b>0b>0b>0 such that, uniformly in t∈Rt\in\mathbb{R}t∈R, as s→+∞s\to+\inftys→+∞,

Ae(s,t)−εTs−d→0,ebs ∣We(s,t)−x(εTt+c)∣→0.A_e(s,t) - \varepsilon T s - d \to 0, \qquad e^{bs}\,\big|W_e(s,t) - x(\varepsilon T t + c)\big| \to 0.Ae​(s,t)−εTs−d→0,ebs​We​(s,t)−x(εTt+c)​→0.

(This is an exponential convergence condition on uuu along the end; it contains no hypothesis on the linearized Reeb flow of PPP.)

ξ\xiξ-coordinates. For x,v∈R4x, v\in\mathbb{R}^4x,v∈R4, with ∣x∣|x|∣x∣ the Euclidean norm, define Q1x=(−x2,x3,x0,−x1)Q_1x = (-x_2, x_3, x_0, -x_1)Q1​x=(−x2​,x3​,x0​,−x1​), Q2x=(x3,x2,−x1,−x0)Q_2x = (x_3, x_2, -x_1, -x_0)Q2​x=(x3​,x2​,−x1​,−x0​),

ei(x)=∣x∣−1(Qix−dHx(Qix)dHx(x) x)(i=1,2),e_i(x) = |x|^{-1}\Big(Q_ix - \frac{dH_x(Q_ix)}{dH_x(x)}\,x\Big)\quad(i=1,2),ei​(x)=∣x∣−1(Qi​x−dHx​(x)dHx​(Qi​x)​x)(i=1,2),

(with 0−1=00^{-1}=00−1=0 and division by 000 giving 000), and

Ξx(v)=ω0(v,e2(x))+i ω0(e1(x),v) ∈C.\Xi_x(v) = \omega_0(v, e_2(x)) + i\,\omega_0(e_1(x), v)\ \in\mathbb{C}.Ξx​(v)=ω0​(v,e2​(x))+iω0​(e1​(x),v) ∈C.

Winding of a loop. For f:R→Cf:\mathbb{R}\to\mathbb{C}f:R→C and k∈Zk\in\mathbb{Z}k∈Z, wind(f)=k\mathrm{wind}(f) = kwind(f)=k means: fff is continuous, 111-periodic, never 000, and 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 and θ(1)−θ(0)=2πk\theta(1) - \theta(0) = 2\pi kθ(1)−θ(0)=2πk.

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