53 Thm 15: Explicit Family of Quantum Codes
A valid prime for the LPS construction with \(p = 401\) is a structure consisting of:
A prime \(q \in \mathbb {N}\) with \(q\) odd, \(q \neq 401\), and \(q {\gt} 2\sqrt{401}\),
Elements \(x, y \in \mathbb {Z}/q\mathbb {Z}\) satisfying \(x^2 + y^2 + 1 = 0\).
The condition \(x^2 + y^2 + 1 = 0\) witnesses that \(-1\) is not a quadratic residue mod \(q\), i.e., the Legendre symbol \((p/q) = -1\).
For a valid prime \(q\), the code length is
This equals \(3|X_1|\) where \(|X_1| = \tfrac {s}{2} \cdot |\operatorname {PGL}(2,q)| = 201 \cdot q(q^2-1)\) is the number of edges of the LPS graph, obtained by the handshaking lemma for \(s\)-regular graphs with \(|X_0| = |\operatorname {PGL}(2,q)| = q(q^2-1)\) vertices and \(s = 402\).
The LDPC weight bound is \(w = 2s = 804\).
For a valid prime \(q\), the LPS code data is a structure consisting of:
The number of \(X\)-type check rows \(r_X \in \mathbb {N}\),
The number of \(Z\)-type check rows \(r_Z \in \mathbb {N}\),
A subsystem CSS code of length \(N = \operatorname {codeLength}(q)\).
For a valid prime \(q\), the LPS construction data is a structure consisting of:
The number of \(X\)-type check rows \(r_X \in \mathbb {N}\),
The number of \(Z\)-type check rows \(r_Z \in \mathbb {N}\),
A subsystem CSS code of length \(N = \operatorname {codeLength}(q)\),
A proof that the \(X\)-type parity check matrix \(H_X\) has bounded weight \(\leq 2s = 804\) (LDPC property),
A proof that the \(Z\)-type parity check matrix \(H_{ZT}\) has bounded weight \(\leq 2s = 804\) (LDPC property).
The bound \(2s = 804\) arises from the Kronecker product structure: the Tanner code differential has weight \(\leq s\) (from \(s\)-regularity) and the cycle graph differential has weight \(2\), giving total weight \(\leq 2s\) after the balanced product quotient.
red[UNPROVEN AXIOM]
For every valid prime \(q\), the balanced product \(C(X, L) \otimes _{\mathbb {Z}_q} C(C_q)\) yields a subsystem CSS code of length \(N = \operatorname {codeLength}(q)\), with the horizontal/vertical homology splitting providing the logical/gauge decomposition.
Note: This is stated as an axiom citing Panteleev–Kalachev [ , Def. 26 and Def. 29. The full formalization of the balanced product construction was not completed.
red[UNPROVEN AXIOM]
For every valid prime \(q\), the parity check matrices of the balanced product code have bounded weight:
Note: This is stated as an axiom citing Panteleev–Kalachev [ , §4.3, Step 8. The bound \(2s = 804\) follows from the Kronecker product structure.
red[UNPROVEN AXIOM]
For any \(M \in \mathbb {N}\), there exists a valid prime \(q {\gt} M\).
Note: This is stated as an axiom appealing to Dirichlet’s theorem on primes in arithmetic progressions (Dirichlet 1837) and quadratic reciprocity for the Legendre symbol condition. The required Dirichlet theorem infrastructure was not formalized from scratch.
red[UNPROVEN AXIOM]
There exists a constant \(c {\gt} 0\) such that for every valid prime \(q\), letting \(D\) denote the balanced product construction data,
where \(K = \operatorname {logicalQubits}(D.\operatorname {code})\) is the number of logical qubits.
Note: This is stated as an axiom citing Sipser–Spielman 1996 (Theorem 7 in this work). Since \(k_L {\gt} s/2 = 201\) and \(|X_1|/\ell = 201(q^2-1)\), one obtains \(K \geq c(q^2-1)\) for a constant \(c {\gt} 0\).
red[UNPROVEN AXIOM]
There exists a constant \(C {\gt} 0\) such that for every valid prime \(q\), letting \(D\) denote the balanced product construction data,
where \(K = \operatorname {logicalQubits}(D.\operatorname {code})\).
Note: This is stated as an axiom appealing to the Rank–Nullity Theorem (Axler, Linear Algebra Done Right, Thm. 3.22). The total chain module \(\operatorname {Tot}_1\) of the balanced product has dimension \(\in \Theta (q^3)\), giving \(K = \dim (H_1) \leq \dim (\operatorname {Tot}_1) \in O(q^2)\) after dividing by \(\ell = q\).
red[UNPROVEN AXIOM]
There exists a constant \(c {\gt} 0\) such that for every valid prime \(q\), letting \(D\) denote the balanced product construction data,
where \(D_Z = D.\operatorname {code}.\operatorname {dZ}\) is the \(Z\)-distance of the subsystem code.
Note: This is stated as an axiom citing Panteleev–Kalachev [ , Theorem 13 (homological distance bound). Since \(|X_1| = 201 \cdot q(q^2-1)\), the bound gives \(D_Z \geq c \cdot q(q^2-1)\) for a constant \(c {\gt} 0\) determined by the expansion parameters \(\alpha _{ho} = 10^{-3}\) and \(\beta _{ho} {\gt} 0\) from Theorem 8.
red[UNPROVEN AXIOM]
There exists a constant \(c {\gt} 0\) such that for every valid prime \(q\), letting \(D\) denote the balanced product construction data,
where \(D_X = D.\operatorname {code}.\operatorname {dX}\) is the \(X\)-distance of the subsystem code.
Note: This is stated as an axiom citing Panteleev–Kalachev [ , Theorem 14 (cohomological distance bound). Using \(|X_0|s = 2|X_1| \in \Theta (q^3)\) and \(\ell = q\), the minimum over horizontal and vertical contributions is \(\Theta (q)\). Expansion parameters \(\alpha _{co} = 10^{-5}\) and \(\beta _{co} {\gt} 0\) come from Theorem 9.
orange[Uses unproven axioms: thm:ExplicitFamilyQuantumCodes.balanced_product_code, thm:ExplicitFamilyQuantumCodes.balanced_product_ldpc, thm:ExplicitFamilyQuantumCodes.infinitelyManyValidPrimes, thm:ExplicitFamilyQuantumCodes.lps_K_lower_bound, thm:ExplicitFamilyQuantumCodes.lps_K_upper_bound, thm:ExplicitFamilyQuantumCodes.lps_DZ_lower_bound, thm:ExplicitFamilyQuantumCodes.lps_DX_lower_bound]
There exists an explicit construction of an infinite family of \([\! [N, K, D_X, D_Z]\! ]\) LDPC subsystem CSS quantum codes satisfying the following simultaneously:
(Code existence) For each valid prime \(q\), there exist row counts \(r_X, r_Z \in \mathbb {N}\) and a subsystem CSS code of length \(N = 3 \cdot 201 \cdot q(q^2-1)\) whose parity check matrices \(H_X\) and \(H_{ZT}\) both have bounded weight \(\leq 804\).
(Infinite family) For any \(M \in \mathbb {N}\), there exists a valid prime \(q\) with \(N {\gt} M\).
(Logical qubit count) There exist constants \(0 {\lt} c \leq C\) such that for every valid prime \(q\),
\[ c(q^2 - 1) \leq K \leq C(q^2 - 1), \]i.e., \(K \in \Theta (q^2) = \Theta (N^{2/3})\).
(X-distance) There exists a constant \(c {\gt} 0\) such that for every valid prime \(q\),
\[ D_X \geq c \cdot q = \Omega (N^{1/3}). \](Z-distance) There exist constants \(0 {\lt} c \leq C\) such that for every valid prime \(q\),
\[ c \cdot N \leq D_Z \leq C \cdot N, \]i.e., \(D_Z \in \Theta (N)\).
orange[Uses unproven axioms as listed above.]
We prove each part in turn using the refine tactic to split the conjunction.
Part 1 (LDPC subsystem CSS code). Let \(q\) be any valid prime. Define \(D = \operatorname {balanced_product_construction}(q)\), which packages the axioms balanced_product_code and balanced_product_ldpc into a single structure. We extract \(D.r_X\), \(D.r_Z\), \(D.\operatorname {code}\), \(D.\operatorname {isLDPC_HX}\), and \(D.\operatorname {isLDPC_HZT}\) to satisfy Part 1.
Part 2 (Infinite family). This is exactly the content of the lemma codeLength_unbounded, which is proved as follows. Let \(M \in \mathbb {N}\) be arbitrary. By the axiom infinitelyManyValidPrimes, there exists a valid prime \(q {\gt} M\). Since \(q \geq 41\) (proved from the lower bound \(q {\gt} 2\sqrt{401} \geq 40\)), and \(q^2 - 1 \geq 1\), we compute:
Part 3 (\(K \in \Theta (q^2)\)). From the axiom lps_K_lower_bound, obtain \(c {\gt} 0\) and the bound \(c(q^2-1) \leq K\) for all valid primes. From the axiom lps_K_upper_bound, obtain \(C {\gt} 0\) and the bound \(K \leq C(q^2-1)\) for all valid primes. Taking both together gives Part 3.
Part 4 (\(D_X \in \Omega (q)\)). This follows directly from the axiom lps_DX_lower_bound, which provides \(c {\gt} 0\) with \(D_X \geq c \cdot q\) for all valid primes.
Part 5 (\(D_Z \in \Theta (N)\)). From the axiom lps_DZ_lower_bound, obtain \(c {\gt} 0\) and the bound \(c \cdot q(q^2-1) \leq D_Z\) for all valid primes. We set \(c' = c/(3 \cdot 201)\) and \(C' = 1\).
For the lower bound: since \(N = 3 \cdot 201 \cdot q(q^2-1)\) (the lemma codeLength_eq_real), we compute
This is verified by simplifying with field_simp and applying linear arithmetic.
For the upper bound: \(D_Z \leq N\) is the content of the lemma dZ_le_codeLength. Indeed, \(D_Z\) is the infimum of a set of Hamming weights of nonzero logical \(Z\) codewords; if this set is empty, then \(D_Z = 0 \leq N\); otherwise any element \(w\) of the set satisfies \(w = \operatorname {hammingWeight}(x) \leq n = N\) (by SipserSpielman.hammingWeight_le_card), so \(D_Z \leq w \leq N\). Hence \(D_Z \leq 1 \cdot N\).
[Paper Corrections] redErrata. The following errors were identified in the original paper and corrected in this formalization:
In Corollary (cor:distanceboundssybsystemcode), the \(D_X\) formula has second term \(\alpha _{\mathrm{co}}|X_1|/2\) but should be \(\alpha _{\mathrm{co}} \cdot \beta _{\mathrm{co}} \cdot |X_1|/2\), derived from Theorem distco Case 1: \(|X_0|s \cdot \alpha _{\mathrm{co}} \cdot \beta _{\mathrm{co}}/4 = 2|X_1| \cdot \alpha _{\mathrm{co}} \cdot \beta _{\mathrm{co}}/4 = \alpha _{\mathrm{co}} \cdot \beta _{\mathrm{co}} \cdot |X_1|/2\). The \(\beta _{\mathrm{co}}\) factor was dropped. This is a typo that does not affect the asymptotic result since the minimum is dominated by the \(\ell \cdot \alpha _{\mathrm{co}} \cdot \beta _{\mathrm{co}}/(4s) = \Theta (q)\) terms, not the \(\Theta (q^3)\) terms.