Def_13: Bivariate Bicycle Code

Statement

A Bivariate Bicycle (BB) code is a CSS code defined as follows:

Setup: Let ℓ, m be positive integers. Define:

• I_r: the r × r identity matrix
• C_r: the cyclic permutation matrix of r items, satisfying ⟨i|C_r = ⟨(i+1) mod r|
• x = C_ℓ ⊗ I_m (cyclic shift in the first coordinate)
• y = I_ℓ ⊗ C_m (cyclic shift in the second coordinate)

These matrices satisfy x^ℓ = y^m = I_{ℓm} and xᵀx = yᵀy = I_{ℓm}.

Qubits: The code uses n = 2ℓm physical qubits divided into ℓm left (L) and ℓm right (R) qubits.

Parity check matrices: Given polynomials A, B ∈ F₂[x,y], the parity check matrices are: H_X = [A | B], H_Z = [Bᵀ | Aᵀ] where Aᵀ = A(x⁻¹, y⁻¹).

Labeling: X checks, Z checks, L qubits, R qubits are each in 1-1 correspondence with elements of M = {x^a y^b : a, b ∈ Z}.

Main Definitions

• M : Monomial set ZMod ℓ × ZMod m
• GroupAlg : Group algebra F₂[M] for polynomials in x, y
• cyclicShiftX : Generator x as group algebra element
• cyclicShiftY : Generator y as group algebra element
• transposeAlg : Transpose operation A ↦ A(x⁻¹, y⁻¹)
• LabelType : Type for labeling {X, Z, L, R}
• BivariateBicycleCode : The full BB code structure with H_X and H_Z
• parityCheckX : H_X = [A | B]
• parityCheckZ : H_Z = [Bᵀ | Aᵀ]

Corollaries

• cyclicShiftX_order : x^ℓ = 1 in the group algebra
• cyclicShiftY_order : y^m = 1 in the group algebra
• transposeAlg_involutive : (Aᵀ)ᵀ = A
• permX_permY_comm : x and y commute as permutations
• permX_transpose_mul : xᵀx = I

Section 1: The Monomial Set M

Elements of M = {x^a y^b} are represented as pairs (a, b) ∈ ZMod ℓ × ZMod m. This is an additive abelian group where addition represents multiplication of monomials.

@[reducible, inline]

abbrev QEC1.BivariateBicycle.M (ℓ m : ℕ) : Type

The monomial set M = {x^a y^b : a ∈ ZMod ℓ, b ∈ ZMod m}.

Equations

• QEC1.BivariateBicycle.M ℓ m = (ZMod ℓ × ZMod m)

Section 2: Group Algebra F₂[M]

Polynomials in x, y over F₂ are elements of the group algebra (ZMod 2)[M]. An element is a finitely supported function M → ZMod 2.

@[reducible, inline]

abbrev QEC1.BivariateBicycle.GroupAlg (ℓ m : ℕ) : Type

The group algebra F₂[x, y] / (x^ℓ - 1, y^m - 1), represented as AddMonoidAlgebra.

Equations

• QEC1.BivariateBicycle.GroupAlg ℓ m = AddMonoidAlgebra (ZMod 2) (QEC1.BivariateBicycle.M ℓ m)

Section 3: Generators x and y

x corresponds to the monomial (1, 0) in M, representing C_ℓ ⊗ I_m. y corresponds to the monomial (0, 1) in M, representing I_ℓ ⊗ C_m.

noncomputable def QEC1.BivariateBicycle.cyclicShiftX (ℓ m : ℕ) : GroupAlg ℓ m

The generator x = C_ℓ ⊗ I_m as an element of the group algebra.

Equations

• QEC1.BivariateBicycle.cyclicShiftX ℓ m = Finsupp.single (1, 0) 1

noncomputable def QEC1.BivariateBicycle.cyclicShiftY (ℓ m : ℕ) : GroupAlg ℓ m

The generator y = I_ℓ ⊗ C_m as an element of the group algebra.

