Definition 6: Subsystem CSS Code

A subsystem CSS code is a CSS code (Def_4) where the homology H₀ = ker(H_X) / im(H_Z^T) is split as a direct sum of 𝔽₂-vector spaces H₀ = H₀^L ⊕ H₀^G, where H₀^L corresponds to logical qubits and H₀^G corresponds to gauge qubits.

The nondegenerate pairing between H₀ and the cohomology H⁰ (Def_2) induces a compatible splitting H⁰ = H⁰_L ⊕ H⁰_G, where compatible means H₀^L pairs nondegenerately with H⁰_L and H₀^G pairs nondegenerately with H⁰_G (and the cross-pairings vanish).

The Z-distance d_Z is the minimum Hamming weight of a representative of a homology class whose projection onto H₀^L is nonzero. The X-distance d_X is defined equivalently using the cohomology splitting. The distance is d = min(d_X, d_Z).

Main Definitions

• SubsystemCSSCode — a subsystem CSS code with direct sum splittings
• SubsystemCSSCode.dZ — the Z-distance (using homology projection)
• SubsystemCSSCode.dX — the X-distance (using cohomology projection)
• SubsystemCSSCode.distance — the overall distance d = min(d_X, d_Z)
• SubsystemCSSCode.logicalQubits — the number of logical qubits dim H₀^L

Homology and cohomology quotient types

@[reducible, inline]

noncomputable abbrev CSSCode.boundariesInCycles {n rX rZ : ℕ} (Q : CSSCode n rX rZ) : Submodule 𝔽₂ ↥Q.HX.ker

The submodule of boundaries inside cycles for the CSS code homology: im(H_Z^T) ∩ ker(H_X) viewed as a submodule of ker(H_X).

Equations

• Q.boundariesInCycles = Submodule.comap Q.HX.ker.subtype Q.HZT.range

@[reducible, inline]

noncomputable abbrev CSSCode.Homology₀ {n rX rZ : ℕ} (Q : CSSCode n rX rZ) : Type

The homology type H₀ = ker(H_X) / im(H_Z^T).

Equations

• Q.Homology₀ = (↥Q.HX.ker ⧸ Q.boundariesInCycles)

@[reducible, inline]

noncomputable abbrev CSSCode.coboundariesInCocycles {n rX rZ : ℕ} (Q : CSSCode n rX rZ) : Submodule 𝔽₂ ↥Q.HZT.dualMap.ker

The submodule of coboundaries inside cocycles for the CSS code cohomology: im(H_X^T) ∩ ker(H_Z) viewed as a submodule of ker(H_Z), where H_Z = (H_Z^T)^T = dualMap(H_Z^T) and H_X^T = dualMap(H_X).

Equations

• Q.coboundariesInCocycles = Submodule.comap Q.HZT.dualMap.ker.subtype Q.HX.dualMap.range

@[reducible, inline]

noncomputable abbrev CSSCode.Cohomology₀ {n rX rZ : ℕ} (Q : CSSCode n rX rZ) : Type

The cohomology type H⁰ = ker(H_Z) / im(H_X^T).

Equations

• Q.Cohomology₀ = (↥Q.HZT.dualMap.ker ⧸ Q.coboundariesInCocycles)

@[reducible, inline]

noncomputable abbrev CSSCode.homologyMkQ {n rX rZ : ℕ} (Q : CSSCode n rX rZ) : ↥Q.HX.ker →ₗ[𝔽₂] Q.Homology₀

The quotient map from ker(H_X) to the homology H₀.

Equations

• Q.homologyMkQ = Q.boundariesInCycles.mkQ

@[reducible, inline]

noncomputable abbrev CSSCode.cohomologyMkQ {n rX rZ : ℕ} (Q : CSSCode n rX rZ) : ↥Q.HZT.dualMap.ker →ₗ[𝔽₂] Q.Cohomology₀

The quotient map from ker(H_Z) (= ker(dualMap H_Z^T)) to the cohomology H⁰.

Equations

• Q.cohomologyMkQ = Q.coboundariesInCocycles.mkQ

Subsystem CSS Code Structure

structure SubsystemCSSCode (n rX rZ : ℕ) extends CSSCode n rX rZ : Type

A subsystem CSS code is a CSS code (Def_4) together with a direct sum decomposition of the homology H₀ = H₀^L ⊕ H₀^G and a compatible splitting of the cohomology H⁰ = H⁰_L ⊕ H⁰_G, induced by a linear equivalence H₀ ≃ H⁰ that respects the decomposition.

The submodule HL (logical) and HG (gauge) of the homology quotient satisfy IsCompl HL HG, giving the direct sum decomposition. The linear equivalence equiv between homology and cohomology (encoding the nondegenerate pairing) induces the cohomology splitting: H⁰_L = equiv(H₀^L) and H⁰_G = equiv(H₀^G). This ensures that H₀^L pairs nondegenerately with H⁰_L, H₀^G pairs nondegenerately with H⁰_G, and the cross-pairings vanish.

• HX : (Fin n → 𝔽₂) →ₗ[𝔽₂] Fin rX → 𝔽₂
• HZT : (Fin rZ → 𝔽₂) →ₗ[𝔽₂] Fin n → 𝔽₂
• css_condition : self.HX ∘ₗ self.HZT = 0
• HL : Submodule 𝔽₂ self.Homology₀

  The logical subspace H₀^L of the homology H₀ = ker(H_X) / im(H_Z^T).

