Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Actual Dyadic Deadline Support

Abstract

Primitive forward executions realize exactly the allowed dyadic final reads.

In the formulas, record(N,past) has event count N and read history past. Execution and ReachedRecord display their period index P while suppressing proof arguments. div and mod denote natural-number quotient and remainder; val unwraps finite values.

A record consists of an event count and chronological time/raw-bit reads. A policy takes only that record and chooses one forward event, a read, or a stop. Execution denotes a finite physical run from a supplied record. No source or future noise is an input to the policy. Fix d>=0, P=2^(d+1), a known b in Fin 2, and E(t)=P-1+P wt(t)-2t. The original query parameter is j=d+1.

Theorem 1.1 (Physical read order).

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

Source. Repository-derived.

Commentary.

For any positive period and any primitive run, events never decrease. The new read trace has the read word’s length, lies between the starting and reporting clocks, and is pairwise ordered by time. Silent events after the final read are permitted; the reporting clock need not be the final-read clock.

Theorem 1.2 (All-source causal realization).

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

Source. Repository-derived.

Commentary.

If D>=sharpWait(d+1), t<2^d, u<2, and E(t)+PK<=D, one record-only policy succeeds on every source in at most d+1 reads and reports by D. On source 2t+u it stops immediately after its literal final read at E(t)+PK.

Theorem 1.3 (Physical final-read normal form).

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

Source. Repository-derived.

Commentary.

For every all-source successful policy under the dyadic read budget, each bounded actual execution has exactly d pre-final reads. Their normalized chronological fold is floor(r/2). The pre-final record is physically reached, the policy reads there, and raw Y=(b+floor(N/P)+r mod 2) mod 2. Its literal final time is E(floor(r/2))+PK for a nonnegative K and is no later than reporting.

DeadlineObservation(d,b,D,policy,r,past,N,Y) means that a correct primitive execution from (0,[]) uses at most d+1 reads, ends its read trace in past++[(N,Y)], and has N<=D. The all-source family requires such an observation for every source. SupportedTime ranges over all policies in this family and all observations with floor(r/2)=t. The deadline always bounds N, rather than any later reporting event.

Theorem 1.4 (Reached deadline observations).

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

Source. Repository-derived.

Commentary.

For a policy in actualDeadlineFamily(d,b,D), each deadline observation has the acquired prefix, reached pre-final record, read action, literal raw bit, and nonnegative period-delay normal form. The history in this statement is the history actually appearing in that observation.

Theorem 1.5 (One policy and one history for both siblings).

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

Source. Repository-derived.

Commentary.

Assume D>=sharpWait(d+1), t<2^d, and E(t)+PK<=D for a natural K. For each such allowed time, the same all-source policy and reached pre-final history realize both final source bits. The writer’s acquired prefix and read action are fixed before either final bit is obtained. The final raw bit is retained.

Theorem 1.6 (Exact actual supported times).

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

Source. Repository-derived.

Commentary.

With D at least the sharp common waiting bound and t<2^d, the supported times of each prefix are exactly E(t)+PK with K a natural number and E(t)+PK<=D.

Theorem 1.7 (Raw clock quotient).

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

Source. Repository-derived.

Commentary.

For t<2^d, floor((E(t)+PK)/P)=wt(t)+K. Thus raw clock parity is (wt(t)+K) mod 2. The delay tag K mod 2 alone is a different quantity.

Theorem 1.8 (Singleton and double raw-parity support).

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

Source. Repository-derived.

Commentary.

If D>=sharpWait(d+1) and t<2^d, the actual support B_D(t) contains wt(t) mod 2. It contains both parities exactly when E(t)+P<=D. Its definition ranges over all realizing policies and their actual histories, rather than a fixed controller.

Theorem 1.9 (Exact primitive type staircase).

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

Source. Repository-derived.

Commentary.

For D=sharpWait(d+1)+h, q counts 1<=i<=d+1 with 2^i<=h. There are L=d+1-q singleton prefixes and M=2^(d+1)-(d+1)+q actual types. Equivalently, n=2^d and M=2n-L. A singleton whose raw parity is one still contributes one type. This counts actual supported types; it does not determine the noisy hidden-schedule label minimum.

References