Equations

• QEC1.BivariateBicycle.cyclicShiftY ℓ m = Finsupp.single (0, 1) 1

noncomputable def QEC1.BivariateBicycle.monomial (ℓ m : ℕ) (a : ZMod ℓ) (b : ZMod m) : GroupAlg ℓ m

A monomial x^a y^b as an element of the group algebra.

Equations

• QEC1.BivariateBicycle.monomial ℓ m a b = Finsupp.single (a, b) 1

Section 4: Transpose Operation

For a BB code, the transpose operation is A^T = A(x⁻¹, y⁻¹). In the additive group M, this corresponds to negating both coordinates: (a, b) ↦ (-a, -b).

def QEC1.BivariateBicycle.transposeMonomial (ℓ m : ℕ) : M ℓ m → M ℓ m

The transpose operation on monomials: (a, b) ↦ (-a, -b).

Equations

• QEC1.BivariateBicycle.transposeMonomial ℓ m (a, b) = (-a, -b)

@[simp]

theorem QEC1.BivariateBicycle.transposeMonomial_apply (ℓ m : ℕ) [NeZero ℓ] [NeZero m] (a : ZMod ℓ) (b : ZMod m) : transposeMonomial ℓ m (a, b) = (-a, -b)

@[simp]

theorem QEC1.BivariateBicycle.transposeMonomial_involutive (ℓ m : ℕ) [NeZero ℓ] [NeZero m] : Function.Involutive (transposeMonomial ℓ m)

theorem QEC1.BivariateBicycle.transposeMonomial_injective (ℓ m : ℕ) [NeZero ℓ] [NeZero m] : Function.Injective (transposeMonomial ℓ m)

noncomputable def QEC1.BivariateBicycle.transposeAlg (ℓ m : ℕ) (p : GroupAlg ℓ m) : GroupAlg ℓ m

The transpose of a group algebra element: A^T = A(x⁻¹, y⁻¹). This maps each monomial (a,b) to (-a,-b), preserving coefficients.

Equations

• QEC1.BivariateBicycle.transposeAlg ℓ m p = Finsupp.mapDomain (QEC1.BivariateBicycle.transposeMonomial ℓ m) p

@[simp]

theorem QEC1.BivariateBicycle.transposeAlg_involutive (ℓ m : ℕ) [NeZero ℓ] [NeZero m] : Function.Involutive (transposeAlg ℓ m)

Section 5: Matrix Representation

The group algebra acts on F₂^{ℓm} by permutation. The matrix representation sends a polynomial p to the matrix whose (α, β) entry is the coefficient of α - β in p (i.e., a circulant-like structure on the product group).

noncomputable def QEC1.BivariateBicycle.toMatrix (ℓ m : ℕ) (p : GroupAlg ℓ m) : Matrix (M ℓ m) (M ℓ m) (ZMod 2)

Matrix representation of a group algebra element: the (α, β)-entry is p(α - β).

Equations

• QEC1.BivariateBicycle.toMatrix ℓ m p = Matrix.of fun (α β : QEC1.BivariateBicycle.M ℓ m) => p (α - β)

theorem QEC1.BivariateBicycle.toMatrix_transpose (ℓ m : ℕ) [NeZero ℓ] [NeZero m] (p : GroupAlg ℓ m) : (toMatrix ℓ m p).transpose = toMatrix ℓ m (transposeAlg ℓ m p)

The matrix transpose equals the algebraic transpose.

Section 6: Label Types

Checks and qubits are labeled by (α, T) where α ∈ M and T ∈ {X, Z, L, R}.

inductive QEC1.BivariateBicycle.LabelType : Type

The four label types for checks and qubits.

• X : LabelType
• Z : LabelType
• L : LabelType
• R : LabelType

instance QEC1.BivariateBicycle.instDecidableEqLabelType : DecidableEq LabelType

Equations

• QEC1.BivariateBicycle.instDecidableEqLabelType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def QEC1.BivariateBicycle.instReprLabelType.repr : LabelType → ℕ → Std.Format

