Documentation

MerLeanBpqc.Theorems.Cor_3_DistanceBalancedFamily

Corollary 3: Distance-Balanced Family of Quantum Codes #

There exists an explicit construction of a family of [[N, K, D]] LDPC quantum codes with K ∈ Θ(N^{4/5}) and D ∈ Ω(N^{3/5}).

Construction #

  1. Start with the [[N₀, K₀, D_{X,0}, D_{Z,0}]] LDPC subsystem CSS codes from Thm_15 with K₀ ∈ Θ(N₀^{2/3}), D_{X,0} ∈ Ω(N₀^{1/3}), D_{Z,0} ∈ Θ(N₀).
  2. Choose classical codes of length n_c ∈ Θ(N₀^{2/3}) via Gilbert–Varshamov (Thm_10) with k_c ∈ Θ(n_c) and d_c ∈ Θ(n_c).
  3. Apply the distance balancing procedure of Evra–Kaufman–Zemor [EKZ, Thm 1], producing a CSS code with N = N₀ · n_c, K = K₀ · k_c, D_X ≥ D_{X,0} · d_c, D_Z ≥ D_{Z,0}.
  4. Compute: N ∈ Θ(N₀^{5/3}), K ∈ Θ(N₀^{4/3}) = Θ(N^{4/5}), D ∈ Ω(N₀) = Ω(N^{3/5}).

Main Results #

Distance-Balanced Parameters #

The distance-balanced code length is N = N₀ · n_c where N₀ = codeLength vp and n_c = q² is the classical code length.

The classical code length n_c = q², which is in Θ(N₀^{2/3}).

Equations
Instances For

    EKZ Distance Balancing Axiom #

    The distance balancing procedure of Evra–Kaufman–Zemor [EKZ22] takes a subsystem CSS code and a classical code, and produces a (non-subsystem) CSS code with balanced distances. We axiomatize this as a single well-known external theorem.

    The output of the EKZ distance balancing procedure for a valid prime q. This bundles the CSS code produced by the procedure together with its LDPC property and the parameter bounds guaranteed by [EKZ22, Theorem 1].

    Instances For

      Evra–Kaufman–Zemor Distance Balancing ([EKZ22, Theorem 1]; Evra, Kaufman, Zemor, "Decodable quantum LDPC codes beyond the √n distance barrier using high-dimensional expanders", FOCS 2022).

      Given the subsystem CSS code from Theorem 15 (with parameters [[N₀, K₀, D_{X,0}, D_{Z,0}]]) and a classical [n_c, k_c, d_c]-code from Gilbert–Varshamov (Theorem 10), the EKZ distance balancing procedure produces a (non-subsystem) CSS code with:

      • Block length N = N₀ · n_c
      • Logical qubits K ≥ K₀ · k_c
      • X-distance D_X ≥ D_{X,0} · d_c
      • Z-distance D_Z ≥ D_{Z,0}
      • LDPC property preserved (weight bounded by a constant).

      Satisfiability witness: the EKZ axiom's premise (a valid prime) is satisfiable.

      Arithmetic Helper Lemmas #

      For a valid prime (q ≥ 41), q² / 2 + 1 ≥ q² / 4.

      For a valid prime (q ≥ 41), q² / 10 ≥ q² / 20.

      N Bounds: N ∈ Θ(q⁵) #

      The balanced code length N = codeLength(vp) · q² satisfies N ∈ Θ(q⁵) since codeLength(vp) ∈ Θ(q³).

      N lower bound: N = codeLength · q² ≥ c · q⁵ for a constant c > 0.

      N upper bound: N = codeLength · q² ≤ C · q⁵ for a constant C > 0.

      K Bounds: K ∈ Θ(q⁴) #

      The logical qubit count K of the balanced code satisfies K ∈ Θ(q⁴). The lower bound uses K ≥ K₀ · k_c from the EKZ axiom, combined with K₀ ∈ Θ(q²) from Thm_15 and k_c ∈ Θ(q²) from GV.

      K lower bound: K ≥ c · q⁴ for a constant c > 0.

      K upper bound: K ≤ C · q⁴ for a constant C > 0. Uses hK_upper: K ≤ K₀ · n_c from the EKZ axiom, combined with K₀ ≤ C₀(q²-1) from Thm_15 and n_c = q².

      Distance Bounds: D_X, D_Z ∈ Ω(q³) #

      D_X lower bound: DX ≥ c · q³ for a constant c > 0.

      D_Z lower bound: DZ ≥ c · q³ for a constant c > 0.

      N Unbounded #

      The family is infinite: for any M, there exists a valid prime with the balanced code length exceeding M.

      Main Theorem #

      theorem DistanceBalancedFamily.distanceBalancedFamily :
      (∀ (vp : ExplicitFamilyQuantumCodes.ValidPrime), ∃ (rX : ) (rZ : ) (code : CSSCode (balancedCodeLength vp) rX rZ) (w : ), HasBoundedWeight code.HX w HasBoundedWeight code.HZT w) (∀ (M : ), ∃ (vp : ExplicitFamilyQuantumCodes.ValidPrime), balancedCodeLength vp > M) (∃ (c : ) (C : ), 0 < c 0 < C ∀ (vp : ExplicitFamilyQuantumCodes.ValidPrime), c * vp.q ^ 4 (distanceBalancing vp).code.logicalQubits (distanceBalancing vp).code.logicalQubits C * vp.q ^ 4) (∃ (c : ), 0 < c ∀ (vp : ExplicitFamilyQuantumCodes.ValidPrime), c * vp.q ^ 3 min (distanceBalancing vp).code.dX (distanceBalancing vp).code.dZ) ∃ (c : ) (C : ), 0 < c 0 < C ∀ (vp : ExplicitFamilyQuantumCodes.ValidPrime), c * vp.q ^ 5 (balancedCodeLength vp) (balancedCodeLength vp) C * vp.q ^ 5

      Corollary 3: Distance-Balanced Family of Quantum Codes.

      There exists an explicit construction of a family of [[N, K, D]] LDPC quantum codes (Def_5) with K ∈ Θ(N^{4/5}) and D = min(D_X, D_Z) ∈ Ω(N^{3/5}).

      The proof combines Theorem 15 (explicit family with unbalanced distances) with the distance balancing procedure of Evra–Kaufman–Zemor [EKZ22, Theorem 1].

      The balanced code for each valid prime vp is (distanceBalancing vp).code, a CSS code of length N = balancedCodeLength vp. Since N ∈ Θ(q⁵), we have q ∈ Θ(N^{1/5}), giving K ∈ Θ(q⁴) = Θ(N^{4/5}) and D ∈ Ω(q³) = Ω(N^{3/5}).