Dyadic Prefix Completion Times
Abstract
A dyadic sensor’s successful causal controllers have exact prefix completion times, and one controller realizes every prescribed nonnegative period-delay table.
Fix d>=0, P=2^(d+1), and a known initial high bit b. A prefix t<P/2 has two sources 2t and 2t+1. The earliest midpoint controller finishes either source at E(t)=P-1+P wt(t)-2t, where wt(t) is the number of nonzero binary digits of t. Controllers receive only raw high-bit observations and their own elapsed clock.
Theorem 1.1 (Delay-table execution on both final-bit siblings).
Proof. Machine-checked in Lean as D5/S3/Observer/Budget/DyadicPrefixDelayRange.delayed_midpoint_execute (✓ std3). ∎
Source. Repository-derived.
Commentary.
For any P, delay table K, and readout agreeing with the threshold below P and invariant under addition of P periods, the recursively delayed midpoint tree returns the same answer as the earliest tree. Its actual last-read time adds exactly P K(floor(r/2)). The source interval has even start a, length 2^(d+1), and lies below P; r ranges over that whole interval, with arbitrary initial time now.
Theorem 1.2 (One causal controller realizes an entire delay table).
Proof. Machine-checked in Lean as D5/S3/Observer/Budget/DyadicPrefixDelayRange.arbitrary_prefix_delay_table (✓ std3). ∎
Source. Repository-derived.
Commentary.
The midpoint questions before the final query distinguish the prefix t. At that query the controller adds P K(t) to its waiting increment. The added interval leaves the threshold unchanged, and raw-bit transport preserves both the answer and the completion time. Thus the same tree succeeds on every source and realizes every entry of K simultaneously.
Theorem 1.3 (Every successful controller has a nonnegative period correction).
Proof. Machine-checked in Lean as D5/S3/Observer/Budget/DyadicPrefixDelayRange.arbitrary_protocol_prefix_time (✓ std3). ∎
Source. Repository-derived.
Commentary.
Binary capacity forces each query to cut its current interval at the midpoint. The first forward occurrence of that phase is no later than any successful controller’s corresponding query. Induction along every source path gives the earliest-time lower bound; the terminal sibling phase then makes the nonnegative difference an integer multiple of P. Both possible last source bits are included.
For deadline D, F_D is the family of actual successful depth-(d+1) raw-bit protocols whose last read is at most D on every source r<P. Write W=sharpWait(d+1), E(t)=P-1+P wt(t)-2t, N_p(r) for the actual last-read time, and Y_p(r) for the raw final bit. The family range result below proves no controller exists below W. For D>=W it characterizes each reachable prefix time and gives an operational same-raw-bit collision when E(t)+P<=D. It does not assert the full minimum clock alphabet.
Theorem 1.4 (Exact deadline times and a cross-controller collision).
Proof. Machine-checked in Lean as D5/S3/Observer/Budget/DyadicPrefixDelayRange.deadline_prefix_time_range_and_collision (✓ std3). ∎
Source. Repository-derived.
Commentary.
A one-prefix delay table reaches each permitted time while the earliest tree keeps every other source within W. A controller below W contradicts the sharp waiting lower bound. For an eligible prefix, the zero-delay even source and one-period-delayed odd source have the same actual raw final read, although their source residues differ and their terminal times differ by P.
Theorem 1.5 (One decoder for every deadline-family controller).
Proof. Machine-checked in Lean as D5/S3/Observer/Budget/DyadicPrefixDelayRange.deadline_family_operational_capacity (✓ std3). ∎
Source. Repository-derived.
Commentary.
Labels are counted only when attained at a terminal time of a successful controller in the common-deadline family. For D below the sharp wait the family is empty. Otherwise any time-only encoder admitting one decoder for every controller and source uses at least 2^d plus the number of prefixes whose earliest time plus one period meets D. The explicit time tag records the prefix and delay parity, and one decoder combines it with the original uncorrected raw final bit. Its actual label image has exactly that cardinality. This proves the deadline-family operational part of source section 9.2; the closed-form slack staircase remains separate.
References
- Truth anchor:
D5/S3/Observer/Budget/DyadicPrefixDelayRange.arbitrary_prefix_delay_table - Truth anchor:
D5/S3/Observer/Budget/DyadicPrefixDelayRange.arbitrary_protocol_prefix_time - Truth anchor:
D5/S3/Observer/Budget/DyadicPrefixDelayRange.deadline_family_operational_capacity - Truth anchor:
D5/S3/Observer/Budget/DyadicPrefixDelayRange.deadline_prefix_time_range_and_collision - Truth anchor:
D5/S3/Observer/Budget/DyadicPrefixDelayRange.delayed_midpoint_execute - Dependency: D5/S3/Observer/Budget/TerminalClockCompression