Equations

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

instance QEC1.BivariateBicycle.instReprLabelType : Repr LabelType

Equations

• QEC1.BivariateBicycle.instReprLabelType = { reprPrec := QEC1.BivariateBicycle.instReprLabelType.repr }

@[reducible, inline]

abbrev QEC1.BivariateBicycle.LabeledElement (ℓ m : ℕ) : Type

A labeled element: a monomial paired with a label type.

Equations

• QEC1.BivariateBicycle.LabeledElement ℓ m = (QEC1.BivariateBicycle.M ℓ m × QEC1.BivariateBicycle.LabelType)

Section 7: Bivariate Bicycle Code Structure

structure QEC1.BivariateBicycle.BivariateBicycleCode (ℓ m : ℕ) : Type

A Bivariate Bicycle (BB) code specified by parameters ℓ, m and polynomials A, B.

• polyA : GroupAlg ℓ m

  First polynomial A ∈ F₂[x, y]

• polyB : GroupAlg ℓ m

  Second polynomial B ∈ F₂[x, y]

def QEC1.BivariateBicycle.BivariateBicycleCode.numPhysicalQubits (ℓ m : ℕ) : ℕ

The number of physical qubits: n = 2ℓm.

Equations

• QEC1.BivariateBicycle.BivariateBicycleCode.numPhysicalQubits ℓ m = 2 * ℓ * m

def QEC1.BivariateBicycle.BivariateBicycleCode.numLeftQubits (ℓ m : ℕ) : ℕ

The number of left qubits: ℓm.

Equations

• QEC1.BivariateBicycle.BivariateBicycleCode.numLeftQubits ℓ m = ℓ * m

def QEC1.BivariateBicycle.BivariateBicycleCode.numRightQubits (ℓ m : ℕ) : ℕ

The number of right qubits: ℓm.

Equations

• QEC1.BivariateBicycle.BivariateBicycleCode.numRightQubits ℓ m = ℓ * m

theorem QEC1.BivariateBicycle.BivariateBicycleCode.numPhysicalQubits_eq (ℓ m : ℕ) : numPhysicalQubits ℓ m = numLeftQubits ℓ m + numRightQubits ℓ m

n = numLeftQubits + numRightQubits

def QEC1.BivariateBicycle.BivariateBicycleCode.numXChecks (ℓ m : ℕ) : ℕ

The number of X checks: ℓm.

Equations

• QEC1.BivariateBicycle.BivariateBicycleCode.numXChecks ℓ m = ℓ * m

def QEC1.BivariateBicycle.BivariateBicycleCode.numZChecks (ℓ m : ℕ) : ℕ

The number of Z checks: ℓm.

Equations

• QEC1.BivariateBicycle.BivariateBicycleCode.numZChecks ℓ m = ℓ * m

Section 8: Parity Check Matrices

H_X = [A | B] : ℓm × 2ℓm matrix (rows indexed by M, columns by M ⊕ M) H_Z = [B^T | A^T] : ℓm × 2ℓm matrix

noncomputable def QEC1.BivariateBicycle.BivariateBicycleCode.matA {ℓ m : ℕ} (code : BivariateBicycleCode ℓ m) : Matrix (M ℓ m) (M ℓ m) (ZMod 2)

Matrix representation of polynomial A.

Equations

• code.matA = QEC1.BivariateBicycle.toMatrix ℓ m code.polyA

noncomputable def QEC1.BivariateBicycle.BivariateBicycleCode.matB {ℓ m : ℕ} (code : BivariateBicycleCode ℓ m) : Matrix (M ℓ m) (M ℓ m) (ZMod 2)

Matrix representation of polynomial B.

Equations

• code.matB = QEC1.BivariateBicycle.toMatrix ℓ m code.polyB

noncomputable def QEC1.BivariateBicycle.BivariateBicycleCode.matAT {ℓ m : ℕ} (code : BivariateBicycleCode ℓ m) : Matrix (M ℓ m) (M ℓ m) (ZMod 2)

