Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Control rewrite directional communication

Abstract

Every correct endpoint-local rewrite pays the required directions on each actual execution, and a fixed exchange attains both bounds.

Definition 1.1 (Both original rewrite outputs after local preparation).

Formalization. D5/S3/ObserverMemory/Algorithms/ControlRewriteDirectionalBound.RewriteCorrect (✓ std3).

Source. Repository-derived.

Commentary.

The original summary types are modules over ZMod 2, with control restrictions ellA and ellB and prescribed projection columns alpha and beta. Preparation maps them into arbitrary persistent local types. Correctness requires finite termination on every prepared pair and local outputs equal to (ellA(a)+ellB(b)) times their respective prescribed column.

Definition 1.2 (The exact zero, one or two bit exchange).

Formalization. D5/S3/ObserverMemory/Algorithms/ControlRewriteDirectionalBound.rewriteProtocol (✓ std3).

Source. Repository-derived.

Commentary.

The right endpoint sends its old control contribution precisely when alpha is nonzero and ellB is nonzero. The left endpoint sends its old contribution precisely when beta is nonzero and ellA is nonzero. The public order is right then left. A zero column produces zero locally; a zero remote restriction supplies a zero contribution locally. Both old summaries remain available until the leaf outputs commit. In the formulas get(h,j) is the optional list entry, and getD supplies false when it is absent; if(condition,x,y) is x when the condition holds and y otherwise.

Theorem 1.3 (Sharp directions on every execution).

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/ControlRewriteDirectionalBound.rewrite_directional_sharpness (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every successful evaluator history has the publicly determined query label at each preceding Boolean prefix and ends at its public leaf. Successful executions on one input are independent of sufficient fuel. These clauses apply to arbitrary persistent endpoint types.

For every correct protocol and every prepared original input, right-to-left bit count is at least the indicator of alpha nonzero and ellB nonzero, and left-to-right count is at least the indicator of beta nonzero and ellA nonzero. Both bounds concern the same execution. Their sum is a lower bound on its total bit length.

If the right-to-left count were zero, fixing the left prepared state and changing the right original summary by a control-one vector preserves the entire finite path. All questions on that path read only the unchanged left state, so the same public leaf and left output contradict the prescribed nonzero change. The symmetric argument proves the other direction.

The fixed exchange is correct on every original input and attains both direction counts and their sum. Its successful witnesses use at most three units of evaluator fuel, including the public leaf. The lower bound permits arbitrary public trees with finite actual termination and imposes no global depth.

References