Theorem 15: Explicit Family of Quantum Codes #
There exists an explicit construction of a family of [[N, K, D_X, D_Z]] LDPC subsystem
CSS quantum codes which encode K ∈ Θ(N^{2/3}) logical qubits, with X-distance
D_X ∈ Ω(N^{1/3}) and Z-distance D_Z ∈ Θ(N).
Construction #
- Base graph: LPS expanders
X_{p,q}onPGL(2,q)withp = 401,q → ∞ - Group: unipotent subgroup
H = ℤ_q ⊂ PGL(2,q)(Def_30) - Cycle graph:
C_qwithℓ = q - Local code: Gilbert–Varshamov code with
δ = 0.1,s = 402(Thm_10) - Code: balanced product
C(X,L) ⊗_{ℤ_q} C(C_q)(Def_26, Def_29)
Formalization Approach #
The theorem is stated in terms of the subsystem CSS code parameters (Def_6):
N = code length, K = SubsystemCSSCode.logicalQubits = dim H₀^L,
D_X = SubsystemCSSCode.dX, D_Z = SubsystemCSSCode.dZ.
The deep algebraic facts are decomposed into individual axioms, each citing exactly one well-known mathematical result:
balanced_product_code— Balanced product yields subsystem CSS code ([PK22], Def_26 + Def_29)balanced_product_ldpc— LDPC property of balanced product codes ([PK22], §4.3)infinitelyManyValidPrimes— Dirichlet's theorem on primes in arithmetic progressionslps_K_lower_bound— Logical qubit lower bound (Sipser–Spielman 1996, Thm_7)lps_K_upper_bound— Logical qubit upper bound (Rank–Nullity Theorem)lps_DZ_lower_bound— Z-distance lower bound ([PK22], Thm_13)lps_DX_lower_bound— X-distance lower bound ([PK22], Thm_14)
Main Results #
codeLength— N = 3 · 201 · q(q² - 1) as a function of valid prime qLPSCodeData— code data (subsystem CSS code) for each valid primeLPSConstructionData— code data + LDPC property for each valid primebalanced_product_construction— combines code + LDPC axiomsexplicitFamilyQuantumCodes— main theorem combining all axioms
Construction Constants #
The prime p = 401 used in the LPS construction.
Equations
Instances For
The regularity s = p + 1 = 402.
Equations
Instances For
Valid Prime Indices #
Key Arithmetic Facts #
√401 < 201/10 since 401 < 40401/100 = (201/10)².
For a valid prime, q ≥ 41.
For a valid prime, q² - 1 ≥ 1 in ℕ.
Code Length #
The code length N = 3 · 201 · q(q² - 1) as a function of a valid prime q.
This equals 3|X₁| where |X₁| = (s/2) · |PGL(2,q)| = 201 · q(q² - 1)
is the number of edges of the LPS graph (by the handshaking lemma for
s-regular graphs with |X₀| = |PGL(2,q)| = q(q² - 1) vertices).
Instances For
The weight bound w = 2 · s = 804 for the LDPC property.
Instances For
LPS Construction Data #
The construction data bundles a subsystem CSS code (Def_6) of length N = codeLength vp
together with its LDPC property. The code is the horizontal subsystem balanced product
code (Def_29), which uses:
- LPS expander
X_{401,q}onPGL(2,q)(Thm_11, Def_20, Def_21) - Unipotent subgroup
H = ℤ_q(Def_30) - Gilbert–Varshamov local code with
δ = 0.1(Thm_10) - Balanced product
C(X,L) ⊗_{ℤ_q} C(C_q)(Def_26, Def_29)
The construction data for the LPS balanced product code at a single valid prime.
This bundles the subsystem CSS code (Def_6) of length N = codeLength vp together
with its LDPC property. The subsystem code has logical/gauge splitting from the
horizontal/vertical homology decomposition (Def_29).
- rX : ℕ
Number of X-type check rows.
- rZ : ℕ
Number of Z-type check rows.
- code : SubsystemCSSCode (codeLength vp) self.rX self.rZ
The subsystem CSS code of length
N = codeLength vp(Def_6). The logical subspaceHLcorresponds to horizontal homology H₁ʰ, and the gauge subspaceHGcorresponds to vertical homology H₁ᵛ. - isLDPC_HX : HasBoundedWeight self.code.HX ldpcWeightBound
The X-type parity check matrix has bounded weight (LDPC, Step 8). The bound
2s = 804comes from the Kronecker product structure: Tanner code differential has weight ≤ s (from s-regularity) and cycle graph differential has weight 2, giving total weight ≤ 2s after balanced product quotient. - isLDPC_HZT : HasBoundedWeight self.code.HZT ldpcWeightBound
The Z-type parity check matrix has bounded weight (LDPC, Step 8).
Instances For
Decomposed Axioms for Deep Algebraic Facts #
Each axiom below cites exactly one well-known mathematical result.
The code data for the LPS balanced product code (without LDPC property).
- rX : ℕ
Number of X-type check rows.
- rZ : ℕ
Number of Z-type check rows.
- code : SubsystemCSSCode (codeLength vp) self.rX self.rZ
The subsystem CSS code of length
N = codeLength vp(Def_6).
Instances For
Balanced Product Subsystem CSS Code (Panteleev–Kalachev [PK22], Def_26 + Def_29).
The balanced product C(X,L) ⊗_{ℤ_q} C(C_q) yields a subsystem CSS code (Def_6)
of length N = 3|X₁| = codeLength vp, with the horizontal/vertical homology
splitting providing the logical/gauge decomposition.
LDPC Property of Balanced Product Codes (Panteleev–Kalachev [PK22], §4.3, Step 8).
The parity check matrices of the balanced product code have bounded weight.
The bound 2s = 804 comes from the Kronecker product structure: the Tanner code
differential has weight ≤ s (from s-regularity) and the cycle graph differential
has weight 2, giving total weight ≤ 2s after balanced product quotient.
Combine the code construction and LDPC property into LPSConstructionData.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Sipser–Spielman Expander Code Distance (Sipser–Spielman 1996; Theorem 7).
The number of logical qubits K = dim H₁ʰ satisfies K ≥ (2k_L/s - 1)|X₁|/ℓ.
Since k_L > s/2 = 201, |X₁|/ℓ = 201(q²-1), we get K ≥ c(q²-1) for a
constant c > 0.
Dimension Upper Bound (Rank–Nullity Theorem; Axler, Linear Algebra Done Right, Thm 3.22).
The number of logical qubits is bounded above: K ≤ dim(Tot₁) ≤ C(q²-1)
for a constant C > 0. The total chain module Tot₁ of the balanced product
has dimension |X₁| + |X₀|·ℓ + |X₁| = 2|X₁| + |X₀|ℓ ∈ Θ(q³), so
K = dim(H₁) ≤ dim(Tot₁) ∈ O(q²) after dividing by ℓ = q.
Homological Distance Bound (Panteleev–Kalachev [PK22], Theorem 13).
The Z-distance of the subsystem code satisfies
D_Z ≥ |X₁| · min(α_ho/2, α_ho·β_ho/4) where α_ho = 10⁻³ and β_ho > 0
is a positive constant from Theorem 8 (ExpanderViolatedChecks).
Since |X₁| = 201·q(q²-1), this gives D_Z ≥ c · q(q²-1) for constant c > 0.
Cohomological Distance Bound (Panteleev–Kalachev [PK22], Theorem 14).
The X-distance of the subsystem code satisfies
D_X ≥ min(|X₀|s · min(α_co/2, α_co·β_co/4), ℓ · min(α_co/(4s), α_co·β_co/(4s))).
Using |X₀|s = 2|X₁| ∈ Θ(q³) and ℓ = q, the minimum is Θ(q).
The expansion parameters α_co = 10⁻⁵, β_co > 0 are from Theorem 9.
Satisfiability Witnesses for Axioms #
At least one valid prime exists (witness for infinitelyManyValidPrimes).
The construction data is satisfiable for any valid prime.
Arithmetic Helper Lemmas for the Main Theorem #
codeLength is positive for valid primes.
codeLength vp = 3 · 201 · q · (q² - 1) as a real number.
Infinite family: for any M, there exists a valid prime with codeLength vp > M.
D_Z is bounded above by N (distance cannot exceed code length).
Main Theorem #
Theorem 15: Explicit Family of Quantum Codes.
There exists an explicit construction of a family of [[N, K, D_X, D_Z]] LDPC subsystem
CSS quantum codes (Def_29, Def_5) which encode K ∈ Θ(N^{2/3}) logical qubits, with
X-distance D_X ∈ Ω(N^{1/3}) and Z-distance D_Z ∈ Θ(N).
The code length is N = codeLength vp = 3 · 201 · q(q² - 1) ∈ Θ(q³), and all
parameters are the subsystem CSS code parameters (Def_6):
K = code.logicalQubits = dim H₀^L, D_X = code.dX, D_Z = code.dZ.
The proof combines individually axiomatized results:
balanced_product_code(Def_26, Def_29) +balanced_product_ldpc(LDPC, §4.3)infinitelyManyValidPrimes(Dirichlet's theorem)lps_K_lower_bound(Sipser–Spielman, Thm_7)lps_K_upper_bound(Rank–Nullity Theorem)lps_DX_lower_bound(Thm_14, cohomological distance)lps_DZ_lower_bound(Thm_13, homological distance) with fully proved asymptotic analysis converting q-bounds to N-bounds.