Matrix representation of A^T = A(x⁻¹, y⁻¹).

Equations

• code.matAT = QEC1.BivariateBicycle.toMatrix ℓ m (QEC1.BivariateBicycle.transposeAlg ℓ m code.polyA)

noncomputable def QEC1.BivariateBicycle.BivariateBicycleCode.matBT {ℓ m : ℕ} (code : BivariateBicycleCode ℓ m) : Matrix (M ℓ m) (M ℓ m) (ZMod 2)

Matrix representation of B^T = B(x⁻¹, y⁻¹).

Equations

• code.matBT = QEC1.BivariateBicycle.toMatrix ℓ m (QEC1.BivariateBicycle.transposeAlg ℓ m code.polyB)

theorem QEC1.BivariateBicycle.BivariateBicycleCode.matAT_eq_transpose {ℓ m : ℕ} [NeZero ℓ] [NeZero m] (code : BivariateBicycleCode ℓ m) : code.matAT = code.matA.transpose

matAT is the matrix transpose of matA.

theorem QEC1.BivariateBicycle.BivariateBicycleCode.matBT_eq_transpose {ℓ m : ℕ} [NeZero ℓ] [NeZero m] (code : BivariateBicycleCode ℓ m) : code.matBT = code.matB.transpose

matBT is the matrix transpose of matB.

noncomputable def QEC1.BivariateBicycle.BivariateBicycleCode.parityCheckX {ℓ m : ℕ} (code : BivariateBicycleCode ℓ m) : Matrix (M ℓ m) (M ℓ m ⊕ M ℓ m) (ZMod 2)

The X parity check matrix H_X = [A | B]. Rows indexed by M (checks), columns by M ⊕ M (left ⊕ right qubits).

Equations

• code.parityCheckX = code.matA.fromCols code.matB

noncomputable def QEC1.BivariateBicycle.BivariateBicycleCode.parityCheckZ {ℓ m : ℕ} (code : BivariateBicycleCode ℓ m) : Matrix (M ℓ m) (M ℓ m ⊕ M ℓ m) (ZMod 2)

The Z parity check matrix H_Z = [B^T | A^T]. Rows indexed by M (checks), columns by M ⊕ M (left ⊕ right qubits).

Equations

• code.parityCheckZ = code.matBT.fromCols code.matAT

Section 9: CSS Orthogonality

For a valid CSS code, H_X · H_Z^T = 0. This follows from AB^T + BA^T = 0 in F₂.

def QEC1.BivariateBicycle.BivariateBicycleCode.isCSS {ℓ m : ℕ} [NeZero ℓ] [NeZero m] (code : BivariateBicycleCode ℓ m) : Prop

CSS orthogonality condition: A * B^T + B * A^T = 0 over F₂. This ensures commutativity of X and Z stabilizers.

Equations

• code.isCSS = (code.matA * code.matBT + code.matB * code.matAT = 0)

Section 10: Pauli Notation

X(p, q) denotes an X-type Pauli acting on left qubits with pattern p and right qubits with pattern q. Similarly Z(p, q) for Z-type.

structure QEC1.BivariateBicycle.BivariateBicycleCode.PauliX (ℓ m : ℕ) [NeZero ℓ] [NeZero m] : Type

An X-type Pauli operator X(p, q) specified by polynomials for left and right qubits.

• leftPoly : GroupAlg ℓ m

  Pattern on left qubits

• rightPoly : GroupAlg ℓ m

  Pattern on right qubits

structure QEC1.BivariateBicycle.BivariateBicycleCode.PauliZ (ℓ m : ℕ) [NeZero ℓ] [NeZero m] : Type

A Z-type Pauli operator Z(p, q) specified by polynomials for left and right qubits.

• leftPoly : GroupAlg ℓ m

  Pattern on left qubits

• rightPoly : GroupAlg ℓ m

  Pattern on right qubits

