Quantum code parameters, checkable by a certificate of provable size

Technical Summary: Quantum Code Parameters Checkable by a Certificate of Provable Size

Problem Statement
Quantum error-correcting codes are characterized by three parameters: the number of physical qubits ($n$), logical qubits ($k$), and the code distance ($d$). While $n$ and $k$ are determined by linear algebra (specifically, the rank of parity-check matrices), $d$ is defined as the minimum weight of a logical operator. Determining $d$ involves finding the lightest vector in the kernel of a check matrix that is not in the row space of the other check matrix. This is an optimization problem over an exponentially large set ($2^n$).

Currently, $d$ is typically determined by external solvers (e.g., mixed-integer programming or SAT solvers). These solvers provide a numerical answer but no certificate of correctness that can be independently verified within a trusted logical framework. Consequently, threshold claims in quantum error correction often rely on unverified solver outputs. The paper addresses the open question of whether code parameters can be checked uniformly across different codes using a certificate of provable size, where the verification is performed entirely within the kernel of a proof assistant.

Methodology
The authors propose a verification framework implemented in the Lean proof assistant. The core strategy is to shift the unit of verification from the code itself to a certificate—a short object whose correctness is decided by computation within Lean's trusted kernel. The methodology relies on three primary mechanisms:

1. Row Reduction and Rank Certification:
   The rank of parity-check matrices ($H_X$ and $H_Z$) is certified by performing Gaussian elimination (row reduction) directly inside the kernel. To handle scalability, the authors utilize an "append-only" echelon form routine. Unlike standard back-substitution, which scales poorly ($O(n^3)$ or worse for wide matrices), the append-only variant maintains a weaker invariant sufficient for rank and membership testing, allowing the kernel to process wider matrices efficiently.

2. Dual Witnesses for Upper Bounds:
   To certify that a specific vector $v$ is a logical operator (i.e., $v \in \ker H$ and $v \notin \text{rowspace } H$), the method replaces expensive row-space membership checks with a dual witness. A witness vector $w$ is provided such that $Hw = 0$ (it is in the kernel) and $w \cdot v = 1$ (it pairs non-trivially with $v$). By linear algebra, if $w$ is orthogonal to the entire row space but not to $v$, then $v$ cannot be in the row space. This reduces the verification cost to a single matrix-vector product and one inner product, avoiding full row reduction.

3. Certificate Forms for Lower Bounds:

   • Enumeration Route: For codes where $d$ is small relative to $n$, the lower bound is certified by enumerating all vectors with weight less than $d$. The certificate is the empty set of undetectable logical operators found in this list. The size of this list is $\sum_{j<d} \binom{n}{j}$, which is polynomial in $n$ for fixed $d$, rather than exponential ($2^n$).
   • Symbolic/Structured Route: For product families (e.g., hypergraph product codes), the lower bound is proved symbolically using a "cleaning argument." This argument shows that any low-weight logical operator can be reduced to a stabilizer. This proof is established once for the family parameters, and specific instances are merely instantiations of this theorem, avoiding candidate generation entirely.

Key Contributions

• Uniform Verification: The paper demonstrates that code parameters can be verified uniformly across different code families using certificates, rather than relying on solver outputs.
• Kernel-Only Verification: The entire verification process, including the reduction of the problem and the checking of certificates, occurs within the Lean kernel. No external solvers or untrusted compilers are part of the trusted base; only the three standard axioms of Lean's logic are used.
• Scalability via Certificate Design: By changing the certificate form (e.g., from row reduction to dual witnesses, or from enumeration to symbolic proofs), the authors achieve significant performance gains. For example, checking a membership assertion for an 18-qubit toric code drops from 42 seconds to 9 seconds when switching from row reduction to a dual witness.
• Certificate Size Theorem: The authors prove that the size of the enumeration certificate is a polynomial in $n$ for fixed $d$, specifically $\sum_{j<d} \binom{n}{j}$. This establishes that the certificate is strictly smaller than the full search space.

Results
The authors verified eleven code families and thirty-nine parameter sets, with the largest instance reaching $n = 1872$ physical qubits (with $d=7$).

• Instances: The dataset includes classical codes (Hamming, Repetition), CSS codes (Steane, Shor, Bivariate Bicycle codes like $[[144, 12, 12]]$), and hypergraph product codes.
• Performance: The "append-only" row reduction routine allowed the kernel to verify the rank and distance of the gauged bivariate bicycle code $[[24, 3, 4]]$ in seconds and minutes, respectively, whereas standard reduction failed to terminate within practical time limits.
• Search Pipeline: A discovery pipeline was run on 44 seed graphs, generating 990 pairs. It admitted 903 candidates and closed the distance bounds for 259 of them (and 891 with a relaxed criterion). The pipeline utilized symbolic theorems for path and cyclic families to avoid enumeration for large instances.
• Comparison: The paper notes that the search pipeline did not discover codes with better parameters than existing published codes; its value lies in the checkability of the parameters, not in parameter optimization.

Significance and Claims
The paper claims to have solved the problem of making quantum code parameters "checkable rather than believed."

• Trust: The verification relies solely on the Lean kernel and three standard axioms, removing the need to trust external solver outputs.
• Efficiency: The shift to certificate-based verification makes the cost of checking parameters manageable, even for codes where the underlying search space is exponential.
• Generality: The approach is not limited to specific code families; it applies to any code specified by parity checks. The symbolic route extends this to large product families.
• Limitations: The authors explicitly state what is not delivered:
  • The $[[144, 12, 12]]$ code's lower bound is "transported" from an independent per-family formalization rather than proved from scratch in this work.
  • Full step-by-step replay of the solver's proof for the $[[144, 12, 12]]$ instance is currently out of reach due to time constraints (estimated at 37–44 days of kernel time).
  • The method assumes the non-triviality of the kernels of the seed matrices; if a kernel is trivial, the distance bound may fail.
  • The search pipeline does not claim to find new optimal codes, but rather to certify existing candidates.

In conclusion, the work establishes a framework where the distance of a quantum code is no longer a black-box result from a solver but a theorem with a verifiable, polynomial-sized certificate, fundamentally changing the basis of threshold claims in quantum error correction.