Buffered Whole-Path Retained-Cone Extension
Abstract
A finite buffered mixed old/new graph retains every old whole path and has one outer-buffer tracer for every new whole path.
Theorem 1.1 (Finite mixed-buffer graph extension).
Proof. Machine-checked in Lean as D5/S1/Dynamics/Shadowing/BufferedConeExtension.buffered_whole_path_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.
For finite old and new discrete alphabets, closed inner buffers are placed inside old P/C and new D interiors. A compactness transfer cover and the existing finite-open-cover HasShadowing contract produce a finite control cover T.
The graph has vertices V×T×B. Its edge relation contains the old edge and one actual point t in X witnessing every old P and new L constraint at both endpoints. The first-coordinate map preserves edges and lifts every specified complete old vertex path, retaining its time-zero vertex.
One shadowing tracer serves an entire new path, placing all its iterates in the outer C/D interiors. Conversely, one specified source x lifts every complete old-K/new-L name. This is a fixed finite cone result; it does not supply the global uniform-follower lemma or solve Peng Question 5.1.
The four-slot Reg audit for buffered_whole_path_extension remains unfinished. The existing dependent-family owner recipe does not supply this theorem’s typed equivalence, variation, sensitivity, observational dependence and exact source-selection evidence. See https://github.com/the-omega-institute/trureturing/issues/25272. No validated registration is claimed.