54 Cor 3: Distance-Balanced Family of Quantum Codes
For a valid prime \(q\), the classical code length is \(n_c = q^2\).
For a valid prime \(q\), the balanced code length is \(N = N_0 \cdot n_c = \operatorname {codeLength}(vp) \cdot q^2\), where \(N_0 = \operatorname {codeLength}(vp)\) is the subsystem code length from Theorem 15.
For a valid prime \(vp\), a balanced code datum is a structure bundling:
row counts \(r_X, r_Z \in \mathbb {N}\) for the X- and Z-type parity checks,
a CSS code \(\mathcal{C}\) of block length \(N = \operatorname {balancedCodeLength}(vp)\),
a weight bound \(w \in \mathbb {N}\) such that the X-parity check matrix \(H_X\) and the transposed Z-parity check matrix \(H_{ZT}\) both have bounded row and column weight at most \(w\) (LDPC property),
a lower bound on logical qubits: \(K \geq K_0 \cdot \lfloor n_c/2 \rfloor + 1\), where \(K_0\) is the logical qubit count of the subsystem code from Theorem 15 and \(n_c = q^2\) is the classical code length,
a lower bound on X-distance: \(D_X \geq D_{X,0} \cdot \lfloor n_c / 10 \rfloor \), where \(D_{X,0}\) is the X-distance of the subsystem code,
an upper bound on logical qubits: \(K \leq K_0 \cdot n_c\),
a lower bound on Z-distance: \(D_Z \geq D_{Z,0}\), where \(D_{Z,0}\) is the Z-distance of the subsystem code.
red[UNPROVEN AXIOM]
For every valid prime \(vp\), there exists a balanced code datum \(\operatorname {BalancedCodeData}(vp)\).
That is, given the subsystem CSS code from Theorem 15 (with parameters \([[N_0, K_0, D_{X,0}, D_{Z,0}]]\)) and the Gilbert–Varshamov classical code of length \(n_c = q^2\) (Theorem 10), the Evra–Kaufman–Zemor distance balancing procedure (EKZ22, Theorem 1) produces a (non-subsystem) CSS code with:
Block length \(N = N_0 \cdot n_c\),
Logical qubits \(K \geq K_0 \cdot k_c\) where \(k_c \geq n_c/2\),
X-distance \(D_X \geq D_{X,0} \cdot d_c\) where \(d_c \geq n_c/10\),
Z-distance \(D_Z \geq D_{Z,0}\),
LDPC property preserved (row and column weights bounded by a constant).
Note: This is stated as an axiom because the full proof was not completed in the formalization. The EKZ result is from: Evra, Kaufman, Zemor, “Decodable quantum LDPC codes beyond the \(\sqrt{n}\) distance barrier using high-dimensional expanders”, FOCS 2022.
There exists a valid prime \(vp\) such that \(\operatorname {BalancedCodeData}(vp)\) is nonempty. In other words, the EKZ axiom’s hypothesis is satisfiable.
From infinitelyManyValidPrimes applied at bound \(0\), we obtain a valid prime \(vp\). Then the axiom ekz_distance_balancing applied to \(vp\) yields an element of \(\operatorname {BalancedCodeData}(vp)\), establishing nonemptiness.
For a valid prime \(vp\), \(\operatorname {distanceBalancing}(vp)\) is the balanced code datum obtained by applying the EKZ distance balancing axiom: \(\operatorname {distanceBalancing}(vp) := \operatorname {ekz_distance_balancing}(vp)\).
For any valid prime \(vp\), we have \(\lfloor n_c / 2 \rfloor + 1 \geq 1\), where \(n_c = \operatorname {classicalCodeLength}(vp) = q^2\).
This follows immediately by integer arithmetic (omega).
For any valid prime \(vp\) (so \(q \geq 41\)), the real-valued inequality
holds, where \(n_c = q^2\).
Unfolding \(\operatorname {classicalCodeLength}\) gives \(n_c = q^2\). Casting to \(\mathbb {R}\) via push_cast and using the fact that \(q^2 \geq 0\) by positivity, the bound \(\lfloor q^2/2 \rfloor + 1 \geq q^2/4\) follows from linear arithmetic (linarith).
For any valid prime \(vp\), the real-valued inequality
holds, where \(n_c = q^2\).
Unfolding \(\operatorname {classicalCodeLength}\) gives \(n_c = q^2\). Casting to \(\mathbb {R}\) and using \(q^2 \geq 0\), the bound follows from linear arithmetic.
For any valid prime \(vp\),
This holds by reflexivity of the definition.
There exists a constant \(c {\gt} 0\) such that for every valid prime \(vp\),
where \(N = \operatorname {balancedCodeLength}(vp)\). Concretely, \(c = \frac{3 \cdot 201}{2}\) works.
We take \(c = 3 \cdot 201 / 2\), which is positive by positivity. For any valid prime \(vp\), we simplify \(\operatorname {balancedCodeLength}(vp) = \operatorname {codeLength}(vp) \cdot q^2\) and cast to \(\mathbb {R}\). We have \(q \geq 41\) from validPrime_q_ge. Using the explicit formula \(\operatorname {codeLength}(vp) = 3 \cdot q \cdot (q^2 - 1)\) (from codeLength_eq_real), and the bounds \(q^2 - 1 \geq q^2/2\) (since \(q \geq 41\) implies \(q^2 \geq 41^2\)), the result follows by nonlinear arithmetic (nlinarith).
There exists a constant \(C {\gt} 0\) such that for every valid prime \(vp\),
where \(N = \operatorname {balancedCodeLength}(vp)\). Concretely, \(C = 3 \cdot 201\) works.
We take \(C = 3 \cdot 201\), which is positive by positivity. For any valid prime \(vp\), we simplify \(N = \operatorname {codeLength}(vp) \cdot q^2\) and cast to \(\mathbb {R}\). Using the formula \(\operatorname {codeLength}(vp) = 3q(q^2-1)\) and the bound \(q^2 - 1 \leq q^2\), the result \(3q(q^2-1) \cdot q^2 \leq 3 \cdot 201 \cdot q^5\) follows by nonlinear arithmetic.
There exists a constant \(c {\gt} 0\) such that for every valid prime \(vp\),
where \(K\) is the number of logical qubits of \(\operatorname {distanceBalancing}(vp).\mathcal{C}\).
From lps_K_lower_bound, we obtain \(c_0 {\gt} 0\) such that \(K_0 \geq c_0 (q^2 - 1)\) for all valid primes. We take \(c = c_0/8\). For any valid prime \(vp\):
From the EKZ axiom (hK field of \(\operatorname {distanceBalancing}(vp)\)), we have \(K \geq K_0 \cdot (\lfloor n_c/2 \rfloor + 1)\).
From lps_K_lower_bound: \(K_0 \geq c_0(q^2 - 1)\).
From classicalK_lower: \(\lfloor n_c/2 \rfloor + 1 \geq q^2/4\).
Since \(q \geq 41\), we have \(q^2 - 1 \geq q^2/2\). Combining:
This chain of inequalities is verified by nlinarith and linarith.
There exists a constant \(C {\gt} 0\) such that for every valid prime \(vp\),
where \(K\) is the number of logical qubits of \(\operatorname {distanceBalancing}(vp).\mathcal{C}\).
From lps_K_upper_bound, we obtain \(C_0 {\gt} 0\) such that \(K_0 \leq C_0(q^2 - 1)\) for all valid primes. We take \(C = C_0\). For any valid prime \(vp\):
From the EKZ axiom (hK_upper field): \(K \leq K_0 \cdot n_c\).
From lps_K_upper_bound: \(K_0 \leq C_0(q^2 - 1)\).
By definition: \(n_c = q^2\).
Combining: \(K \leq K_0 \cdot q^2 \leq C_0(q^2-1) \cdot q^2 \leq C_0 q^4\), where the last step uses \(q^2 - 1 \leq q^2\), verified by nlinarith.
There exists a constant \(c {\gt} 0\) such that for every valid prime \(vp\),
where \(D_X\) is the X-distance of \(\operatorname {distanceBalancing}(vp).\mathcal{C}\).
From lps_DX_lower_bound, we obtain \(c_0 {\gt} 0\) such that \(D_{X,0} \geq c_0 \cdot q\) for all valid primes. We take \(c = c_0/20\). For any valid prime \(vp\):
From the EKZ axiom (hDX field): \(D_X \geq D_{X,0} \cdot \lfloor n_c/10 \rfloor \).
From lps_DX_lower_bound: \(D_{X,0} \geq c_0 q\).
From classicalD_lower: \(\lfloor n_c/10 \rfloor \geq q^2/20\).
Combining:
The chain is assembled by calc steps using linarith and exact casts.
There exists a constant \(c {\gt} 0\) such that for every valid prime \(vp\),
where \(D_Z\) is the Z-distance of \(\operatorname {distanceBalancing}(vp).\mathcal{C}\).
From lps_DZ_lower_bound, we obtain \(c_0 {\gt} 0\) such that \(D_{Z,0} \geq c_0 \cdot q(q^2-1)\) for all valid primes. We take \(c = c_0/2\). For any valid prime \(vp\):
From the EKZ axiom (hDZ field): \(D_Z \geq D_{Z,0}\).
From lps_DZ_lower_bound: \(D_{Z,0} \geq c_0 q(q^2-1)\).
Since \(q \geq 41\), we have \(q^2 \geq 41^2\), hence \(q^2 - 1 \geq q^2/2\).
Therefore \(q(q^2-1) \geq q \cdot q^2/2 = q^3/2\) (verified by nlinarith), and:
The family is infinite: for every \(M \in \mathbb {N}\), there exists a valid prime \(vp\) such that \(\operatorname {balancedCodeLength}(vp) {\gt} M\).
Let \(M \in \mathbb {N}\) be arbitrary. From balancedN_lower, we obtain \(c {\gt} 0\) such that \(c \cdot q^5 \leq N\) for all valid primes. Applying infinitelyManyValidPrimes at the bound \(\lceil (M+1)/c \rceil + 1\), we obtain a valid prime \(vp\) with \(q {\gt} \lceil (M+1)/c \rceil + 1\). Since \(\lceil (M+1)/c \rceil \geq (M+1)/c\), we have \(q {\gt} (M+1)/c\), i.e., \(cq {\gt} M+1\). Since \(q \geq 41 \geq 1\), we get \(q^5 \geq q^1 \geq q\), hence \(c q^5 \geq cq {\gt} M\). Therefore \(N \geq c q^5 {\gt} M\), establishing \(N {\gt} M\) (cast back to \(\mathbb {N}\)).
There exists an explicit construction of an infinite family of \([[N, K, D]]\) LDPC quantum CSS codes such that:
(LDPC existence) For each valid prime \(vp\), there exists an LDPC CSS code of block length \(N = \operatorname {balancedCodeLength}(vp)\) with parity check matrices of bounded weight.
(Infinitely many) For every \(M \in \mathbb {N}\), there exists a valid prime \(vp\) with \(\operatorname {balancedCodeLength}(vp) {\gt} M\).
(\(K \in \Theta (N^{4/5})\)) There exist constants \(0 {\lt} c \leq C\) such that for every valid prime \(vp\),
\[ c \cdot q^4 \; \leq \; K \; \leq \; C \cdot q^4, \]where \(K\) is the logical qubit count of the balanced code and \(N \in \Theta (q^5)\) gives \(q \in \Theta (N^{1/5})\).
(\(D \in \Omega (N^{3/5})\)) There exists a constant \(c {\gt} 0\) such that for every valid prime \(vp\),
\[ c \cdot q^3 \; \leq \; \min (D_X, D_Z), \]so \(D = \min (D_X, D_Z) \in \Omega (q^3) = \Omega (N^{3/5})\).
(\(N \in \Theta (q^5)\)) There exist constants \(0 {\lt} c \leq C\) such that for every valid prime \(vp\),
\[ c \cdot q^5 \; \leq \; N \; \leq \; C \cdot q^5. \]
orange[Uses unproven axiom: thm:DistanceBalancedFamily.ekz_distance_balancing (EKZ22, Theorem 1)]
We verify each part separately.
Part 1 (LDPC existence). For each valid prime \(vp\), let \(D = \operatorname {distanceBalancing}(vp)\). The fields \(D.r_X\), \(D.r_Z\), \(D.\mathcal{C}\), \(D.w\), \(D.\texttt{isLDPC\_ HX}\), and \(D.\texttt{isLDPC\_ HZT}\) directly provide the required LDPC CSS code.
Part 2 (Infinitely many). This is exactly the statement of balancedN_unbounded.
Part 3 (\(K \in \Theta (q^4)\)). From balancedK_lower, we obtain \(c {\gt} 0\) with \(c q^4 \leq K\) for all valid primes. From balancedK_upper, we obtain \(C {\gt} 0\) with \(K \leq C q^4\) for all valid primes. We then set \(c, C\) and verify \(c q^4 \leq K \leq C q^4\) pointwise.
Part 4 (\(D \in \Omega (q^3)\)). From balancedDX_lower, we obtain \(c_1 {\gt} 0\) with \(c_1 q^3 \leq D_X\). From balancedDZ_lower, we obtain \(c_2 {\gt} 0\) with \(c_2 q^3 \leq D_Z\). Setting \(c = \min (c_1, c_2) {\gt} 0\) (since \(c {\gt} 0\) iff \(c_1 {\gt} 0\) and \(c_2 {\gt} 0\)), we verify:
\(\min (c_1,c_2) q^3 \leq c_1 q^3 \leq D_X\), using \(\min (c_1,c_2) \leq c_1\) and \(q^3 \geq 0\).
\(\min (c_1,c_2) q^3 \leq c_2 q^3 \leq D_Z\), using \(\min (c_1,c_2) \leq c_2\) and \(q^3 \geq 0\).
Both bounds are verified by le_min_iff decomposition and calc.
Part 5 (\(N \in \Theta (q^5)\)). From balancedN_lower and balancedN_upper, we obtain constants \(c, C {\gt} 0\) with \(c q^5 \leq N \leq C q^5\) for all valid primes.