Finite Complete Names and Initial-Point Tracing
Abstract
Finitely many complete names for every finite continuous observation yield an actual finite open control cover and tracing by the initial point.
Theorem 1.1 (Constructing the control cover).
Proof. Machine-checked in Lean as D5/S1/Dynamics/Shadowing/FiniteObservationShadowing.initial_point_tracing_of_finite_observation_names (✓ std3). ∎
Source. Repository-derived.
Acknowledgement. Dekui Peng (2026). Shadowing in Dynamical Systems: Zero-dimensional Extensions and Inverse Limits. URL: https://arxiv.org/abs/2606.14435v3.
Commentary.
Let X be compact Hausdorff and zero-dimensional, with continuous f:X→X. Assume that for each natural m and each continuous q:X→Fin m, the exact range of complete names x↦(n↦q(f^n(x))) is finite. For every finite open cover C, there is a finite open cover D such that every D-pseudo-orbit a is C-shadowed by a(0), simultaneously at all natural times including zero. IsOpenCover in the formula is applied to U↦U.val with U ranging over the indicated finset. PseudoOrbit and Shadows are the existing finite-open-cover contracts. The compact Hausdorff totally disconnected hypothesis supplies a clopen basis. There is no metric, countability, nonempty, surjectivity or invertibility assumption.
Refine C by a finite disjoint clopen partition W indexed by Fin m, using Mathlib’s IsOpenCover.exists_finite_nonempty_disjoint_clopen_cover. The unique cell containing x defines q(x); each cell is open, so q is locally constant and continuous. The existing continuous_observationName theorem makes the complete-name map continuous. Its range S is finite by hypothesis and Hausdorff as a subspace of the product of discrete alphabets; hence S is discrete. The inverse images of singleton names are open and form the finite cover D. This constructs D from the observations.
A D-controlled error pair f(a(n)),a(n+1) lies in one complete-name fiber, so their names are equal. The name of f(x) is the left shift of the name of x. Induction therefore identifies the complete names of a(n) and f^n(a(0)). At coordinate zero these points have the same partition label. Their common clopen cell lies inside one member of C, proving tracing. The proof includes empty sources and empty name images without choosing an initial point unless a pseudo-orbit is already supplied.
The theorem above converts finite complete observations into finite-cover tracing. For an application constructing a shadowing extension, let X be any compact Hausdorff space, f:X→X continuous, and K=⋂_{n∈ℕ}f^n(X), including n=0. Assume that the actual core K is zero-dimensional and that the iterates of T=StableRange.restriction f:K→K are equicontinuous. The exact hypotheses are TotallyDisconnectedSpace K and Equicontinuous (fun n : ℕ => T^[n]); compact Hausdorff K turns the former into a clopen basis. These core hypotheses yield the extension described below. Empty and nonmetrizable spaces are included, with no countability, ambient surjectivity, injectivity, invertibility or source-shadowing assumption.
Equicontinuity uses the compatible compact Hausdorff uniformity. Starting with UniformSpace X uses its own topology; starting with a compact Hausdorff topology, uniformSpaceOfCompactR1 supplies a uniformity whose topology is definitionally the given one, on X or directly on its closed core K. This preserves topology and is not a metrization. The subtype uniformity on K is compatible. If the hypothesis is instead Equicontinuous (fun (n : ℕ) (c : K) => f^[n] c.val), the actual subtype inclusion semiconjugates T with f. Semiconj.iterate_right identifies its composite with T^[n] with that ambient-valued family; the subtype uniform embedding’s IsUniformInducing.equicontinuous_iff gives exactly the required equicontinuity of T’s iterates. UniformEquicontinuous first gives Equicontinuous by .equicontinuous.
Each iterate image f^n(X) is compact and closed, so StableRange.is_closed_core makes K closed and compact. StableRange.compact_surjective_restriction supplies continuity and surjectivity of this actual T. Indeed, for c∈K the nested nonempty closed sets f^n(X)∩f⁻¹({c}) have a common point by compactness, giving a preimage in K. A core point is supplied before a preimage is chosen, so the argument also covers the empty case.
Let B_K consist of all actual subsets A⊆X whose ambient frontier misses K. Put e(x)(A)=1_A(x), j(x)=(x,e(x)), and Y=closure(j(X))⊆X×{false,true}^{B_K}; this is RelativeBoolean.Space K, with the binary coordinates discrete. Let π=RelativeBoolean.projection K and s=RelativeBoolean.sectionC K, so s(c)=j(c). The closed product subtype Y is compact Hausdorff, π is continuous and onto, and s is continuous since every admissible indicator is locally constant at K. The graph j need not be continuous on X. Zero-dimensionality of Y comes from its cube-coordinate embedding: clopen neighborhoods in K and normal shrinking give separating ambient neighborhoods whose frontiers miss K. The resulting Boolean coordinates separate first coordinates, so the cube projection is injective, hence a closed embedding by compactness. Its clopen basis pulls back to Y; zero-dimensionality is not inferred from the product with X.
Forward invariance of K makes inverse image under f preserve B_K. The continuous ambient map (x,t)↦(f(x), A↦t(f⁻¹(A))) preserves the graph closure and restricts to g=RelativeBoolean.stableLift f hf. Thus π∘g=f∘π and g∘s=s∘T, and both identities iterate at every natural time, including zero. At c∈K every coordinate over c is forced to equal e(c), giving π⁻¹({c})={RelativeBoolean.point K c} and π(s(c))=c.val. In particular every y with π(y)∈K equals s(⟨π(y),membership⟩).
The exact lifted core is K_g=⋂_{n∈ℕ}g^n(Y)=π⁻¹(K)=range(s). For the first inclusion, project any upstairs n-step preimage. Conversely, when π(y)∈K, choose x with f^n(x)=π(y); then g^n(j(x)) and y lie in the same singleton fiber, so they are equal. Each finite n is handled separately. This is RelativeBoolean.stable_range_lift_eq_preimage, followed by the section identity. The map c↦⟨s(c),membership⟩ is a homeomorphism K→K_g with inverse induced by π; the singleton-fiber identities give its inverse laws, and continuity comes from s and π. It conjugates T with the actual restriction of g to K_g.
Fix a continuous finite observer q:Y→Fin m and put Q=q∘s. Applying finite_observation_period_of_equicontinuous_surjective to T and Q gives M>0 with Q(T^M(c))=Q(c) for every c∈K. Equicontinuity makes the complete Q-name map locally constant; compactness makes its image finite. Surjectivity of T makes shift on that image a finite permutation, whose positive exponent supplies M. For y∈K_g write y=s(c); the iterated section identity gives q(g^M(y))=q(s(T^M(c)))=q(s(c))=q(y). M may depend on q; no common point period on the whole core is required. This transfer uses s directly and requires no uniform structure on Y or K_g.
Now finite_observation_range_finite_of_stable_core_periodic applies to this derived positive period on the exact core of g. It gives finiteness of the whole-space range { (n↦q(g^n(y))) : y∈Y }, including transient points. The closed mismatch set {y : q(g^M(y))≠q(y)} misses K_g; compactness makes it miss some iterate image g^N(Y). Every name is therefore M-periodic after N and is determined by its first N+M symbols. Neither this finiteness nor a core period was assumed.
Apply initial_point_tracing_of_finite_observation_names on this compact Hausdorff zero-dimensional Y. For every finite open cover C it constructs an actual finite open control cover D from the singleton complete-name fibers of a clopen partition refining C, as above. Every D-pseudo-orbit a is C-shadowed by a(0) at every natural time. Taking a(0) as the tracing witness gives HasShadowing g, with continuous onto factor π. An initial point is used only after a pseudo-orbit is supplied, so no nonempty-space guard is needed.
The boundary-avoiding Boolean compactification follows the classical Stone/Banaschewski picture of the Michael modification, which isolates X outside K and retains the original neighborhoods at K. The bibliographic attribution is Bernhard Banaschewski, Über nulldimensionale Räume, Mathematische Nachrichten 13 (1955), 129–140, DOI 10.1002/mana.19550130302, as recorded in Library/Topology/banaschewski1955nulldimensional.md. The original article has not been inspected; no theorem number or exact relative formulation is attributed to it. A universal-property characterization is explanatory context, not an additional formalized theorem. The explicit relative graph and stable-range arguments are repository derivations.
This application is a sufficient criterion for zero-dimensional equicontinuous actual stable cores. It does not show that every shadowing system has these core properties. No equicontinuity conclusion for the whole upstairs map g is asserted. Peng’s unrestricted Question 5.1 and the simultaneous finite-face construction of Question 5.2 remain unresolved.