Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

FiniteLocalRecoveryObstruction

Abstract

For normalized common-label source families whose local rank-one projectors span every local Hermitian matrix space, an orthogonal pair at one holder rules out exact all-matrix recovery by any finite local protocol. The protocol permits arbitrary independent mixed local ancillas, adaptive coarse completely positive instruments, changing finite memories, repeated visits, zero branches and early leaves, with system unitary feedback only at termination. Scalar leaf maps and label-independent prefix weights are derived from recovery, not assumed.

Theorem 1.1 (finite local recovery obstruction).

Lean statement: D5/S3/Quantum/Recovery/FiniteLocalRecoveryObstruction.actual_informationally_complete_obstruction

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

Source. Repository-derived.

Commentary.

For normalized common-label source families whose local rank-one projectors span every local Hermitian matrix space, an orthogonal pair at one holder rules out exact all-matrix recovery by any finite local protocol. The protocol permits arbitrary independent mixed local ancillas, adaptive coarse completely positive instruments, changing finite memories, repeated visits, zero branches and early leaves, with system unitary feedback only at termination. Scalar leaf maps and label-independent prefix weights are derived from recovery, not assumed.

References