Original finite-memory directed graphs

Abstract

The original lower and upper finite-memory source languages are exactly the bilateral labels of a finite directed graph, whose retained paths have the original weighted adjacency expansion.

A vertex is a function from Fin n to the original c/u alphabet. Index zero holds the most recent past letter. Reversing these indices gives the chronological n-letter word. A transition inserts its label at index zero and drops the oldest letter. The seed composition uses the original high-side letter maps. A current run of K+1 c letters is forbidden. At the current Kth c, the lower graph requires a strict zero-seed bound; the upper graph requires a nonstrict h-seed bound. Both use the original threshold chi to K-1 times d.

Theorem 1.1 (window value).

$\forall n \in N a t, o m e g a \in I n t \to C uL e tt er, i \in I n t, z \in R e a l, memoryValue (memoryWindow (n, o m e g a, i), z) = finitePast (o m e g a, i, n, z)$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/MemoryGraph.window_value (✓ std3). ∎

Source. Repository-derived.

Commentary.

The graph seed composition equals finitePast on the actual n-letter past, for every real seed and integer position.

Theorem 1.2 (window shift).

$\forall n \in N a t, o m e g a \in I n t \to C uL e tt er, i \in I n t, memoryWindow (n, o m e g a, add (i, 1)) = memoryShift (memoryWindow (n, o m e g a, i), apply (o m e g a, i))$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/MemoryGraph.window_shift (✓ std3). ∎

Source. Repository-derived.

Commentary.

Moving one integer position inserts exactly the current letter into the past window.

Theorem 1.3 (path memory reconstruction).

$\forall n \in N a t, p \in I n t \to MemoryVertex (n), o m e g a \in I n t \to C uL e tt er, (\forall i \in I n t, apply (p, add (i, 1)) = memoryShift (apply (p, i), apply (o m e g a, i))) \Rightarrow p = memoryWindow (n, o m e g a)$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/MemoryGraph.path_memory_reconstruction (✓ std3). ∎

Source. Repository-derived.

Commentary.

Induction on each finite memory coordinate reconstructs it from the bilateral label sequence. No arbitrary memory annotation survives the shift equations.

Theorem 1.4 (window run).

$\forall n \in N a t, r \in N a t, o m e g a \in I n t \to C uL e tt er, i \in I n t, (lt (0, r) \land le (r, add (n, 1))) \Rightarrow (memoryRun (memoryWindow (n, o m e g a, i), apply (o m e g a, i), r) \Leftrightarrow (\forall k \in Fin (r), apply (o m e g a, subtract (i, toInt (k))) = c))$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/MemoryGraph.window_run (✓ std3). ∎

Source. Repository-derived.

Commentary.

For positive run lengths up to n+1, the finite memory test is exactly the run ending at the current position, including the current letter.

Theorem 1.5 (forbidden run reversal).

$\forall K \in N a t, o m e g a \in I n t \to C uL e tt er, (\forall i \in I n t, not (\forall k \in Fin (add (K, 1)), apply (o m e g a, add (i, toInt (k))) = c)) \Leftrightarrow (\forall i \in I n t, not (\forall k \in Fin (add (K, 1)), apply (o m e g a, subtract (i, toInt (k))) = c))$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/MemoryGraph.forbidden_run_reversal (✓ std3). ∎

Source. Repository-derived.

Commentary.

Reversing the K+1 indices converts the original forward forbidden block into the equivalent current-ending block without changing the sequence.

Theorem 1.6 (original memory graph correspondence).

$\forall s i d e \in M e m ory S i d e, n \in N a t, K \in N a t, d \in R e a l, \forall o m e g a \in I n t \to C uL e tt er, (lt (0, K) \land le (K, n)) \Rightarrow (member (o m e g a, MemoryLanguage (s i d e, n, K, d)) \Leftrightarrow existsUnique ((BilateralGraphPath (s i d e, K, d, p, o m e g a))_{p \in I n t \to MemoryVertex (n)}))$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/MemoryGraph.original_memory_graph_correspondence (✓ std3). ∎

Source. Repository-derived.

Commentary.

For n at least K and positive K, each original lower or upper sequence has exactly one bilateral graph path. Conversely every graph path has the reconstructed actual past windows and precisely the original guard at the current Kth c. All thresholds d remain in scope.

Theorem 1.7 (prepend bilateral path).

$\forall s i d e \in M e m ory S i d e, n \in N a t, K \in N a t, d \in R e a l, \forall v \in MemoryVertex (n), t \in MemoryVertex (n), a \in C uL e tt er, p \in I n t \to MemoryVertex (n), o m e g a \in I n t \to C uL e tt er, (LiveVertex (s i d e, K, d, v) \land (BilateralGraphPath (s i d e, K, d, p, o m e g a) \land (apply (p, 0) = t \land MemoryEdge (s i d e, K, d, v, a, t)))) \Rightarrow (\exists q \in I n t \to MemoryVertex (n), n u \in I n t \to C uL e tt er, BilateralGraphPath (s i d e, K, d, q, n u) \land (apply (q, 0) = v \land (apply (n u, 0) = a \land (\forall i \in I n t, le (0, i) \Rightarrow apply (n u, add (i, 1)) = apply (o m e g a, i)))))$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/MemoryGraph.prepend_bilateral_path (✓ std3). ∎

