Weinstein conjecture in dimension three (Taubes 2007)

weinstein_conjecture_dim3

Submitter: Kim Morrison.

Notes: Every Reeb vector field of a contact form on a closed smooth 3-manifold has a closed periodic orbit. Mathlib lacks contact-geometry API and a manifold exterior derivative, so the encoding fixes dα by the intrinsic coordinate-free identity dα(X, Y) = X(α(Y)) − Y(α(X)) − α([X, Y]) (which uniquely determines dα from α via mathlib's mfderiv + VectorField.mlieBracket), and uses the equivalent dimension-3 contact condition `α ≠ 0 ∧ dα nondegenerate on ker α` in place of `α ∧ dα ≠ 0`. [I.Boundaryless] is essential: on the cube [0,1]³ with α = dz + x·dy, every Reeb integral curve has affine z-component with |z'| = 1 and escapes the cube, so closed orbits do not exist without the boundaryless hypothesis. §141 of Knill's *Some Fundamental Theorems in Mathematics*.

Source: C.H. Taubes, 'The Seiberg–Witten equations and the Weinstein conjecture', Geom. Topol. 11 (2007) 2117–2202; arXiv:math/0611007. Conjecture: A. Weinstein, 'On the hypotheses of Rabinowitz' periodic orbit theorems', J. Differential Equations 33 (1979) 353–358. §141 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Taubes proves the three-dimensional Weinstein conjecture using Seiberg–Witten theory, relating large-parameter solutions of the Seiberg–Witten equations on Y × ℝ associated to a contact form to Reeb dynamics. If a closed contact 3-manifold had no closed Reeb orbit, the large-`r` analysis of the deformed Seiberg–Witten equations would contradict the nonvanishing input from Seiberg–Witten Floer homology / embedded contact homology in the relevant Spin^c structure. Mathlib has the smooth-manifold infrastructure used to state the problem (smooth manifolds, tangent spaces, mfderiv, Lie brackets) but not the contact-geometry, Reeb-dynamics, Seiberg–Witten, or embedded-contact-homology machinery needed to prove it.

theorem declaration uses `sorry`weinstein_conjecture_dim_three (E' : Type*) [NormedAddCommGroup E'] [NormedSpace ℝ E']
    [FiniteDimensional ℝ E']
    (H' : Type*) [TopologicalSpace H']
    (I' : ModelWithCorners ℝ E' H')
    (M' : Type*) [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' ∞ M']
    [T2Space M'] [CompactSpace M'] [Nonempty M'] [Fact (Module.finrank ℝ E' = 3)]
    [I'.Boundaryless]
    (α : LeanEval.Geometry.WeinsteinConjecture3DProblem.OneForm I' (M := M')) (dα : LeanEval.Geometry.WeinsteinConjecture3DProblem.TwoForm I' (M := M'))
    (R : ∀ x : M', TangentSpace I' x)
    (_hcontact : LeanEval.Geometry.WeinsteinConjecture3DProblem.IsContactForm3 I' α dα)
    (_hReeb : LeanEval.Geometry.WeinsteinConjecture3DProblem.IsReebVectorField I' α dα R) :
    LeanEval.Geometry.WeinsteinConjecture3DProblem.HasClosedReebOrbit I' R := byE':Type u_4inst✝¹¹:NormedAddCommGroup E'inst✝¹⁰:NormedSpace ℝ E'inst✝⁹:FiniteDimensional ℝ E'H':Type u_5inst✝⁸:TopologicalSpace H'I':ModelWithCorners ℝ E' H'M':Type u_6inst✝⁷:TopologicalSpace M'inst✝⁶:ChartedSpace H' M'inst✝⁵:IsManifold I' ∞ M'inst✝⁴:T2Space M'inst✝³:CompactSpace M'inst✝²:Nonempty M'inst✝¹:Fact (Module.finrank ℝ E' = 3)inst✝:I'.Boundarylessα:OneForm I'dα:TwoForm I'R:(x : M') → TangentSpace I' x_hcontact:IsContactForm3 I' α dα_hReeb:IsReebVectorField I' α dα R⊢ HasClosedReebOrbit I' R
  sorryAll goals completed! 🐙

Solved by

Not yet solved.