Definition 29: Horizontal Subsystem Balanced Product Code

The horizontal subsystem balanced product code is the subsystem CSS code (Def_6) whose underlying CSS code is the balanced product Tanner cycle code (Def_26), with the logical/gauge splitting defined by:

• H₁ᴸ := H₁ʰ (logical Z-operators correspond to horizontal homology)
• H₁ᴳ := H₁ᵛ (gauge Z-operators correspond to vertical homology)

We define HL and HG as submodules of H₁ via the Künneth isomorphism and prove they form a complementary pair (IsCompl). This gives the direct sum decomposition H₁ ≅ H₁ᴸ ⊕ H₁ᴳ required by the subsystem CSS code structure.

When the quotient Tanner differential is injective, H₁ᵛ = 0 and hence H₁ᴳ = 0, reducing the subsystem code to an ordinary CSS code.

Main Definitions

• HL — the logical submodule of H₁ (image of H₁ʰ under the Künneth iso)
• HG — the gauge submodule of H₁ (image of H₁ᵛ under the Künneth iso)
• hcompl — proof that HL and HG are complementary
• HG_eq_bot_of_tanner_H0_subsingleton — when H₀(C(X,L)) = 0, HG = ⊥
• cohomology_iscompl — the cohomology splitting H¹ = H¹_L ⊕ H¹_G

Main Results

• HL_eq_bot_of_quotient_ker_trivial — injectivity of quotient ∂ implies HL = ⊥
• encodingRate_eq — the logical qubits equal dim H₁(C(X/H, L))

Abbreviations from Def_27

@[reducible, inline]

abbrev HorizontalSubsystemBalancedProductCode.bpComplex {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) : ChainComplex𝔽₂

The balanced product complex.

Equations

• HorizontalSubsystemBalancedProductCode.bpComplex X Λ ℓ hΛ hcompat = HorizontalVerticalHomologySplitting.bpComplex X Λ ℓ hΛ hcompat

@[reducible, inline]

abbrev HorizontalSubsystemBalancedProductCode.H1 {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) : Type

The degree-1 homology of the balanced product complex.

Equations

• HorizontalSubsystemBalancedProductCode.H1 X Λ ℓ hΛ hcompat = HorizontalVerticalHomologySplitting.H1 X Λ ℓ hΛ hcompat

@[reducible, inline]

abbrev HorizontalSubsystemBalancedProductCode.H1h {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) : Type

The horizontal homology H₁ʰ.

Equations

• HorizontalSubsystemBalancedProductCode.H1h X Λ ℓ hΛ hcompat = HorizontalVerticalHomologySplitting.H1h X Λ ℓ hΛ hcompat

@[reducible, inline]

abbrev HorizontalSubsystemBalancedProductCode.H1v {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) : Type

The vertical homology H₁ᵛ.

Equations

• HorizontalSubsystemBalancedProductCode.H1v X Λ ℓ hΛ hcompat = HorizontalVerticalHomologySplitting.H1v X Λ ℓ hΛ hcompat

Logical and Gauge Submodules

We define the logical submodule HL and gauge submodule HG as the images of the horizontal and vertical summand inclusions under the inverse Künneth isomorphism.

def HorizontalSubsystemBalancedProductCode.incH {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) : H1h X Λ ℓ hΛ hcompat →ₗ[𝔽₂] (HorizontalVerticalHomologySplitting.tannerHEq X Λ hΛ).balancedKunnethSum (HorizontalVerticalHomologySplitting.cycleHEq ℓ hcompat) 1

The inclusion of the horizontal summand H₁ʰ into the Künneth direct sum.

Equations

• HorizontalSubsystemBalancedProductCode.incH X Λ ℓ hΛ hcompat = HorizontalVerticalHomologySplitting.directSumInc X Λ ℓ hΛ hcompat 1

def HorizontalSubsystemBalancedProductCode.incV {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) : H1v X Λ ℓ hΛ hcompat →ₗ[𝔽₂] (HorizontalVerticalHomologySplitting.tannerHEq X Λ hΛ).balancedKunnethSum (HorizontalVerticalHomologySplitting.cycleHEq ℓ hcompat) 1

The inclusion of the vertical summand H₁ᵛ into the Künneth direct sum.