• HG : Submodule 𝔽₂ self.Homology₀

  The gauge subspace H₀^G of the homology.

• hcompl : IsCompl self.HL self.HG

  The direct sum decomposition H₀ = H₀^L ⊕ H₀^G.

• equiv : self.Homology₀ ≃ₗ[𝔽₂] self.Cohomology₀

  The linear equivalence H₀ ≃ H⁰ between homology and cohomology, encoding the nondegenerate pairing. The cohomology splitting is induced by this map: H⁰_L = equiv(H₀^L) and H⁰_G = equiv(H₀^G).

Derived cohomology splitting

noncomputable def SubsystemCSSCode.coHL {n rX rZ : ℕ} (S : SubsystemCSSCode n rX rZ) : Submodule 𝔽₂ S.Cohomology₀

The logical subspace H⁰_L of the cohomology, defined as the image of H₀^L under the equivalence equiv : H₀ ≃ H⁰.

Equations

• S.coHL = Submodule.map (↑S.equiv) S.HL

noncomputable def SubsystemCSSCode.coHG {n rX rZ : ℕ} (S : SubsystemCSSCode n rX rZ) : Submodule 𝔽₂ S.Cohomology₀

The gauge subspace H⁰_G of the cohomology, defined as the image of H₀^G under the equivalence equiv : H₀ ≃ H⁰.

Equations

• S.coHG = Submodule.map (↑S.equiv) S.HG

theorem SubsystemCSSCode.cohcompl {n rX rZ : ℕ} (S : SubsystemCSSCode n rX rZ) : IsCompl S.coHL S.coHG

The cohomology splitting H⁰ = H⁰_L ⊕ H⁰_G is induced by the homology splitting and the linear equivalence.

Projection onto the logical subspace

noncomputable def SubsystemCSSCode.projL {n rX rZ : ℕ} (S : SubsystemCSSCode n rX rZ) : S.Homology₀ →ₗ[𝔽₂] ↥S.HL

The linear projection from H₀ onto the logical subspace H₀^L, using the direct sum decomposition H₀ = H₀^L ⊕ H₀^G.

Equations

• S.projL = S.HL.linearProjOfIsCompl S.HG ⋯

noncomputable def SubsystemCSSCode.coprojL {n rX rZ : ℕ} (S : SubsystemCSSCode n rX rZ) : S.Cohomology₀ →ₗ[𝔽₂] ↥S.coHL

The linear projection from H⁰ onto the logical cohomology subspace H⁰_L, using the derived direct sum decomposition H⁰ = H⁰_L ⊕ H⁰_G.

Equations

• S.coprojL = S.coHL.linearProjOfIsCompl S.coHG ⋯

Number of logical qubits

noncomputable def SubsystemCSSCode.logicalQubits {n rX rZ : ℕ} (S : SubsystemCSSCode n rX rZ) : ℕ

The number of logical qubits k = dim H₀^L. In a subsystem code, only the logical subspace H₀^L encodes information, while the gauge subspace H₀^G corresponds to gauge degrees of freedom.

Equations

• S.logicalQubits = Module.finrank 𝔽₂ ↥S.HL

Subsystem Z-distance

noncomputable def SubsystemCSSCode.dZ {n rX rZ : ℕ} (S : SubsystemCSSCode n rX rZ) : ℕ

The Z-distance d_Z for a subsystem CSS code. This is the minimum Hamming weight of a representative z ∈ ker(H_X) of a homology class [z] ∈ H₀ whose projection onto the logical subspace H₀^L is nonzero. Equivalently, d_Z is the largest integer such that every representative of a class with nonzero logical projection has Hamming weight at least d_Z.

By convention, d_Z = 0 when there is no such class (i.e., H₀^L = 0).

Equations

• S.dZ = sInf {w : ℕ | ∃ (x : Fin n → 𝔽₂) (hx : x ∈ S.HX.ker), S.projL (S.homologyMkQ ⟨x, hx⟩) ≠ 0 ∧ hammingWeight x = w}

Subsystem X-distance

noncomputable def SubsystemCSSCode.dX {n rX rZ : ℕ} (S : SubsystemCSSCode n rX rZ) : ℕ

The X-distance d_X for a subsystem CSS code. This is the minimum Hamming weight (under the dotProductEquiv identification Dual(𝔽₂^n) ≅ 𝔽₂^n) of a representative ζ ∈ ker(H_Z) of a cohomology class [ζ] ∈ H⁰ whose projection onto H⁰_L is nonzero.

By convention, d_X = 0 when H⁰_L = 0.

Equations

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

Overall distance

noncomputable def SubsystemCSSCode.distance {n rX rZ : ℕ} (S : SubsystemCSSCode n rX rZ) : ℕ

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

Equations

• S.distance = min S.dX S.dZ

Code parameter predicates

def SubsystemCSSCode.IsNKDCode {n rX rZ : ℕ} (S : SubsystemCSSCode n rX rZ) (k d : ℕ) : Prop

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

Equations

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

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

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

Equations

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