noncomputable def QEC1.BivariateBicycle.BivariateBicycleCode.PauliX.support {ℓ m : ℕ} [NeZero ℓ] [NeZero m] (P : PauliX ℓ m) : M ℓ m ⊕ M ℓ m → ZMod 2

Support of a Pauli X(p,q) as a binary vector over left ⊕ right qubits.

Equations

• P.support (Sum.inl α) = P.leftPoly α
• P.support (Sum.inr α) = P.rightPoly α

noncomputable def QEC1.BivariateBicycle.BivariateBicycleCode.PauliZ.support {ℓ m : ℕ} [NeZero ℓ] [NeZero m] (P : PauliZ ℓ m) : M ℓ m ⊕ M ℓ m → ZMod 2

Support of a Pauli Z(p,q) as a binary vector over left ⊕ right qubits.

Equations

• P.support (Sum.inl α) = P.leftPoly α
• P.support (Sum.inr α) = P.rightPoly α

Section 11: Order Properties of x and y

theorem QEC1.BivariateBicycle.cyclicShiftX_order (ℓ m : ℕ) [NeZero ℓ] [NeZero m] : monomial ℓ m (↑ℓ) 0 = monomial ℓ m 0 0

x^ℓ = 1 in the group algebra (since ℓ · (1, 0) = (0, 0) in ZMod ℓ × ZMod m).

theorem QEC1.BivariateBicycle.cyclicShiftY_order (ℓ m : ℕ) [NeZero ℓ] [NeZero m] : monomial ℓ m 0 ↑m = monomial ℓ m 0 0

y^m = 1 in the group algebra (since m · (0, 1) = (0, 0) in ZMod ℓ × ZMod m).

Section 12: The Cyclic Permutation Matrix

C_r is the permutation matrix for the cyclic shift i ↦ i + 1 on ZMod r. We define it using Equiv.Perm and relate it to the group algebra representation.

def QEC1.BivariateBicycle.cyclicPerm (r : ℕ) [NeZero r] : Equiv.Perm (ZMod r)

The cyclic permutation on ZMod r: i ↦ i + 1.

Equations

• QEC1.BivariateBicycle.cyclicPerm r = { toFun := fun (i : ZMod r) => i + 1, invFun := fun (i : ZMod r) => i - 1, left_inv := ⋯, right_inv := ⋯ }

def QEC1.BivariateBicycle.permX (ℓ m : ℕ) : Equiv.Perm (M ℓ m)

x as a permutation on M = ZMod ℓ × ZMod m: (a, b) ↦ (a + 1, b).

Equations

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

def QEC1.BivariateBicycle.permY (ℓ m : ℕ) : Equiv.Perm (M ℓ m)

y as a permutation on M = ZMod ℓ × ZMod m: (a, b) ↦ (a, b + 1).

Equations

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

theorem QEC1.BivariateBicycle.permX_permY_comm (ℓ m : ℕ) [NeZero ℓ] [NeZero m] : Equiv.trans (permX ℓ m) (permY ℓ m) = Equiv.trans (permY ℓ m) (permX ℓ m)

x and y commute as permutations.

theorem QEC1.BivariateBicycle.permX_transpose_mul (ℓ m : ℕ) [NeZero ℓ] [NeZero m] [DecidableEq (M ℓ m)] : (Equiv.Perm.permMatrix (ZMod 2) (permX ℓ m)).transpose * Equiv.Perm.permMatrix (ZMod 2) (permX ℓ m) = 1

The permutation matrix of x is orthogonal: xᵀx = I.

theorem QEC1.BivariateBicycle.permY_transpose_mul (ℓ m : ℕ) [NeZero ℓ] [NeZero m] [DecidableEq (M ℓ m)] : (Equiv.Perm.permMatrix (ZMod 2) (permY ℓ m)).transpose * Equiv.Perm.permMatrix (ZMod 2) (permY ℓ m) = 1

The permutation matrix of y is orthogonal: yᵀy = I.