Equations

• HorizontalSubsystemBalancedProductCode.incV X Λ ℓ hΛ hcompat = HorizontalVerticalHomologySplitting.directSumInc X Λ ℓ hΛ hcompat 0

def HorizontalSubsystemBalancedProductCode.embH {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (hodd : Odd (Fintype.card H)) : H1h X Λ ℓ hΛ hcompat →ₗ[𝔽₂] H1 X Λ ℓ hΛ hcompat

The embedding of H₁ʰ into H₁ via the inverse Künneth isomorphism.

Equations

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

def HorizontalSubsystemBalancedProductCode.embV {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (hodd : Odd (Fintype.card H)) : H1v X Λ ℓ hΛ hcompat →ₗ[𝔽₂] H1 X Λ ℓ hΛ hcompat

The embedding of H₁ᵛ into H₁ via the inverse Künneth isomorphism.

Equations

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

def HorizontalSubsystemBalancedProductCode.HL {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (hodd : Odd (Fintype.card H)) : Submodule 𝔽₂ (H1 X Λ ℓ hΛ hcompat)

The logical submodule H₁ᴸ := H₁ʰ as a submodule of H₁, defined as the range of the horizontal embedding. Logical Z-operators correspond to nontrivial elements of the horizontal homology.

Equations

• HorizontalSubsystemBalancedProductCode.HL X Λ ℓ hΛ hcompat hodd = (HorizontalSubsystemBalancedProductCode.embH X Λ ℓ hΛ hcompat hodd).range

def HorizontalSubsystemBalancedProductCode.HG {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (hodd : Odd (Fintype.card H)) : Submodule 𝔽₂ (H1 X Λ ℓ hΛ hcompat)

The gauge submodule H₁ᴳ := H₁ᵛ as a submodule of H₁, defined as the range of the vertical embedding. Gauge Z-operators correspond to the vertical homology.

Equations

• HorizontalSubsystemBalancedProductCode.HG X Λ ℓ hΛ hcompat hodd = (HorizontalSubsystemBalancedProductCode.embV X Λ ℓ hΛ hcompat hodd).range

Subsingleton infrastructure for direct sum decomposition

Complementarity

theorem HorizontalSubsystemBalancedProductCode.hcompl {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (hodd : Odd (Fintype.card H)) : IsCompl (HL X Λ ℓ hΛ hcompat hodd) (HG X Λ ℓ hΛ hcompat hodd)

The logical and gauge submodules form a complementary pair: H₁ = H₁ᴸ ⊕ H₁ᴳ. This follows from the Künneth decomposition H₁ ≅ ⊕_p H_p(C(X,L)) ⊗_H H_{1-p}(C_ℓ) with only the p = 0, 1 summands being nontrivial.

Cohomology splitting

Over 𝔽₂, homology and cohomology are naturally isomorphic (Def_2). In Def_27, the cohomology summands coH1h and coH1v are defined as the same balanced Künneth summands as H1h and H1v respectively (since the underlying types coincide over 𝔽₂). Therefore the cohomology logical/gauge submodules are definitionally equal to their homology counterparts, and the cohomology complementarity follows from hcompl.

@[reducible, inline]

abbrev HorizontalSubsystemBalancedProductCode.coHL {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (hodd : Odd (Fintype.card H)) : Submodule 𝔽₂ (H1 X Λ ℓ hΛ hcompat)

The logical cohomology submodule H¹_L := H¹_h. Over 𝔽₂, the cohomology summands coincide with the homology summands (Def_27: coH1h = H1h), so the logical cohomology submodule equals HL.

Equations

• HorizontalSubsystemBalancedProductCode.coHL X Λ ℓ hΛ hcompat hodd = HorizontalSubsystemBalancedProductCode.HL X Λ ℓ hΛ hcompat hodd

@[reducible, inline]

abbrev HorizontalSubsystemBalancedProductCode.coHG {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (hodd : Odd (Fintype.card H)) : Submodule 𝔽₂ (H1 X Λ ℓ hΛ hcompat)

The gauge cohomology submodule H¹_G := H¹_v. Over 𝔽₂, the cohomology summands coincide with the homology summands (Def_27: coH1v = H1v), so the gauge cohomology submodule equals HG.

Equations

• HorizontalSubsystemBalancedProductCode.coHG X Λ ℓ hΛ hcompat hodd = HorizontalSubsystemBalancedProductCode.HG X Λ ℓ hΛ hcompat hodd

theorem HorizontalSubsystemBalancedProductCode.cohomology_iscompl {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (hodd : Odd (Fintype.card H)) : IsCompl (coHL X Λ ℓ hΛ hcompat hodd) (coHG X Λ ℓ hΛ hcompat hodd)

The cohomology logical and gauge submodules are complementary: H¹ = H¹_L ⊕ H¹_G. This follows directly from the homology complementarity hcompl since over 𝔽₂, the cohomology splitting is identified with the homology splitting via Def_2 and Def_27.

Reduction to ordinary CSS code

theorem HorizontalSubsystemBalancedProductCode.HL_eq_bot_of_quotient_ker_trivial {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (hodd : Odd (Fintype.card H)) (h_odd : ℓ % 2 = 1) (hker : (IotaPiMaps.quotientTannerDifferential X Λ hΛ).ker = ⊥) : HL X Λ ℓ hΛ hcompat hodd = ⊥

When the quotient Tanner differential is injective (i.e., ker(∂) = 0), the horizontal homology H₁ʰ is zero. By the iota/pi isomorphism (Def_28), H₁ʰ ≅ H₁(C(X/H, L)), so injectivity of the quotient differential implies H₁ʰ = 0 and hence HL = ⊥.

Note: this is a consequence of injectivity, proving the logical part vanishes. The paper's main reduction result (gauge vanishes) is HG_eq_bot_of_tanner_H0_subsingleton.

theorem HorizontalSubsystemBalancedProductCode.HG_eq_bot_of_tanner_H0_subsingleton {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (hodd : Odd (Fintype.card H)) (hss : Subsingleton ((HorizontalVerticalHomologySplitting.tannerHEq X Λ hΛ).complex.homology' 0)) : HG X Λ ℓ hΛ hcompat hodd = ⊥

When the degree-0 homology of the Tanner complex H₀(C(X,L)) is trivial, the gauge submodule HG = H₁ᵛ vanishes. The proof proceeds through the Künneth structure:

1. H₀(C(X,L)) is subsingleton (hypothesis)
2. H₀(C(X,L)) ⊗ H₁(C_ℓ) is subsingleton (tensor with subsingleton)
3. Coinvariants(H₀(C(X,L)) ⊗ H₁(C_ℓ)) is subsingleton (quotient of subsingleton)
4. H₁ᵛ = 0 since H₁ᵛ is this coinvariant module
5. HG = range(embV) = ⊥ since embV maps zero to zero

The paper states this follows from H₀(C(X/H, L)) = 0 (surjectivity of the quotient differential ∂: C₁(X/H, L) → C₀(X/H, L)), which is a weaker condition: H₀ of the quotient being trivial implies trivial coinvariants of H₀(C(X,L)), which in turn implies the result. We use the stronger condition H₀(C(X,L)) = 0 here since the degree-0 iota/pi maps (connecting quotient H₀ to equivariant H₀ coinvariants) are not formalized.

Encoding rate

def HorizontalSubsystemBalancedProductCode.logicalQubits {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (hodd : Odd (Fintype.card H)) : ℕ

The number of logical qubits of the horizontal subsystem code equals the dimension of the logical submodule HL.

Equations

• HorizontalSubsystemBalancedProductCode.logicalQubits X Λ ℓ hΛ hcompat hodd = Module.finrank 𝔽₂ ↥(HorizontalSubsystemBalancedProductCode.HL X Λ ℓ hΛ hcompat hodd)

Witness lemmas

theorem HorizontalSubsystemBalancedProductCode.HL_nonempty {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (hodd : Odd (Fintype.card H)) : (HL X Λ ℓ hΛ hcompat hodd).carrier.Nonempty

Witness: HL is nonempty (it is a submodule, hence contains 0).

theorem HorizontalSubsystemBalancedProductCode.HG_nonempty {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (hodd : Odd (Fintype.card H)) : (HG X Λ ℓ hΛ hcompat hodd).carrier.Nonempty

Witness: HG is nonempty (it is a submodule, hence contains 0).