The identity map has no attractors

Proved

PalisConjecture.identity_not_finitely_many_attractors

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

attractorsdynamical-systems

Let $M$ be a nonempty Hausdorff manifold modelled on $\mathbb R^n$ with $n\ge1$ . The identity map $\mathrm{id}_M$ does not have finitely many attractors whose basins cover Lebesgue-almost all of $M$ .

This shows that the property in the Palis conjecture is not satisfied by every diffeomorphism, so the density requirement has content. Each transitive invariant set of the identity is a single point. Its basin is that point, which is Lebesgue-null when $n\ge1$ . So there are no attractors, and $M$ itself is not null.

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 identity_not_finitely_many_attractors (n : ℕ) (hn : 1 ≤ n) {M : Type*}
    [TopologicalSpace M] [T2Space M] [Nonempty M]
    [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] :
    ¬ HasFiniteAttractorsCoveringAE n (id : M → M) := 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