Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite Stationary Positive Interval Control

Abstract

A finite stationary unit table realizes positive interval sensing, recovers both source labels, and attains its logarithmic worst read count.

Fix natural p>=2 and P>0. Set H=clog(2,P), B=H(P-1), and X=ZMod(pP). The physical source starts at the unknown x. A wait adds one to the source and returns no information; a read preserves the source and returns floor([s]_(pP)/P). The table has one common Start control.

Apart from Start, a control stores a first digit in Fin(p), an ordered pair of interval endpoints in Fin(P), an elapsed count in Fin(B+1), a remaining-wait counter in Fin(P), and a mode in Fin(3). The modes are Wait, Read, and Done. Every changing field belongs to this finite carrier Q. The fixed action, wait successor, read successor, and output tables use only these fields and, for a read successor, the actual digit. Write Q=Control(p,P,B) and C for this fixed table.

The first read stores its digit and the full interval. A singleton enters Done; otherwise the control enters Wait with the positive phase distance minus one in the countdown. Each Wait performs one source increment, increments the stored elapsed count, and either decreases the countdown or enters Read when it was zero. Read splits the interval at its midpoint, using the retained digit and stored elapsed count to decode the actual answer. The successor is Done for a singleton and otherwise Wait. Waiting requires the elapsed count to be below B; a final read remains available at B. Other nonterminal rows perform a read and enter Done, so all nominal rows and all digits have a defined successor.

For a natural list w, Unit(w) concatenates W repeated w_i times and one R for each entry. Follows(C,c,v,z) recursively checks that each letter of v is exactly the action prescribed at c, then applies the corresponding unit transition. It ends at z with no additional action. RCount and WCount count the corresponding letters. Initial(q)=bP+L modulo pP and Current(q)=bP+L+E modulo pP are fixed functions of the terminal control. All letters in R::Unit(w) are actual source actions.

Theorem 1.1 (Finite execution, both outputs, exact counts, and the singleton case).

Proof. Machine-checked in Lean as D5/S3/Observer/Budget/FinitePositiveIntervalControl.result (✓ std3). ∎

Source. Repository-derived.

Commentary.

Induction on the interval tree constructs the same physical execution as its query semantics. A countdown segment executes exactly its positive number of unit waits, with every intermediate elapsed count inside Fin(B+1). The ensuing read selects the correct child interval. The budget inequality guarantees that the waiting guard succeeds, including a segment whose last wait reaches B. At a leaf, the two fixed outputs equal the original and current sources. The original source P-1 follows the rightmost path and attains exactly 1+H reads. For P=1 the sole first read immediately reaches the correct halt control.

References