Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

KrausLeftInverseNecessity

Abstract

Actual finite Kraus left inversion forces scalar error products. Scalarity of composite Kraus maps is derived from a positive commutator defect. The represented-family quantifier is explicit.

Theorem 1.1 (identity kraus commute).

Lean statement: D5/S3/Quantum/Recovery/KrausLeftInverseNecessity.identity_kraus_commute

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

Source. Repository-derived.

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

Acknowledgement. Man-Duen Choi and Nathaniel Johnston and David W. Kribs (2009). The multiplicative domain in quantum error correction. DOI: 10.1088/1751-8113/42/24/245303.

Commentary.

Actual finite Kraus left inversion forces scalar error products. Scalarity of composite Kraus maps is derived from a positive commutator defect. The represented-family quantifier is explicit.

Theorem 1.2 (identity kraus scalar).

Lean statement: D5/S3/Quantum/Recovery/KrausLeftInverseNecessity.identity_kraus_scalar

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

Source. Repository-derived.

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

Acknowledgement. Man-Duen Choi and Nathaniel Johnston and David W. Kribs (2009). The multiplicative domain in quantum error correction. DOI: 10.1088/1751-8113/42/24/245303.

Commentary.

Actual finite Kraus left inversion forces scalar error products. Scalarity of composite Kraus maps is derived from a positive commutator defect. The represented-family quantifier is explicit.

Theorem 1.3 (left inverse error products).

Lean statement: D5/S3/Quantum/Recovery/KrausLeftInverseNecessity.left_inverse_error_products

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

Source. Repository-derived.

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

Acknowledgement. Man-Duen Choi and Nathaniel Johnston and David W. Kribs (2009). The multiplicative domain in quantum error correction. DOI: 10.1088/1751-8113/42/24/245303.

Commentary.

Actual finite Kraus left inversion forces scalar error products. Scalarity of composite Kraus maps is derived from a positive commutator defect. The represented-family quantifier is explicit.

References

  • Truth anchor: D5/S3/Quantum/Recovery/KrausLeftInverseNecessity.identity_kraus_commute
  • Truth anchor: D5/S3/Quantum/Recovery/KrausLeftInverseNecessity.identity_kraus_scalar
  • Truth anchor: D5/S3/Quantum/Recovery/KrausLeftInverseNecessity.left_inverse_error_products
  • Dependency: D5/S3/Quantum/Reduction/IsometricCompression