Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

MatrixUnitDecoder

Abstract

Actual matrix units construct the full decoder without a syndrome basis. Its trace-pairing formula recovers supported commutant-weighted logical matrices. No global bundle or Chern-number claim is made.

Theorem 1.1 (decoder kraus gram).

Lean statement: D5/S3/Quantum/Recovery/MatrixUnitDecoder.decoder_kraus_gram

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

Source. Repository-derived.

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

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 matrix units construct the full decoder without a syndrome basis. Its trace-pairing formula recovers supported commutant-weighted logical matrices. No global bundle or Chern-number claim is made.

Theorem 1.2 (decoder trace pairing).

Lean statement: D5/S3/Quantum/Recovery/MatrixUnitDecoder.decoder_trace_pairing

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

Source. Repository-derived.

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

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 matrix units construct the full decoder without a syndrome basis. Its trace-pairing formula recovers supported commutant-weighted logical matrices. No global bundle or Chern-number claim is made.

Theorem 1.3 (matrix unit decoder channel).

Lean statement: D5/S3/Quantum/Recovery/MatrixUnitDecoder.matrix_unit_decoder_channel

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

Source. Repository-derived.

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

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 matrix units construct the full decoder without a syndrome basis. Its trace-pairing formula recovers supported commutant-weighted logical matrices. No global bundle or Chern-number claim is made.

Theorem 1.4 (represented matrix mul).

Lean statement: D5/S3/Quantum/Recovery/MatrixUnitDecoder.represented_matrix_mul

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

Source. Repository-derived.

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

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 matrix units construct the full decoder without a syndrome basis. Its trace-pairing formula recovers supported commutant-weighted logical matrices. No global bundle or Chern-number claim is made.

Theorem 1.5 (decoder recovers commutant weight).

Lean statement: D5/S3/Quantum/Recovery/MatrixUnitDecoder.decoder_recovers_commutant_weight

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

Source. Repository-derived.

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

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 matrix units construct the full decoder without a syndrome basis. Its trace-pairing formula recovers supported commutant-weighted logical matrices. No global bundle or Chern-number claim is made.

References

  • Truth anchor: D5/S3/Quantum/Recovery/MatrixUnitDecoder.decoder_kraus_gram
  • Truth anchor: D5/S3/Quantum/Recovery/MatrixUnitDecoder.decoder_recovers_commutant_weight
  • Truth anchor: D5/S3/Quantum/Recovery/MatrixUnitDecoder.decoder_trace_pairing
  • Truth anchor: D5/S3/Quantum/Recovery/MatrixUnitDecoder.matrix_unit_decoder_channel
  • Truth anchor: D5/S3/Quantum/Recovery/MatrixUnitDecoder.represented_matrix_mul
  • Dependency: D5/S3/Quantum/Recovery/KrausCompletion