Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

All-History Deadline Label Supports

Abstract

Causal labels over all histories are equivalent to coloring actual supported types.

In the formulas, record(N,past) has event count N and read history past. div and mod denote natural-number quotient and remainder, real is the real coercion, and angle brackets construct the indicated finite value. The expanded feasibility condition is CommonRepairFeasible.

Fix d>=0, P=2^(d+1), known b, a deadline D, and a closed error radius eps. The primitive deadline family requires correct acquisition on every source within d+1 reads and literal last-read time at most D. A type consists of a prefix t and raw clock parity nu=floor(N/P) mod 2 that is realized by some member of this entire family. Its circular phase center is P-1-2t. Two distinct supported types conflict when their closed phase balls intersect. Different parities at the same prefix have the same phase center.

Theorem 1.1 (Causal writing and one shared receiver).

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

Source. Repository-derived.

Commentary.

A proper coloring of the supported types yields a record-only writer. It normalizes and folds acquired pre-final reads to obtain t, computes nu from the pre-final event count, and emits the color of (t,nu). One receiver takes only noisy phase, the exact final raw bit, and that label; d,b,D,eps and the coloring are fixed public parameters. The receiver selects a compatible type using phase and label, then returns 2t+((Y+b+nu) mod 2). Properness makes the type unique. This receiver sees neither the policy, N, nor past reads, and works for all deadline-family policies, sources and closed errors.

A causal writer may depend on its policy and complete acquired pre-final record, but receives no unseen final source bit or future error. A type’s label support is the set of labels emitted by every realizing policy and every actual pre-final history for that type. It is not the image of a single fixed policy or a chosen representative history.

Theorem 1.2 (Nonempty and disjoint all-history supports).

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

Source. Repository-derived.

Commentary.

Every supported type has a nonempty label support. If one receiver recovers all policies and closed errors, conflicting types have disjoint supports. For any shared label, sibling replay under each realizing policy preserves the same reached pre-final record and chooses u=(b+nu) mod 2, giving raw Y=0. A shared closed-ball phase then gives the receiver identical inputs with different sources. This includes a single prefix with different nu.

Theorem 1.3 (Exact operational coloring equivalence).

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

Source. Repository-derived.

Commentary.

For any label type Z, an all-history causal writer with one common receiver exists exactly when the actual supported types admit a proper Z-coloring. Necessity selects one label from each nonempty support; disjointness makes the selection proper. Sufficiency constructs the causal writer and shared receiver described above. The criterion is expressed using actual closed-ball intersections. It does not itself identify the integer distance graph or compute its mixed-demand chromatic minimum.

References