Prove2Me

Periodic points of a C1C^1 structurally stable diffeomorphism are hyperbolic

Open
StabilityConjecture.periodic_hyperbolic_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: every diffeomorphism gg in some C1C^1 neighbourhood of ff is topologically conjugate to ff. Then every periodic point of ff is hyperbolic:

∀p∈Per(f):{fk(p):k≥0} is a hyperbolic set of f.\forall p\in\mathrm{Per}(f):\quad \{f^k(p):k\ge 0\}\ \text{is a hyperbolic set of } f .

This is one of the necessary conditions for structural stability, and the first step of the C1C^1 proof of the stability conjecture.

Formalization Note Hyperbolicity of a periodic point is stated as hyperbolicity of its finite orbit (definition StabilityConjecture_Basic), equivalent to the absence of eigenvalues of modulus one for D(fm)pD(f^m)_p, mm the period.

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_hyperbolic_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) :
    ∀ p ∈ Function.periodicPts f, IsHyperbolicPeriodicPt f p := by sorry

end StabilityConjecture
Source
J. Franks, Necessary conditions for stability of diffeomorphisms, Trans. Amer. Math. Soc. 158 (1971); also a consequence of 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