Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

RetainedLocalProtocol

Abstract

For every finite local instrument tree and every input matrix with arbitrary finite inaccessible garbage and untouched spectator, tracing the recursively retained outputs reproduces the complete coarse terminal and prefix lists. At every nonterminal root the internally selected spectral Kraus data reproduce its actual CP action on every local matrix. Later operations leave old garbage coordinates untouched and branch only on observed outcomes.

Theorem 1.1 (recursive coarse retained).

Lean statement: D5/S3/Quantum/Recovery/RetainedLocalProtocol.recursive_coarse_retained

Proof. Machine-checked in Lean as D5/S3/Quantum/Recovery/RetainedLocalProtocol.recursive_coarse_retained (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every finite local instrument tree and every input matrix with arbitrary finite inaccessible garbage and untouched spectator, tracing the recursively retained outputs reproduces the complete coarse terminal and prefix lists. At every nonterminal root the internally selected spectral Kraus data reproduce its actual CP action on every local matrix. Later operations leave old garbage coordinates untouched and branch only on observed outcomes.

References