Prove2Me

Periodic points are dense in Ω(f)\Omega(f) for C1C^1 structurally stable ff

Open
StabilityConjecture.periodic_dense_of_C1_stable

by Lucas · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

differential-topologydynamical-systems

Let MM be a closed manifold: a compact Hausdorff smooth manifold without boundary, modelled on Rn\mathbb R^n. Let f∈Diff1(M)f\in\mathrm{Diff}^1(M) be C1C^1 structurally stable. Then the periodic points of ff are dense in its nonwandering set:

Per(f)‾=Ω(f).\overline{\mathrm{Per}(f)}=\Omega(f).

This is the density half of Axiom A for C1C^1 structurally stable diffeomorphisms; for CrC^r, r≥2r\ge2, the corresponding statement is not known, since no CrC^r closing lemma is available.

Preamble
import Mathlib
import Definitions.Def_ClosingLemma_DiffeoCrTopology
import Definitions.Def_PughClosingLemma_nonwandering
import Definitions.Def_StabilityConjecture_Basic

open scoped Manifold ContDiff Topology
Formal statement
namespace StabilityConjecture

open ClosingLemma

theorem periodic_dense_of_C1_stable {n : ℕ} {M : Type*} [TopologicalSpace M] [T2Space M]
    [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsManifold (𝓡 n) ∞ M]
    (f : Diff n M 1) (hf : IsStructurallyStable 1 f) :
    closure (Function.periodicPts f) = PughClosingLemma.nonwanderingSet f := by sorry

end StabilityConjecture
Source
Consequence of C. Pugh, An improved closing lemma and a general density theorem, Amer. J. Math. 89 (1967) (General Density Theorem), together with the invariance of Per(f) and Omega(f) under topological conjugacy; also contained in R. Mañé, A proof of the C^1 stability conjecture, Publ. Math. IHÉS 66 (1988). Context: Open Problem Garden, "C^r Stability Conjecture" (Conjecture, author(s) J. Palis and S. Smale; posted by m n, December 20th, 2007), https://www.openproblemgarden.org/op/c_r_stability_conjecture
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