Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

StationaryHistoryPrefix

Abstract

Actual complete action prefixes, indexed reads, roots, and original terminal histories.

Fix P greater than one, one controller C on the full nominal carrier Q, and Initialized C hP ell h. Every original x in ZMod(3P) starts at the common initial control and physical phase x. Wait adds one, read returns the absolute digit floor(val/P), and halt stores an original label. Each path has ell initial waits, a first read, positive literal waits between reads, at most h reads, and halt immediately after its final read. Long waits, modular wraps, singleton continuations, unused nominal states, and control cycles which terminate on all initialized inputs are retained.

Action records wait, read with its actual answer, or halt with its stored label. Trace x t records every action before time t. The finite ordered set readTimes x enumerates all actual read times; reads x is its cardinality. Event is the dependent pair (x,i), with i in Fin(reads x). Its full eventWord ends at that read and includes all previous waits and answers. History is the finite image of these words; word(n) means its full list n.val. Drawing an existing path again introduces no node. Sharing a row or a wait length does not identify two different full words. In a physical-phase expression, every natural shift is cast into ZMod(3P); the shift itself remains a literal natural number.

Theorem 1.1 (Exact prefix replay).

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/StationaryHistoryPrefix.trace_reconstruction (✓ std3). ∎

Source. Repository-derived.

Commentary.

Replay is the left fold of the controller transition over the complete action and answer word. The list fold concatenation law separates the earlier prefix from its next action, so induction on time reconstructs the control. The physical phase is x plus the number of literal wait actions; reads and absorbing halts contribute no physical increment.

Theorem 1.2 (Every history has an indexed occurrence).

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/StationaryHistoryPrefix.event_surjective (✓ std3). ∎

Source. Repository-derived.

Commentary.

History is the finite image of full indexed read prefixes. Every history therefore has an original input and read index producing it.

Theorem 1.3 (One history per read index of an input).

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/StationaryHistoryPrefix.event_input_injective (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a fixed original input, equal full prefixes have equal lengths and read times. The increasing enumeration of read times then gives the same read index.

Theorem 1.4 (An indexed prefix reconstructs its read).

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/StationaryHistoryPrefix.event_reconstruction (✓ std3). ∎

Source. Repository-derived.

Commentary.

Removing the last action leaves the exact pre-read trace. Replay reconstructs its configuration, and the final recorded answer is the actual absolute digit there.

Theorem 1.5 (Configuration of a supporting label).

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/StationaryHistoryPrefix.history_configuration (✓ std3). ∎

Source. Repository-derived.

Commentary.

Support consists exactly of original labels whose indexed read produces this full prefix. Time is word length minus one, level is the number of recorded reads minus one, and historyShift counts every literal wait.

Theorem 1.6 (Unique prefix parent).

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/StationaryHistoryPrefix.parent_successor (✓ std3). ∎

Source. Repository-derived.

Commentary.

The parent truncates the full word to the greatest earlier read position. It is defined from the word itself, so every nonroot history has one parent regardless of row sharing or repeated control states.

Theorem 1.7 (Exactly the first-answer roots).

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/StationaryHistoryPrefix.roots_exact (✓ std3). ∎

Source. Repository-derived.

Commentary.

The three roots are ell literal waits followed by one read with answer c. Every answer occurs because all original input phases are initialized.

Theorem 1.8 (Literal time accounting).

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/StationaryHistoryPrefix.history_time_decomposition (✓ std3). ∎

Source. Repository-derived.

Commentary.

Before the current read, each live action is either one wait or an earlier read. Thus time equals physical shift plus read level, without reducing the shift modulo P or modulo 3P.

Theorem 1.9 (Actual graph leaves).

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/StationaryHistoryPrefix.leaf_iff_terminal (✓ std3). ∎

Source. Repository-derived.

Commentary.

IsLeaf means that no actual history has this prefix as parent. It is equivalent to halt immediately after the recorded read. A nonfinal read has a later actual child even when its support is a singleton.

Theorem 1.10 (Every leaf emits its original supporting label).

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/StationaryHistoryPrefix.leaf_original (✓ std3). ∎

Source. Repository-derived.

Commentary.

A supporting occurrence of a graph leaf is that input’s final read. Its post-read instruction halts with the same original label.

References