High-Rate Quantum Codes with Proven Distance and Low-Weight Measurements
Kishor Bharti, Tobias Haug, Runzhou Tao, Kevin Ye
quant-ph
Oct 2, 2026 · v1
TL;DR
Formally verifies in Lean the subsystem-code construction on rectangular grids and its dressed and bare distances, with Lean snippets explained throughout.
Abstract
We study a family of quantum subsystem codes defined on rectangular coordinate grids of any dimension, with even side lengths of at least four. The directly measured operators act along coordinate lines. For every member of the family, we derive the number of protected logical qubits and prove its dressed distance without a numerical search. To illustrate the resulting design choices, we impose a budget of at most 10,000 data qubits and determine the complete tradeoff between encoding rate and measurement weight within this family at distances 16, 32, and 64. At distance 16, one code protects 4,096 logical qubits among 10,000 data qubits using weight-ten measurements. At distances 32 and 64, codes with 7,776 and 9,216 data qubits protect 1,024 and 256 logical qubits, respectively, using weight-six measurements. We include and explain Lean code snippets throughout the paper to guide readers through the formal verification of our subsystem-code construction and its dressed and bare distances.
Problem
Quantum memories need codes that combine a high encoding rate, a large distance, and low-weight measured operators. For subsystem codes, the distance must be taken over dressed logical operators, which makes it hard to prove.
Approach
The authors define the subsystem codes RLG(q_1,...,q_L) on even rectangular grids with side lengths at least four, using full coordinate-line X and Z gauge operators. Tensor-product linear algebra over F_2 gives the gauge and stabilizer ranks and the number of logical qubits. A functional-labelling argument proves the dressed distance 2^L. The construction and its dressed and bare distances are formally verified in Lean, and code snippets are explained throughout the paper.
Results
For every member of the family, K = ∏(q_i−2) and D = 2^L, and the minimum stabilizer weight is 2^{L−1}·min q_i. Under a budget of 10,000 data qubits, the complete rate versus measurement-weight frontier is determined at distances 16, 32 and 64, including [[10000,4096,974,16]], [[7776,1024,2550,32]] and [[9216,256,5422,64]] codes.
| Sides | N | K | g | D | max weight |
|---|
| 10^4 | 10000 | 4096 | 974 | 16 | 10 |
| 6^5 | 7776 | 1024 | 2550 | 32 | 6 |
| 4^4 6^2 | 9216 | 256 | 5422 | 64 | 6 |
Maximum-rate codes under N ≤ 10,000
