Saturated histories of the original stationary controller
Abstract
A saturated worst-case read bound forces complete physical history trees and distinct reading slots.
Use the original Controller and Correct model on ZMod(pP), with p at least two, P positive, and an initial read. The action table has fixed read successors, fixed wait successors and fixed terminal outputs. The physical source stays in the joint run. readEvents(x) is the finite set of actual read times before the correct halt. firstFiber(b) is the set of original inputs whose initial physical digit is b, and has P elements.
A SaturatedHistory certificate records a complete binary expansion, its remaining height, its current slot, its original-input support, and its physical read-time function. Every parent-to-child transition is realized on that same original input with only actual waits between the two reads. The zero time function supplies the first read. Thus the certificate describes the existing run and adds no control register or clock.
Write Entry for the dependent sum of remaining height, reading slot, finite original-input support, time function and SaturatedHistory certificate. entrySlot, entrySupport and entryTime denote its projections. historyEntries lists all nodes of one complete actual tree, including the first read and terminal reads. allHistories concatenates these trees over all first digits, in depth-first order. Its slot list is obtained by mapping entrySlot; get indexes this list.
readingPositions lists the pairs of child answer slots at every internal history. Each pair is one subsequent reading occurrence. Its two controls are equal and its digits are distinct. allReadingPositions concatenates these lists over first digits, excluding the initial reads. occurrenceCount counts, with multiplicity, the positions assigned to the specified control. TerminatesIn counts subsequent reads in the global actual-slot relation and retains the fixed terminal label.
Theorem 1.1 (Finite residues preserve natural values).
Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/SaturatedActualHistories.fin_equiv_val (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every nonzero natural modulus m and x in Fin m, Mathlib’s ZMod.finEquiv sends x to a residue with the same natural value.
Theorem 1.2 (Complete histories, slot injection and row packing).
Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/SaturatedActualHistories.result (✓ std3). ∎
Source. Repository-derived.
Commentary.
The finite set of later read times has a least next event whenever the current slot does not halt. Its removal decreases the remaining read count by one. The actual adjacent-slot contract partitions the original support into at most two children. This constructs an actual tree within the read budget, allowing empty branches and early terminal leaves. Erasing physical annotations gives a binary adaptive protocol, so the general leaf bound controls support size. Equality at two to the remaining depth excludes empty children and early leaves, producing the complete actual histories. The global slot expansion then fixes each node’s remaining height and original support. Ancestors have greater remaining height, sibling subtrees have disjoint supports, and different first digits have disjoint supports. Consequently their slots are distinct across the whole forest. Every physical read event belongs to one of these histories. Each subsequent occurrence occupies two distinct slots of one control; the whole forest has no repeated slot, giving at most floor(p/2) occurrences per control. At P=1 the complete trees have height zero and no such subsequent positions.