Arbitrary-Index Constrained Product

Abstract

A common-source constrained product of arbitrary many actual metric extensions has shadowing under positive expansivity.

Theorem 1.1 (Every observation has finite support).

$$\begin{array}{r}\forall I:Type,\forall Y:I\Rightarrow Type,\\ [\forall i:I,\mathrm{MetricSpace}(Y(i))]\\ \forall S:\mathrm{Set}(\mathrm{Product}(Y)),\forall E:\mathrm{Set}(\mathrm{Pair}(S)),\\ \mathrm{Entourage}(S,E)\Rightarrow \\ \exists F:\mathrm{Finset}(I),eps:I\Rightarrow \mathbb{R},\\ \mathrm{PositiveOn}(eps,F)\wedge \mathrm{CylinderImplies}(S,F,eps,E)\end{array}$$

Proof. Machine-checked in Lean as D5/S1/Dynamics/Shadowing/ConstrainedProduct.finite_support_entourage (✓ std3). ∎

Source. Repository-derived.

Commentary.

I is any set-index type, Y(i) any dependent metric family, S any product subspace, and E any entourage on S. There are a finite F and real eps(i)>0 for i in F such that, for every a,b in S, all inequalities dist(a(i),b(i))<eps(i) on F imply (a,b) in E. Subtype uniformity, Pi.uniformity, Filter.HasBasis.iInf’ and the metric distance basis produce this implication. Neither I nor F must be nonempty.

Theorem 1.2 (Shadowing in the actual constrained subspace).

$$\begin{array}{r}\forall I:Type,\forall X:Type,[\mathrm{UniformSpace}(X)][\mathrm{CompactSpace}(X)]\\ \forall B:I\Rightarrow Type,\forall Y:I\Rightarrow Type,\\ [\forall i:I,\mathrm{MetricSpace}(B(i))][\forall i:I,\mathrm{MetricSpace}(Y(i))][\forall i:I,\mathrm{CompactSpace}(Y(i))]\\ \forall pi:\mathrm{DependentMap}(I,X,B),\forall p:\mathrm{CoordinateMap}(I,Y,B),\\ \mathrm{CoordinateContinuous}(pi,p)\Rightarrow \\ \mathrm{SeparatesPoints}(pi)\Rightarrow \\ \mathrm{CoordinateSurjective}(p)\Rightarrow \\ \forall f:X\Rightarrow X,\forall d:\mathrm{CoordinateEndomorphism}(B),\forall g:\mathrm{CoordinateEndomorphism}(Y),\\ \mathrm{CoordinateSemiconjugacies}(pi,p,f,d,g)\Rightarrow \\ \mathrm{HasShadowing}(f)\wedge \mathrm{CoordinateShadowing}(g)\wedge \mathrm{CoordinatePositiveExpansivity}(d)\Rightarrow \\ \mathrm{HasShadowing}(\mathrm{CommonSourceDynamics}(pi,p,f,d,g))\end{array}$$

Proof. Machine-checked in Lean as D5/S1/Dynamics/Shadowing/ConstrainedProduct.constrained_product_hasShadowing (✓ std3). ∎

Source. Repository-derived.

Commentary.

CoordinateContinuous means that every pi(i):X to B(i) and p(i):Y(i) to B(i) is continuous. CoordinateSurjective means every p(i) is onto. CoordinateSemiconjugacies asserts pi(i) f=d(i) pi(i) and p(i) g(i)=d(i) p(i). CoordinateShadowing and CoordinatePositiveExpansivity quantify over all i. No source or coordinate dynamics is required to be onto. The supplied metric extension spaces Y(i), their compactness and shadowing, and the positive expansive factors B(i), are parameters. No paper extension theorem is treated as an existing Lean instance.

Z consists of y in the product of Y(i) for which there exists one x with p(i)(y(i))=pi(i)(x) for every i. Separation makes x unique. For an entourage E on Z, finite_support_entourage selects F and tolerances. For every i in F, positive_expansivity_source_relative derives the exact-fibre tracing controls before the sequence is given. A finite intersection of pulled-back base observations and the projection’s uniform continuity give the pseudo-orbit control. One base shadowing point x is chosen. The controlled coordinates trace in the exact fibres over pi(i)(x); uncontrolled coordinates are filled in those same fibres by choice. Their tuple lies in Z and E-traces at every natural time.

Theorem 1.3 (Topology, projection and simultaneous whole orbits).

