arXiv preprint ·
QECert: Formal Foundations for Quantum Error-Correction Theory in Lean
- Published
- Source
- arXiv preprint, posted before peer review
- Original
- Read it at arXiv
- Topics
Abstract
Quantum error correction provides the mathematical basis for protecting quantum information against noise. Existing formalizations have established foundations for stabilizer codes and code verification. However, a systematic formal treatment of the asymptotic constructions and fundamental limitations that underpin scalable quantum error correction is still needed. We present QECert, a Lean library providing reusable formal foundations for these theoretical questions. It connects quantum error-correction criteria, stabilizer and Calderbank-Shor-Steane codes, and algebraic and homological constructions within a common framework. Asymptotically good quantum low density parity check codes provide the principal case study. We formalize constructions and asymptotic parameter theorems spanning hypergraph products, balanced products, lifted products, and quantum Tanner codes. Further developments cover Bravyi-Poulin-Terhal bounds and related locality restrictions, constant overhead magic state distillation, and energy barriers and storage errors for quantum memories. QECert establishes a reusable formal foundation for studying the capabilities, resource requirements, and fundamental limitations of quantum error correction, supporting systematic verification and further development of its theory.
The authors’ abstract, as arXiv lists it. arXiv’s listings, abstracts included, are free for anyone to reuse.
Read it on ReadSearch
Each opens after you create an account, and brings you back to this paper.
More in Quantum Physics
Anti-distinguishability of quantum channels
Static and dynamical Casimir effects in a wedge within the worldline formulation
Entanglement Allocation for Quantum Integrated Sensing and Communication
Exact teleportation bounds for fermionic Hawking thermality beyond the single-mode approximation
Quantum identity authentication protocol via perturbed probability amplitudes
Get the few papers worth your time in Quantum Physics every morning.
ReadSearch reads the new papers in your field each day and brings you the few worth reading, each with its key finding in a sentence.