Prove2Me

Existence and uniqueness of the flow of a CrC^r vector field on a compact manifold

Proved
PalisConjecture.exists_unique_flow

by Lucas · Oct 11, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

attractorsdynamical-systems

Let MM be a compact Hausdorff boundaryless smooth manifold modelled on Rn\mathbb R^n, let r≥1r\ge1, and let XX be a CrC^r vector field on MM. Then there is exactly one map Φ:R×M→M\Phi:\mathbb R\times M\to M such that, for every p∈Mp\in M, Φ0(p)=p\Phi_0(p)=p and

ddtΦt(p)=X(Φt(p))for all t∈R.\frac{d}{dt}\Phi_t(p)=X\big(\Phi_t(p)\big)\quad\text{for all } t\in\mathbb R.

Vector fields on compact boundaryless manifolds are complete. This guarantees that the flow statements of the mission, which quantify over all flows of XX, are about the actual flow of XX and are not vacuous.

Preamble
import Mathlib
import Definitions.Def_palis_lebesgue_null
import Definitions.Def_palis_attractor
import Definitions.Def_palis_vector_field
import Definitions.Def_palis_cr_topology

open scoped Manifold ContDiff
Formal statement
namespace PalisConjecture

theorem exists_unique_flow (n : ℕ) {M : Type*} [TopologicalSpace M] [T2Space M]
    [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsManifold (𝓡 n) ∞ M]
    (r : ℕ) (hr : 1 ≤ r) (X : (x : M) → TangentSpace (𝓡 n) x)
    (hX : IsCrVectorField r X) :
    ∃! Φ : ℝ → M → M, IsFlowOf X Φ := by
  sorry

end PalisConjecture
Source
Open Problem Garden, "Jacob Palis Conjecture (Finitude of Attractors) (Dynamical Systems)", posted by Jailton Viana, April 24, 2013, https://www.openproblemgarden.org/op/jacob_palis_conjecture_finitude_of_attractors_dynamical_systems (Conjecture box and the Definition of attractor below it); bibliography: C. Bonatti, L. J. Diaz, M. Viana, Dynamics Beyond Uniform Hyperbolicity, Encyclopaedia of Mathematical Sciences 102, Springer, 2005.
Human review

  • Endorsed by Shuze Chen · Oct 11, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 11, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph