Pugh's closing lemma

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements of this proposal, with full knowledge of the source and of the intended meaning. It is not a blind audit and must not be mistaken for independent testimony; reviewers should check the Lean code against the source themselves or obtain a blind read-back from an independent auditor.

$d\ge 0$ is a natural number and $M$ is a topological space that is Hausdorff and compact, equipped with a charted-space structure with model space $\mathbb R^d$ (Euclidean space $\mathbb R^{\mathrm{Fin}\,d}$, so no boundary) whose transition maps are $C^\infty$ (a $C^\infty$ manifold for the model with corners $\mathbb R^d$ with trivial corners). $M$ may be empty, and $d=0$ is allowed. Here $\mathrm{Diff}^1(M)$ (the type BCWCentralizer.Diff1 d M from the referenced definition file BCWCentralizer_Basic) is the set of $C^1$ diffeomorphisms $g\colon M\to M$ (bijections such that $g$ and $g^{-1}$ are $C^1$ with respect to the manifold structure). The topology used on $\mathrm{Diff}^1(M)$ is BCWCentralizer.c1Topology: the coarsest topology for which the map $g\mapsto Tg$ is continuous, where $Tg\colon TM\to TM$ is the tangent map of $g$ and the space of continuous self-maps $C(TM,TM)$ carries the compact-open topology (uniform convergence on compact subsets of the tangent bundle $TM$). A point $x$ is nonwandering for a map $h\colon X\to X$ (PughClosingLemma.IsNonwandering h x) if for every neighbourhood $U$ of $x$ there is a natural number $n\ge 1$ with $h^n(U)\cap U\neq\emptyset$, where $h^n$ is the $n$-fold composite. The nonwandering set $\Omega(h)$ (PughClosingLemma.nonwanderingSet h) is the set of all such $x$. $\mathrm{Per}(g)$ (Mathlib's Function.periodicPts g) is the set of points $y$ for which there exists $n\ge 1$ with $g^n(y)=y$ (period $0$ is excluded).

Statement. For every such $d$ and $M$, every $f\in\mathrm{Diff}^1(M)$ and every point $x\in M$ that is nonwandering for (the underlying map of) $f$: for every set $\mathcal U\subseteq\mathrm{Diff}^1(M)$ that is a neighbourhood of $f$ in the topology described above, there exists $g\in\mathcal U$ such that $x\in\mathrm{Per}(g)$, i.e.

Notes on the literal content: $g$ is only required to be a $C^1$ diffeomorphism (not $C^\infty$); $f$ is itself only $C^1$; the period $n$ is not bounded; $M$ being empty makes the statement vacuous for that $M$ but non-empty manifolds are included. Closeness of $g$ to $f$ is expressed only through the compact-open topology on tangent maps (which also controls $C^0$-closeness, via the zero section).