Source. Repository-derived.

Commentary.

A retained start supplies a genuine left past. One allowed edge joins it to a genuine right future at the edge target. The joined path preserves the selected label and every future letter.

Theorem 1.8 (retained walk extension).

$\forall s i d e \in M e m ory S i d e, n \in N a t, K \in N a t, d \in R e a l, \forall v \in MemoryVertex (n), w \in List (C uL e tt er), RetainedWalk (s i d e, K, d, v, w) \Rightarrow (\exists p \in I n t \to MemoryVertex (n), o m e g a \in I n t \to C uL e tt er, BilateralGraphPath (s i d e, K, d, p, o m e g a) \land (apply (p, 0) = v \land (\forall k \in Fin (length (w)), apply (o m e g a, toInt (k)) = getElem (w, k))))$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/MemoryGraph.retained_walk_extension (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every finite path through retained vertices has an actual two-sided extension. Induction joins one edge at a time and preserves every finite word letter. Empty paths and transient bridges are included; strong connectivity is unnecessary.

Theorem 1.9 (bilateral path segment).

$\forall s i d e \in M e m ory S i d e, n \in N a t, K \in N a t, d \in R e a l, \forall p \in I n t \to MemoryVertex (n), o m e g a \in I n t \to C uL e tt er, w \in List (C uL e tt er), i \in I n t, (BilateralGraphPath (s i d e, K, d, p, o m e g a) \land (\forall k \in Fin (length (w)), apply (o m e g a, add (i, toInt (k))) = getElem (w, k))) \Rightarrow RetainedWalk (s i d e, K, d, apply (p, i), w)$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/MemoryGraph.bilateral_path_segment (✓ std3). ∎

Source. Repository-derived.

Commentary.

Any finite word occurring on one bilateral path gives a retained walk starting at its actual vertex. Translation supplies the required bilateral realization of each visited vertex.

Theorem 1.10 (original weighted path count).

$\forall s i d e \in M e m ory S i d e, n \in N a t, K \in N a t, d \in R e a l, \forall T \in N a t, (lt (0, K) \land le (K, n)) \Rightarrow (Finite (RetainedPathDictionary (s i d e, n, K, d, T)) \land (le (factorCount (MemoryLanguage (s i d e, n, K, d), T), NatCard (RetainedPathDictionary (s i d e, n, K, d, T))) \land le (NatCard (RetainedPathDictionary (s i d e, n, K, d, T)), multiply (power (2, n), factorCount (MemoryLanguage (s i d e, n, K, d), T)))))$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/MemoryGraph.original_weighted_path_count (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every total weight T, the complete retained path dictionary is finite. Forgetting the initial vertex maps onto the original factor dictionary. A path is determined by its word and initial n-letter vertex, so its count is between the factor count and 2 to n times that count. Weight zero and unsupported weights retain the same formulas.

Theorem 1.11 (original weighted adjacency paths).

$\forall s i d e \in M e m ory S i d e, n \in N a t, K \in N a t, d \in R e a l, \forall z \in R e a l, (\forall k \in N a t, v \in CoreVertex (s i d e, n, K, d), c h o i ces \in Fin (k) \to Product (C uL e tt er, CoreVertex (s i d e, n, K, d)), CorePath (s i d e, K, d, k, v, c h o i ces) \Rightarrow RetainedWalk (s i d e, K, d, val (v), ofFn ((fst (apply (c h o i ces, i)))_{i \in Fin (k)}))) \land (\forall k \in N a t, v \in CoreVertex (s i d e, n, K, d), sum ((matrixEntry (power (weightedAdjacency (s i d e, n, K, d, z), k), v, t))_{t \in CoreVertex (s i d e, n, K, d)}) = sum ((coreMonomial (s i d e, K, d, z, k, v, c h o i ces))_{c h o i ces \in Fin (k) \to Product (C uL e tt er, CoreVertex (s i d e, n, K, d))}))$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/MemoryGraph.original_weighted_adjacency_paths (✓ std3). ∎

Source. Repository-derived.

Commentary.

The matrix is indexed by precisely the vertices appearing on bilateral paths. Its entry sums z to letterWeight(a) over all original allowed labels with those endpoints, including parallel labels. Each complete labeled path contributes z to its total original wordWeight; a disallowed path contributes zero. Matrix powers sum these monomials exactly. The empty path contributes one. Every allowed path supplies a retained word in the same graph, which has a two-sided extension by the preceding theorem. Identifying the convergence boundary with a unique spectral-radius-one root, and then identifying that root with the weighted factor rate, are separate conclusions.

trureturing — Discovering truth

Original finite-memory directed graphs

Abstract

References

Keyboard shortcuts

trureturing — Discovering truth

Original finite-memory directed graphs

Abstract

References