Actual reading slots and stationary control capacity
Abstract
General-base stationary execution constructs its actual directed reading-slot graph and capacity bounds.
For p at least two and positive P, the source is ZMod(pP), and its digit is floor(val/P) in Fin p. The width P may in particular be p to any nonnegative integer power. A controller has one source-independent initial control and fixed total action, wait-successor, digit-row-successor and output functions. The three actions partition Q into read, wait and halt. Wait increments the source by one; read preserves it. Halt is absorbing in the mathematical trajectory and emits no action.
Correct supplies a finite stop time for every original source, fixed terminal decoding of that original source, and no earlier halt. The initial action is a read, a positive wait separates reads, and the final action is a read. Used(q,b) means an actual read at q with digit b. Waiting(q) means an actual wait at q. Terminal(q,b) adds that the fixed digit-row successor halts. Write R for the subtype of controls with at least one used digit.
StationaryUnitControl treats p=3 and P>1. The present model additionally admits P=1 and arbitrary p at least two. A correspondence between the two models is not formalized here.
Occurs(x,t,u) means t is before the stop on original input x, the control is the control of slot u, and the physical digit is its digit. Edge(u,v) means two such occurrences on the same original input at times i<j, with every intermediate action a wait. Edges count distinct slot pairs, including repeated pairs only once. Reading-control revisits and mergers are unrestricted.
A SlotGraph on R times Fin p records its root, used slots, successor sets and one target control for each nonempty successor set. Every successor has a used source and target, the p root slots are used and have no incoming edge, and every used nonroot slot has an incoming edge. Every successor set has at most two elements. At q, missing counts unused digits, excess sums incoming cardinalities minus one, and singles counts one-successor slots assigned to q. terminalCount counts used slots with no successor. All these counts refer to the same graph, with natural subtraction.
Theorem 1.1 (The actual graph, exact identity, and capacity bounds).
Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/ActualControlSlots.result (✓ std3). ∎
Source. Repository-derived.
Commentary.
The graph G has exactly the actual used slots and actual next-read edges. Its root is the common start. Every active slot follows a fixed positive wait chain to one target read control, with at most two cyclically adjacent digits. Final slots biject with original sources. The start cannot recur, since every physical value already occurs there initially. Every other reading control has a distinct actual immediate wait predecessor. Incidence accounting gives the displayed identity and the binary lower bound. A zero-deficit nonroot row gives a bipartite incidence relation of degree two on active predecessor slots and degree one on its p digits. Double counting makes p even. For odd p, every nonroot target therefore has a positive deficit, yielding the final product inequality, equivalently r at least 1 plus 2p(P-1)/(p-1). Natural subtraction is used throughout. Here r is NatCard(R), and w counts Waiting controls.