SpectralTransposeRecovery

Abstract

The existing finite-matrix functional calculus constructs a support projection and spectral inverse square root. Explicit Kraus completion gives a canonical CPTP candidate even for a zero CP branch. Exact recoverability and smoothness are separate conclusions.

Theorem 1.1 (spectral support on kraus).

Lean statement: D5/S3/Quantum/Recovery/SpectralTransposeRecovery.spectral_support_on_kraus

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

Source. Repository-derived.

Acknowledgement. H. Barnum and E. Knill (2002). Reversing quantum dynamics with near-optimal quantum and classical fidelity. DOI: 10.1063/1.1459754.

Commentary.

The existing finite-matrix functional calculus constructs a support projection and spectral inverse square root. Explicit Kraus completion gives a canonical CPTP candidate even for a zero CP branch. Exact recoverability and smoothness are separate conclusions.

Theorem 1.2 (spectral transpose candidate).

Lean statement: D5/S3/Quantum/Recovery/SpectralTransposeRecovery.spectral_transpose_candidate

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

Source. Repository-derived.

Acknowledgement. H. Barnum and E. Knill (2002). Reversing quantum dynamics with near-optimal quantum and classical fidelity. DOI: 10.1063/1.1459754.

Commentary.

The existing finite-matrix functional calculus constructs a support projection and spectral inverse square root. Explicit Kraus completion gives a canonical CPTP candidate even for a zero CP branch. Exact recoverability and smoothness are separate conclusions.

References

• Truth anchor: D5/S3/Quantum/Recovery/SpectralTransposeRecovery.spectral_support_on_kraus
• Truth anchor: D5/S3/Quantum/Recovery/SpectralTransposeRecovery.spectral_transpose_candidate
• Dependency: D5/S3/Quantum/Recovery/KrausCompletion