Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Actual Dyadic Deadline Repair Minimum

Abstract

The original causal deadline repair contract has the exact mixed-demand cyclic capacity.

In the formulas, div denotes natural-number division, real is the real coercion, and record(N,past) has event count N and read history past. The displayed writer and decoder condition expands CommonRepairFeasible. In support ranking, equivFin bijects each finite parity support with the ranks below its cardinality.

Let P=2^(d+1), n=2^d, and b be a known bit. A primitive policy chooses only forward events, noiseless nondisturbing reads, and stops from its acquired record. The deadline family includes every deterministic policy successful on every source in at most d+1 reads with literal final query N<=D. Reporting delay is unrestricted. A supported type (t,nu) retains the actual raw parity nu=floor(N/P) mod 2 and the phase center P-1-2t.

Definition 1.1 (Actual support demand).

Formalization. D5/S3/Observer/Budget/ActualDyadicDeadlineRepairMinimum.actualDemand (✓ std3).

Source. Repository-derived.

Commentary.

The demand at t is the cardinality of its actual raw-parity support. For D>=sharpWait(d+1) and t<n this is one or two.

Definition 1.2 (Lossless support ranking).

Formalization. D5/S3/Observer/Budget/ActualDyadicDeadlineRepairMinimum.supportedTypeRankEquiv (✓ std3).

Source. Repository-derived.

Commentary.

There is a prefix-preserving equivalence between actual supported raw types and demand-ranked types. Each finite raw-parity support is bijected with the ranks below its cardinality. Both inverse laws hold. A singleton has rank zero even when its sole raw parity is one. Double support has two ranks; unranking recovers the actual raw parity.

Theorem 1.3 (Exact closed error shell).

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

Source. Repository-derived.

Commentary.

Assume D>=sharpWait(d+1), m>=2, and m-1<=eps<m. Two prefix phase balls intersect exactly when the circular integer distance of their prefixes is less than m. A realized all-source schedule supplies the phase-distance scaling by two. Closed-ball intersection includes equality at eps=m-1. The circular seam and equal prefixes are included.

Theorem 1.4 (Both coloring transports).

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

Source. Repository-derived.

Commentary.

Under the same deadline and error-shell assumptions, for any label type Z the actual supported types admit a proper Z-coloring exactly when the ranked mixed-demand cyclic graph does. The equivalence preserves prefixes and distinct supported raw types in both directions. Unsupported pairs are given an existing supported color when extending to a total function. Different raw parities at the same prefix remain distinct adjacent types.

Theorem 1.5 (Original prefix-window size).

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

Source. Repository-derived.

Commentary.

For j>=2 and m>=2, the original logarithmic size condition 3+floor(log2(m))<=j implies 2m<2^(j-1).

Theorem 1.6 (Exact original shared-decoder minimum).

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

Source. Repository-derived.

Commentary.

For j>=2, h>=0, known b, P=2^j, n=2^(j-1), and D=(j-1)P+1+h, assume m>=2, m-1<=eps<m, j>=3+floor(log2(m)), n=ma+rho, rho<m, and a>=2rho. Put q=#{1<=i<=j:2^i<=h} and L=j-q. The least alphabet cardinality is max(2m,ceil((2n-L)/a))=2m+indicator(L<2rho). The logarithmic hypothesis supplies n>2m and a consecutive m-prefix window with double demand; these are consequences, not extra premises. Feasibility means a writer receiving only policy and actual pre-final record and one common receiver recovering every source for every deadline-family policy and every closed phase error. The label precedes the final read and future error. The receiver sees only phase, exact raw Y, label, and fixed public parameters; policy, N, and past reads are hidden. All-history label separation and the two coloring transports give both attainment and the universal lower bound.

References