QECTOR Research Archive
The research and verification archive of QECTOR, the quantum error correction work of Guillaume Lessard (iD01t Productions, Longueuil, Québec). Records state their scope and limits, and most ship with the data, scripts and SHA-256 checksums needed to reproduce them.
Highlights
- [[832, 10, 15]], machine-checked. The genus5 GB CLEAN quantum LDPC code has 832 physical qubits, 10 logical qubits and minimum distance exactly 15. The full result, lower bound included, is proved in Coq 8.18 with no axioms, and cross-checked in Lean 4.19 and Isabelle2025-2. Formal proofs · Paper · Verification bundle
- Fold-and-lift. An exact method for certifying the minimum distance of quasi-cyclic CSS codes whose circulant size carries a large power of two. For the [[832, 10]] code the search takes about one second per sector on a single CPU core. Paper
- LCL-832 as a Metastable Effective Theory. Every theorem, proposition, lemma and corollary of version 4.0 of the note is machine-checked in Coq 8.18, using only the three standard axioms of Coq's real numbers. Formal proofs · Original note
- QECTOR Decoder v3. A decoding library for Python with a compiled Rust core: Union-Find, exact MWPM (Blossom), BP-OSD and Relay-BP, CPU and GPU batch decoding, with Stim and Sinter integration. Every correction it returns reproduces the syndrome, H c = s (mod 2). PyPI · Reference manual · Verification report · Benchmark datasets
- QECTOR Mega. Decoder certification and benchmark reports for surface, qLDPC and bivariate bicycle codes. 4.5.0 benchmark report · 4.0.2 certification
How results are labelled
Each record says what kind of evidence it carries: machine-checked proof, computer-assisted proof, measured benchmark, or developer-run certification. Verification was run by the author unless a record says otherwise; independent rebuilds and reviews are welcome. Some source code and data are kept in restricted records for IP protection, and their SHA-256 digests are published.
Licensing
Papers, reports and data: CC BY 4.0 unless a record states otherwise. QECTOR software: source-available under the PolyForm Noncommercial License 1.0.0, free for academic, educational and non-commercial research; commercial plans at qector.store/pricing.
Guillaume Lessard
iD01t Productions · Longueuil, Québec
ORCID: 0009-0000-3465-3753 · qector.store