$$\begin{array}{r}\forall I:Type,\forall X:Type,[\mathrm{TopologicalSpace}(X)][\mathrm{CompactSpace}(X)][\mathrm{TTwoSpace}(X)]\\ \forall B:I\Rightarrow Type,\forall Y:I\Rightarrow Type,\\ [\forall i:I,\mathrm{MetricSpace}(B(i))][\forall i:I,\mathrm{MetricSpace}(Y(i))][\forall i:I,\mathrm{CompactSpace}(Y(i))][\forall i:I,\mathrm{TotallyDisconnectedSpace}(Y(i))]\\ \forall pi:\mathrm{DependentMap}(I,X,B),\forall p:\mathrm{CoordinateMap}(I,Y,B),\\ \mathrm{CoordinateContinuous}(pi,p)\Rightarrow \\ \mathrm{SeparatesPoints}(pi)\Rightarrow \\ \mathrm{CoordinateSurjective}(p)\Rightarrow \\ \forall f:X\Rightarrow X,\forall d:\mathrm{CoordinateEndomorphism}(B),\forall g:\mathrm{CoordinateEndomorphism}(Y),\\ \mathrm{CoordinateSemiconjugacies}(pi,p,f,d,g)\Rightarrow \\ \mathrm{HasShadowing}(f)\wedge \mathrm{CoordinateShadowing}(g)\wedge \mathrm{CoordinatePositiveExpansivity}(d)\Rightarrow \\ \mathrm{CoordinateContinuous}(g)\Rightarrow \\ Z=\mathrm{CommonSource}(pi,p),q=\mathrm{CommonSourceMap}(pi,p),\\ G=\mathrm{CommonSourceDynamics}(pi,p,f,d,g)\\ \mathrm{IsClosed}(\mathrm{CommonSourceSet}(pi,p))\wedge \\ \mathrm{CompactSpace}(Z)\wedge \mathrm{TTwoSpace}(Z)\wedge \mathrm{TotallyDisconnectedSpace}(Z)\wedge \\ \mathrm{Continuous}(q)\wedge \mathrm{Surjective}(q)\wedge \mathrm{Continuous}(G)\wedge \\ \mathrm{Semiconj}(q,G,f)\wedge \mathrm{HasShadowing}(G)\wedge \\ \mathrm{WholeOrbitCoding}(X,I,Z,q,G,p,pi,f)\end{array}$$

Proof. Machine-checked in Lean as D5/S1/Dynamics/Shadowing/ConstrainedProduct.constrained_product_extension (✓ 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.

X is compact Hausdorff; the compatible uniformity is introduced explicitly inside the proof. Each Y(i) is also totally disconnected. The exact conclusion is a conjunction: commonSourceSet is closed; Z is compact, Hausdorff and totally disconnected; q is continuous and onto; G is continuous; q semiconjugates G to f; and G has the existing finite-open-cover shadowing property. WholeOrbitCoding is: for every x in X there is z in Z with q(z)=x and, for every i and every natural n including zero, p(i)((G^n(z))(i))=pi(i)(f^n(x)). Compact Hausdorff totally disconnected spaces have the Mathlib clopen basis. Z is the inverse image of the compact range of the separating coordinate embedding. Continuity of q follows through that embedding, not from continuity of an arbitrary choice function. Tychonoff and ordinary choice are represented by Mathlib and Classical.choice.

Empty and singleton index types, empty finite support and empty source are included. For an empty index, separation forces a nonempty source to be a singleton. No inverse orbit or orbit-surjectivity is used. Onto factor maps pi(i), compactness and shadowing of B(i), and continuity of f and d(i) may be added to recover the approved system telescope; the proof does not require these extra premises. Peng Q5.1 and Q5.2 remain open here. Without positive expansivity, the unpaid obligation is one joint source point lying in every finite coordinate’s prescribed-fibre tracer set, with the control chosen before each pseudo-orbit. ALP and vertex surjectivity do not pay it. No novelty or priority is claimed.

References

• Truth anchor: D5/S1/Dynamics/Shadowing/ConstrainedProduct.constrained_product_extension
• Truth anchor: D5/S1/Dynamics/Shadowing/ConstrainedProduct.constrained_product_hasShadowing
• Truth anchor: D5/S1/Dynamics/Shadowing/ConstrainedProduct.finite_support_entourage
• Dependency: D5/S1/Dynamics/Shadowing/UniformTracing