Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

OrthogonalSyndromeChannel

Abstract

Concrete canonical CPTP encoding and full-space decoding of arbitrary positive unit-trace syndrome densities, together with the multiplicative logical algebra. This is classical orthogonal-syndrome correction, with no novelty claim.

Theorem 1.1 (logical representation mul).

Lean statement: D5/S3/Quantum/Recovery/OrthogonalSyndromeChannel.logical_representation_mul

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

Source. Repository-derived.

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

Acknowledgement. Cédric Bény and Achim Kempf and David W. Kribs (2007). Quantum Error Correction of Observables. DOI: 10.1103/PhysRevA.76.042303.

Commentary.

Concrete canonical CPTP encoding and full-space decoding of arbitrary positive unit-trace syndrome densities, together with the multiplicative logical algebra. This is classical orthogonal-syndrome correction, with no novelty claim.

Theorem 1.2 (logical representation on copy).

Lean statement: D5/S3/Quantum/Recovery/OrthogonalSyndromeChannel.logical_representation_on_copy

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

Source. Repository-derived.

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

Acknowledgement. Cédric Bény and Achim Kempf and David W. Kribs (2007). Quantum Error Correction of Observables. DOI: 10.1103/PhysRevA.76.042303.

Commentary.

Concrete canonical CPTP encoding and full-space decoding of arbitrary positive unit-trace syndrome densities, together with the multiplicative logical algebra. This is classical orthogonal-syndrome correction, with no novelty claim.

Theorem 1.3 (logical action on encoding).

Lean statement: D5/S3/Quantum/Recovery/OrthogonalSyndromeChannel.logical_action_on_encoding

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

Source. Repository-derived.

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

Acknowledgement. Cédric Bény and Achim Kempf and David W. Kribs (2007). Quantum Error Correction of Observables. DOI: 10.1103/PhysRevA.76.042303.

Commentary.

Concrete canonical CPTP encoding and full-space decoding of arbitrary positive unit-trace syndrome densities, together with the multiplicative logical algebra. This is classical orthogonal-syndrome correction, with no novelty claim.

Theorem 1.4 (full syndrome decoder).

Lean statement: D5/S3/Quantum/Recovery/OrthogonalSyndromeChannel.full_syndrome_decoder

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

Source. Repository-derived.

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

Acknowledgement. Cédric Bény and Achim Kempf and David W. Kribs (2007). Quantum Error Correction of Observables. DOI: 10.1103/PhysRevA.76.042303.

Commentary.

Concrete canonical CPTP encoding and full-space decoding of arbitrary positive unit-trace syndrome densities, together with the multiplicative logical algebra. This is classical orthogonal-syndrome correction, with no novelty claim.

Theorem 1.5 (encoding kraus gram).

Lean statement: D5/S3/Quantum/Recovery/OrthogonalSyndromeChannel.encoding_kraus_gram

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

Source. Repository-derived.

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

Acknowledgement. Cédric Bény and Achim Kempf and David W. Kribs (2007). Quantum Error Correction of Observables. DOI: 10.1103/PhysRevA.76.042303.

Commentary.

Concrete canonical CPTP encoding and full-space decoding of arbitrary positive unit-trace syndrome densities, together with the multiplicative logical algebra. This is classical orthogonal-syndrome correction, with no novelty claim.

Theorem 1.6 (encoding kraus action).

Lean statement: D5/S3/Quantum/Recovery/OrthogonalSyndromeChannel.encoding_kraus_action

Proof. Machine-checked in Lean as D5/S3/Quantum/Recovery/OrthogonalSyndromeChannel.encoding_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.

Acknowledgement. Cédric Bény and Achim Kempf and David W. Kribs (2007). Quantum Error Correction of Observables. DOI: 10.1103/PhysRevA.76.042303.

Commentary.

Concrete canonical CPTP encoding and full-space decoding of arbitrary positive unit-trace syndrome densities, together with the multiplicative logical algebra. This is classical orthogonal-syndrome correction, with no novelty claim.

Theorem 1.7 (gram syndrome encoder).

Lean statement: D5/S3/Quantum/Recovery/OrthogonalSyndromeChannel.gram_syndrome_encoder

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

Source. Repository-derived.

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

Acknowledgement. Cédric Bény and Achim Kempf and David W. Kribs (2007). Quantum Error Correction of Observables. DOI: 10.1103/PhysRevA.76.042303.

Commentary.

Concrete canonical CPTP encoding and full-space decoding of arbitrary positive unit-trace syndrome densities, together with the multiplicative logical algebra. This is classical orthogonal-syndrome correction, with no novelty claim.

Theorem 1.8 (positive syndrome encoder).

Lean statement: D5/S3/Quantum/Recovery/OrthogonalSyndromeChannel.positive_syndrome_encoder

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

Source. Repository-derived.

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

Acknowledgement. Cédric Bény and Achim Kempf and David W. Kribs (2007). Quantum Error Correction of Observables. DOI: 10.1103/PhysRevA.76.042303.

Commentary.

Concrete canonical CPTP encoding and full-space decoding of arbitrary positive unit-trace syndrome densities, together with the multiplicative logical algebra. This is classical orthogonal-syndrome correction, with no novelty claim.

References

  • Truth anchor: D5/S3/Quantum/Recovery/OrthogonalSyndromeChannel.encoding_kraus_action
  • Truth anchor: D5/S3/Quantum/Recovery/OrthogonalSyndromeChannel.encoding_kraus_gram
  • Truth anchor: D5/S3/Quantum/Recovery/OrthogonalSyndromeChannel.full_syndrome_decoder
  • Truth anchor: D5/S3/Quantum/Recovery/OrthogonalSyndromeChannel.gram_syndrome_encoder
  • Truth anchor: D5/S3/Quantum/Recovery/OrthogonalSyndromeChannel.logical_action_on_encoding
  • Truth anchor: D5/S3/Quantum/Recovery/OrthogonalSyndromeChannel.logical_representation_mul
  • Truth anchor: D5/S3/Quantum/Recovery/OrthogonalSyndromeChannel.logical_representation_on_copy
  • Truth anchor: D5/S3/Quantum/Recovery/OrthogonalSyndromeChannel.positive_syndrome_encoder
  • Dependency: D5/S3/Quantum/Recovery/KrausCompletion
  • Dependency: D5/S3/Quantum/Recovery/OrthogonalSyndromeDecoding