Definition 4: CSS Code

A CSS (Calderbank-Shor-Steane) quantum code is defined by a chain complex (Def_1) of length two over 𝔽₂: C₁ →[H_Z^T] C₀ →[H_X] C_{-1} where H_X ∘ H_Z^T = 0.

The matrices H_X ∈ 𝔽₂^{r_X × n} and H_Z ∈ 𝔽₂^{r_Z × n} are the X-type and Z-type parity check matrices, so that C₀ = 𝔽₂^n, C_{-1} = 𝔽₂^{r_X}, and C₁ = 𝔽₂^{r_Z}.

Code Parameters

• n = dim C₀: number of physical qubits
• k = dim H₀(C) = dim(ker H_X / im H_Z^T): number of logical qubits
• d_X: minimum Hamming weight of a nontrivial element of H₀(C) = ker H_X / im H_Z^T
• d_Z: minimum Hamming weight of a nontrivial element of H⁰(C) = ker H_Z / im H_X^T
• d = min(d_X, d_Z): overall distance

Main Definitions

• CSSCode — a CSS quantum code specified by parity check matrices H_X and H_Z
• CSSCode.complex — the three-term chain complex C₁ →[H_Z^T] C₀ →[H_X] C_{-1}
• CSSCode.numQubits — the number of physical qubits n
• CSSCode.logicalQubits — the number of logical qubits k = dim H₀(C)
• CSSCode.dX — the X-distance
• CSSCode.dZ — the Z-distance
• CSSCode.distance — the overall distance d = min(d_X, d_Z)
• CSSCode.IsNKDCode — the property of being an [[n, k, d]]-code
• CSSCode.IsNKDXZCode — the property of being an [[n, k, d_X, d_Z]]-code

CSS Code Structure

structure CSSCode (n rX rZ : ℕ) : Type

A CSS (Calderbank-Shor-Steane) quantum code is defined by parity check matrices H_X : 𝔽₂^n → 𝔽₂^{r_X} and H_Z : 𝔽₂^n → 𝔽₂^{r_Z} satisfying the CSS condition H_X ∘ H_Z^T = 0. Here H_Z^T : 𝔽₂^{r_Z} → 𝔽₂^n is the transpose of H_Z, which serves as the differential from degree 1 to degree 0 in the chain complex C₁ →[H_Z^T] C₀ →[H_X] C_{-1}.

• HX : (Fin n → 𝔽₂) →ₗ[𝔽₂] Fin rX → 𝔽₂

  The X-type parity check matrix H_X : 𝔽₂^n → 𝔽₂^{r_X}.

• HZT : (Fin rZ → 𝔽₂) →ₗ[𝔽₂] Fin n → 𝔽₂

  The Z-type parity check matrix transpose H_Z^T : 𝔽₂^{r_Z} → 𝔽₂^n. This is the differential from degree 1 to degree 0 in the chain complex.

• css_condition : self.HX ∘ₗ self.HZT = 0

  The CSS condition: H_X ∘ H_Z^T = 0, ensuring ∂² = 0.

Three-term chain complex

We construct the three-term chain complex C₁ →[H_Z^T] C₀ →[H_X] C_{-1} directly as a HomologicalComplex (ModuleCat 𝔽₂) (ComplexShape.down ℤ).

The objects are defined by an if-cascade on the degree:

• degree 0: ModuleCat.of 𝔽₂ (Fin n → 𝔽₂)
• degree 1: ModuleCat.of 𝔽₂ (Fin rZ → 𝔽₂)
• degree -1: ModuleCat.of 𝔽₂ (Fin rX → 𝔽₂)
• otherwise: 0

The differentials use eqToHom to transport between the if-defined objects and the concrete ModuleCat.of types, following the pattern of HomologicalComplex.double.

noncomputable def CSSCode.complex {n rX rZ : ℕ} (Q : CSSCode n rX rZ) : ChainComplex𝔽₂

