Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

KrausCompletion

Abstract

Explicit row-reset Kraus operators complete the input effect and produce the repository canonical CPTP channel. Spectral inverse construction is a separate obligation.

Theorem 1.1 (row reset action).

Lean statement: D5/S3/Quantum/Recovery/KrausCompletion.row_reset_action

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

Source. Repository-derived.

Acknowledgement. E. Knill and R. Laflamme (1997). Theory of quantum error-correcting codes. DOI: 10.1103/PhysRevA.55.900.

Commentary.

Explicit row-reset Kraus operators complete the input effect and produce the repository canonical CPTP channel. Spectral inverse construction is a separate obligation.

Theorem 1.2 (complete kraus action).

Lean statement: D5/S3/Quantum/Recovery/KrausCompletion.complete_kraus_action

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

Source. Repository-derived.

Acknowledgement. E. Knill and R. Laflamme (1997). Theory of quantum error-correcting codes. DOI: 10.1103/PhysRevA.55.900.

Commentary.

Explicit row-reset Kraus operators complete the input effect and produce the repository canonical CPTP channel. Spectral inverse construction is a separate obligation.

Theorem 1.3 (complete quantum channel).

Lean statement: D5/S3/Quantum/Recovery/KrausCompletion.complete_quantum_channel

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

Source. Repository-derived.

Acknowledgement. E. Knill and R. Laflamme (1997). Theory of quantum error-correcting codes. DOI: 10.1103/PhysRevA.55.900.

Commentary.

Explicit row-reset Kraus operators complete the input effect and produce the repository canonical CPTP channel. Spectral inverse construction is a separate obligation.

References