Prescribed-word realization

Abstract

An essential directed multigraph realizes every prescribed positive legal word as one actual bi-infinite history, retaining every edge label.

Theorem 1.1 (One actual history containing the entire prescribed word).

$$\forall V\in Type,E\in Type,[\mathrm{Fintype}\left(V\right)],[\mathrm{Fintype}\left(E\right)],[\mathrm{DecidableEq}\left(V\right)],\forall G\in \mathrm{DirectedMultigraph}\left(V,E\right),n\in Nat,word\in \mathrm{LegalWord}\left(G,n\right),\mathrm{Essential}\left(G\right)\Rightarrow \left(0<n\Rightarrow \left(\exists x\in \mathrm{History}\left(G\right),\forall j\in \mathrm{Fin}\left(n\right),\mathrm{historyEdge}\left(x,j\right)=\mathrm{wordEdge}\left(word,j\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/EssentialWordRealization.exists_history_containing (✓ std3). ∎

Source. Repository-derived.

Commentary.

Essential means that each vertex has an actual outgoing edge and an actual incoming edge. Edges are elements of the supplied edge type, so loops and distinct parallel edges remain distinct. LegalWord stores all those edges and each target/source adjacency equation. History is the subtype of Int-indexed actual edges satisfying every adjacency equation.

In the display, historyEdge(x,j) is x evaluated at the integer cast of j; wordEdge(word,j) is the j-th prescribed edge. The history uses iterated incoming choices at negative times, the entire prescribed word at times 0 through n minus 1, and iterated outgoing choices afterward. The proof verifies both outer seams and every interior seam. No strong connectivity, word-extension assumption or redefinition by globally realizable words is present.

The positive-length requirement covers both table lengths, both seam lengths and the common recovery length in the finite-window criterion, for all four natural radii including zero. The empty LegalWord type does not specify a vertex for a zero-edge path.

References

• Truth anchor: D5/S3/ConceptDynamics/Coding/EssentialWordRealization.exists_history_containing