The three-term chain complex C₁ →[H_Z^T] C₀ →[H_X] C_{-1} associated to a CSS code. The objects are 𝔽₂^{r_Z} in degree 1, 𝔽₂^n in degree 0, 𝔽₂^{r_X} in degree -1, and 0 elsewhere. The differentials are H_Z^T from degree 1 to 0 and H_X from degree 0 to -1.

Equations

• One or more equations did not get rendered due to their size.

Code parameters

def CSSCode.numQubits {n : ℕ} : ℕ

The number of physical qubits n = dim C₀.

Equations

• CSSCode.numQubits = n

noncomputable def CSSCode.logicalQubits {n rX rZ : ℕ} (Q : CSSCode n rX rZ) : ℕ

The number of logical qubits k = dim H₀(C) = dim(ker H_X / im H_Z^T). The homology at degree 0 of the chain complex is ker H_X / im H_Z^T, which counts the number of independent logical qubits.

Equations

• Q.logicalQubits = Module.finrank 𝔽₂ (↥Q.HX.ker ⧸ Submodule.comap Q.HX.ker.subtype Q.HZT.range)

noncomputable def CSSCode.dX {n rX rZ : ℕ} (Q : CSSCode n rX rZ) : ℕ

The X-distance d_X is the minimum Hamming weight of a representative of a non-trivial element of H₀(C) = ker H_X / im H_Z^T. Equivalently, this is the minimum Hamming weight of any vector in ker H_X that is not in im H_Z^T. By convention (following ClassicalCode.distance), d_X = 0 when the homology is trivial (i.e., ker H_X = im H_Z^T).

Equations

• Q.dX = sInf {w : ℕ | ∃ x ∈ Q.HX.ker, x ∉ Q.HZT.range ∧ hammingWeight x = w}

noncomputable def CSSCode.dZ {n rX rZ : ℕ} (Q : CSSCode n rX rZ) : ℕ

The Z-distance d_Z is the minimum Hamming weight of a representative of a non-trivial element of H⁰(C) = ker H_Z / im H_X^T (Def_2). Since H_Z = (H_Z^T)^T and H_X^T is the transpose of H_X, we define this using dualMap:

• ker H_Z corresponds to ker (dualMap H_Z^T) in the dual of C₀
• im H_X^T corresponds to range (dualMap H_X) in the dual of C₀

Over 𝔽₂ with canonical bases, Dual(𝔽₂^n) ≅ 𝔽₂^n via dotProductEquiv. We use this identification to define the Hamming weight of dual functionals. By convention, d_Z = 0 when the cohomology is trivial.

Equations

• Q.dZ = sInf {w : ℕ | ∃ φ ∈ Q.HZT.dualMap.ker, φ ∉ Q.HX.dualMap.range ∧ hammingNorm ((dotProductEquiv 𝔽₂ (Fin n)).symm φ) = w}

noncomputable def CSSCode.distance {n rX rZ : ℕ} (Q : CSSCode n rX rZ) : ℕ

The overall distance d = min(d_X, d_Z).

Equations

• Q.distance = min Q.dX Q.dZ

Code parameter predicates

def CSSCode.IsNKDCode {n rX rZ : ℕ} (Q : CSSCode n rX rZ) (k d : ℕ) : Prop

A CSS code is an [[n, k, d]]-code if it has k logical qubits and distance d.

Equations

• Q.IsNKDCode k d = (Q.logicalQubits = k ∧ Q.distance = d)

def CSSCode.IsNKDXZCode {n rX rZ : ℕ} (Q : CSSCode n rX rZ) (k dX_val dZ_val : ℕ) : Prop

A CSS code is an [[n, k, d_X, d_Z]]-code when X- and Z-distances differ.

Equations

• Q.IsNKDXZCode k dX_val dZ_val = (Q.logicalQubits = k ∧ Q.dX = dX_val ∧ Q.dZ = dZ_val)