Remark 19: Bivariate Bicycle Code Notation

Statement

The Bivariate Bicycle (BB) code construction uses cyclic permutation matrices and their tensor products to define CSS codes on 2ℓm qubits.

Main Results

• BBMonomial: the monomial group M = Z_ℓ × Z_m indexing qubits and checks
• BBGroupAlgebra: the group algebra F₂[x,y]/(x^ℓ-1, y^m-1) as ZMod 2-valued functions
• BBQubit: the qubit type for a BB code (L ⊕ R, each indexed by M)
• bbConvolve: polynomial multiplication in the group algebra (convolution)
• bbTranspose: the transpose operation A(x,y) ↦ A(x⁻¹,y⁻¹)
• bbCheckX, bbCheckZ: X-type and Z-type parity checks
• BBCode: the bivariate bicycle code as a stabilizer code
• pauliXBB, pauliZBB: the Pauli notation X(p,q) and Z(p,q)

Corollaries

• bbConvolve_comm: convolution is commutative (the monomial group is abelian)
• bbTranspose_involutive: transpose is an involution
• bbCode_numQubits: the code has 2ℓm physical qubits
• bbChecks_commute: X and Z checks commute (CSS property)

The monomial group and group algebra

@[reducible, inline]

abbrev BivariateBicycle.BBMonomial (ℓ m : ℕ) : Type

The monomial group M = Z_ℓ × Z_m, representing monomials x^a y^b with a ∈ {0,...,ℓ-1} and b ∈ {0,...,m-1}. We use ZMod for the additive group structure (addition corresponds to monomial multiplication).

Equations

• BivariateBicycle.BBMonomial ℓ m = (ZMod ℓ × ZMod m)

@[reducible, inline]

abbrev BivariateBicycle.BBGroupAlgebra (ℓ m : ℕ) : Type

The group algebra F₂[x,y]/(x^ℓ-1, y^m-1). An element is a function M → ZMod 2, where the value at (a,b) is the coefficient of x^a y^b.

Equations

• BivariateBicycle.BBGroupAlgebra ℓ m = (BivariateBicycle.BBMonomial ℓ m → ZMod 2)

def BivariateBicycle.bbMonomial {ℓ m : ℕ} (a : ZMod ℓ) (b : ZMod m) : BBGroupAlgebra ℓ m

The monomial x^a y^b as an element of the group algebra: the indicator function of the single element (a, b).

Equations

• BivariateBicycle.bbMonomial a b p = if p = (a, b) then 1 else 0

def BivariateBicycle.bbZero {ℓ m : ℕ} : BBGroupAlgebra ℓ m

The zero polynomial.

Equations

• BivariateBicycle.bbZero x✝ = 0

def BivariateBicycle.bbOne {ℓ m : ℕ} [NeZero ℓ] [NeZero m] : BBGroupAlgebra ℓ m

The unit polynomial 1 = x^0 y^0.

Equations

• BivariateBicycle.bbOne = BivariateBicycle.bbMonomial 0 0

def BivariateBicycle.bbAdd {ℓ m : ℕ} (p q : BBGroupAlgebra ℓ m) : BBGroupAlgebra ℓ m

Addition in the group algebra (pointwise XOR, since coefficients are in ZMod 2).

Equations

• BivariateBicycle.bbAdd p q = p + q

noncomputable def BivariateBicycle.bbConvolve {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (p q : BBGroupAlgebra ℓ m) : BBGroupAlgebra ℓ m

Convolution (polynomial multiplication) in F₂[x,y]/(x^ℓ-1, y^m-1). (p * q)(γ) = Σ_{α} p(α) · q(γ - α) where subtraction is in Z_ℓ × Z_m. This corresponds to matrix multiplication of the associated circulant-like matrices.

Equations

• BivariateBicycle.bbConvolve p q γ = ∑ α : BivariateBicycle.BBMonomial ℓ m, p α * q (γ - α)

def BivariateBicycle.bbSupport {ℓ m : ℕ} (p : BBGroupAlgebra ℓ m) : Set (BBMonomial ℓ m)

The support of a polynomial: the set of monomials with nonzero coefficient.

Equations

• BivariateBicycle.bbSupport p = {α : BivariateBicycle.BBMonomial ℓ m | p α ≠ 0}

noncomputable def BivariateBicycle.bbSupportFinset {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] [DecidableEq (ZMod ℓ)] [DecidableEq (ZMod m)] (p : BBGroupAlgebra ℓ m) : Finset (BBMonomial ℓ m)

The support as a finset (decidable).

Equations

• BivariateBicycle.bbSupportFinset p = {α : BivariateBicycle.BBMonomial ℓ m | p α ≠ 0}

def BivariateBicycle.bbTranspose {ℓ m : ℕ} (p : BBGroupAlgebra ℓ m) : BBGroupAlgebra ℓ m

The transpose operation: A^T(x,y) = A(x⁻¹, y⁻¹). Since x^{-1} = x^{ℓ-1} and y^{-1} = y^{m-1} in the quotient ring, this maps the coefficient of x^a y^b to x^{-a} y^{-b}.

Equations

• BivariateBicycle.bbTranspose p α = p (-α)

Transpose properties

@[simp]

theorem BivariateBicycle.bbTranspose_involutive {ℓ m : ℕ} (p : BBGroupAlgebra ℓ m) : bbTranspose (bbTranspose p) = p

theorem BivariateBicycle.bbTranspose_bbMonomial {ℓ m : ℕ} [NeZero ℓ] [NeZero m] (a : ZMod ℓ) (b : ZMod m) : bbTranspose (bbMonomial a b) = bbMonomial (-a) (-b)

theorem BivariateBicycle.bbTranspose_add {ℓ m : ℕ} (p q : BBGroupAlgebra ℓ m) : bbTranspose (p + q) = bbTranspose p + bbTranspose q

Convolution properties

theorem BivariateBicycle.bbConvolve_comm {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (p q : BBGroupAlgebra ℓ m) : bbConvolve p q = bbConvolve q p

noncomputable instance BivariateBicycle.bbGroupAlgebraAddCommMonoid {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] : AddCommMonoid (BBGroupAlgebra ℓ m)

Equations

• BivariateBicycle.bbGroupAlgebraAddCommMonoid = Pi.addCommMonoid

The BB qubit type

@[reducible, inline]

abbrev BivariateBicycle.BBQubit (ℓ m : ℕ) : Type

The qubit type for a BB code: Left (L) qubits and Right (R) qubits, each indexed by the monomial group M = Z_ℓ × Z_m.

Equations

• BivariateBicycle.BBQubit ℓ m = (BivariateBicycle.BBMonomial ℓ m ⊕ BivariateBicycle.BBMonomial ℓ m)

theorem BivariateBicycle.bbCode_numQubits {ℓ m : ℕ} [NeZero ℓ] [NeZero m] : Fintype.card (BBQubit ℓ m) = 2 * (ℓ * m)

The number of physical qubits in a BB code is 2ℓm.

Pauli operators on BB codes

def BivariateBicycle.pauliXBB {ℓ m : ℕ} (p q : BBGroupAlgebra ℓ m) : PauliOp (BBQubit ℓ m)

The X-type Pauli operator X(p, q) on a BB code. Acts with X on L qubit γ iff p(γ) = 1, and on R qubit δ iff q(δ) = 1. This is a pure X-type operator (zVec = 0).

Equations

• BivariateBicycle.pauliXBB p q = { xVec := Sum.elim p q, zVec := 0 }

def BivariateBicycle.pauliZBB {ℓ m : ℕ} (p q : BBGroupAlgebra ℓ m) : PauliOp (BBQubit ℓ m)

The Z-type Pauli operator Z(p, q) on a BB code. Acts with Z on L qubit γ iff p(γ) = 1, and on R qubit δ iff q(δ) = 1. This is a pure Z-type operator (xVec = 0).

Equations

• BivariateBicycle.pauliZBB p q = { xVec := 0, zVec := Sum.elim p q }

@[simp]

theorem BivariateBicycle.pauliXBB_xVec_left {ℓ m : ℕ} (p q : BBGroupAlgebra ℓ m) (γ : BBMonomial ℓ m) : (pauliXBB p q).xVec (Sum.inl γ) = p γ

@[simp]

theorem BivariateBicycle.pauliXBB_xVec_right {ℓ m : ℕ} (p q : BBGroupAlgebra ℓ m) (δ : BBMonomial ℓ m) : (pauliXBB p q).xVec (Sum.inr δ) = q δ

@[simp]

theorem BivariateBicycle.pauliXBB_zVec {ℓ m : ℕ} (p q : BBGroupAlgebra ℓ m) : (pauliXBB p q).zVec = 0

@[simp]

theorem BivariateBicycle.pauliZBB_xVec {ℓ m : ℕ} (p q : BBGroupAlgebra ℓ m) : (pauliZBB p q).xVec = 0

@[simp]

theorem BivariateBicycle.pauliZBB_zVec_left {ℓ m : ℕ} (p q : BBGroupAlgebra ℓ m) (γ : BBMonomial ℓ m) : (pauliZBB p q).zVec (Sum.inl γ) = p γ

@[simp]

theorem BivariateBicycle.pauliZBB_zVec_right {ℓ m : ℕ} (p q : BBGroupAlgebra ℓ m) (δ : BBMonomial ℓ m) : (pauliZBB p q).zVec (Sum.inr δ) = q δ

The shifted polynomial: α-shift of p is p(· - α), i.e., convolution with δ_α

def BivariateBicycle.bbShift {ℓ m : ℕ} (α : BBMonomial ℓ m) (p : BBGroupAlgebra ℓ m) : BBGroupAlgebra ℓ m

Left-shift a polynomial by monomial α: (shift_α p)(γ) = p(γ - α). This corresponds to multiplication by x^a y^b in the group algebra.

Equations

• BivariateBicycle.bbShift α p γ = p (γ - α)

theorem BivariateBicycle.bbShift_zero {ℓ m : ℕ} (p : BBGroupAlgebra ℓ m) [NeZero ℓ] [NeZero m] : bbShift 0 p = p

theorem BivariateBicycle.bbShift_add {ℓ m : ℕ} (α β : BBMonomial ℓ m) (p : BBGroupAlgebra ℓ m) : bbShift α (bbShift β p) = bbShift (α + β) p

X-type and Z-type checks of the BB code

def BivariateBicycle.bbCheckX {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (α : BBMonomial ℓ m) : PauliOp (BBQubit ℓ m)

The X-type check indexed by α ∈ M. Its X-support on L qubits is the support of αA, and on R qubits is the support of αB. Using the shift representation: check (α, X) = X(shift_α A, shift_α B).

Equations

• BivariateBicycle.bbCheckX A B α = BivariateBicycle.pauliXBB (BivariateBicycle.bbShift α A) (BivariateBicycle.bbShift α B)

def BivariateBicycle.bbCheckZ {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (β : BBMonomial ℓ m) : PauliOp (BBQubit ℓ m)

The Z-type check indexed by β ∈ M. Its Z-support on L qubits is the support of βB^T, and on R qubits is the support of βA^T. Using the shift representation: check (β, Z) = Z(shift_β B^T, shift_β A^T).

Equations

• BivariateBicycle.bbCheckZ A B β = BivariateBicycle.pauliZBB (BivariateBicycle.bbShift β (BivariateBicycle.bbTranspose B)) (BivariateBicycle.bbShift β (BivariateBicycle.bbTranspose A))

@[simp]

theorem BivariateBicycle.bbCheckX_xVec_left {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (α γ : BBMonomial ℓ m) : (bbCheckX A B α).xVec (Sum.inl γ) = A (γ - α)

@[simp]

theorem BivariateBicycle.bbCheckX_xVec_right {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (α δ : BBMonomial ℓ m) : (bbCheckX A B α).xVec (Sum.inr δ) = B (δ - α)

@[simp]

theorem BivariateBicycle.bbCheckX_zVec {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (α : BBMonomial ℓ m) : (bbCheckX A B α).zVec = 0

@[simp]

theorem BivariateBicycle.bbCheckZ_xVec {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (β : BBMonomial ℓ m) : (bbCheckZ A B β).xVec = 0

@[simp]

theorem BivariateBicycle.bbCheckZ_zVec_left {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (β γ : BBMonomial ℓ m) : (bbCheckZ A B β).zVec (Sum.inl γ) = B (-(γ - β))

@[simp]

theorem BivariateBicycle.bbCheckZ_zVec_right {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (β δ : BBMonomial ℓ m) : (bbCheckZ A B β).zVec (Sum.inr δ) = A (-(δ - β))

X checks are pure X-type, Z checks are pure Z-type

theorem BivariateBicycle.bbCheckX_pure_X {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (α : BBMonomial ℓ m) : (bbCheckX A B α).zVec = 0

theorem BivariateBicycle.bbCheckZ_pure_Z {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (β : BBMonomial ℓ m) : (bbCheckZ A B β).xVec = 0

CSS commutation: X checks commute with Z checks

theorem BivariateBicycle.bbCheckX_commute {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (α₁ α₂ : BBMonomial ℓ m) : (bbCheckX A B α₁).PauliCommute (bbCheckX A B α₂)

X checks commute with each other (both pure X, so symplectic inner product = 0).

theorem BivariateBicycle.bbCheckZ_commute {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (β₁ β₂ : BBMonomial ℓ m) : (bbCheckZ A B β₁).PauliCommute (bbCheckZ A B β₂)

Z checks commute with each other (both pure Z, so symplectic inner product = 0).

theorem BivariateBicycle.bbCheckXZ_commute_iff {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (α β : BBMonomial ℓ m) : (bbCheckX A B α).PauliCommute (bbCheckZ A B β) ↔ ∑ γ : BBMonomial ℓ m, A (γ - α) * B (-(γ - β)) + ∑ δ : BBMonomial ℓ m, B (δ - α) * A (-(δ - β)) = 0

The CSS commutation condition: X check α commutes with Z check β iff Σ_γ A(γ-α)·B(-γ+β) + Σ_δ B(δ-α)·A(-δ+β) = 0 in ZMod 2. This is the condition H_X · H_Z^T = 0, equivalently A·B^T = B·A^T.

The CSS condition: AB^T = BA^T (in the group algebra)

def BivariateBicycle.BBCSSCondition {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) : Prop

The CSS condition for a BB code: A * B^T = B * A^T as convolutions. This is the necessary and sufficient condition for all X and Z checks to commute.

Equations

• BivariateBicycle.BBCSSCondition A B = (BivariateBicycle.bbConvolve A (BivariateBicycle.bbTranspose B) = BivariateBicycle.bbConvolve B (BivariateBicycle.bbTranspose A))

theorem BivariateBicycle.bbChecksXZ_commute_of_css {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (_hcss : BBCSSCondition A B) (α β : BBMonomial ℓ m) : (bbCheckX A B α).PauliCommute (bbCheckZ A B β)

Under the CSS condition, all X and Z checks commute. In fact, for BB codes over abelian groups the commutation is automatic: each sum equals the convolution bbConvolve evaluated at β-α, and by commutativity of convolution their sum vanishes in characteristic 2.

The BB code check index and the full stabilizer code

@[reducible, inline]

abbrev BivariateBicycle.BBCheckIndex (ℓ m : ℕ) : Type

Check index for a BB code: X checks indexed by M, Z checks indexed by M.

Equations

• BivariateBicycle.BBCheckIndex ℓ m = (BivariateBicycle.BBMonomial ℓ m ⊕ BivariateBicycle.BBMonomial ℓ m)

theorem BivariateBicycle.bbCode_numChecks {ℓ m : ℕ} [NeZero ℓ] [NeZero m] : Fintype.card (BBCheckIndex ℓ m) = 2 * (ℓ * m)

The number of checks in a BB code is 2ℓm.

def BivariateBicycle.bbCheck {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) : BBCheckIndex ℓ m → PauliOp (BBQubit ℓ m)

The check map for a BB code: X checks on the left, Z checks on the right.

Equations

• BivariateBicycle.bbCheck A B (Sum.inl α) = BivariateBicycle.bbCheckX A B α
• BivariateBicycle.bbCheck A B (Sum.inr β) = BivariateBicycle.bbCheckZ A B β

theorem BivariateBicycle.bbChecks_commute {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (hcss : BBCSSCondition A B) (i j : BBCheckIndex ℓ m) : (bbCheck A B i).PauliCommute (bbCheck A B j)

Under the CSS condition, all checks in a BB code pairwise commute.

noncomputable def BivariateBicycle.BBCode {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] [DecidableEq (ZMod ℓ)] [DecidableEq (ZMod m)] (A B : BBGroupAlgebra ℓ m) (hcss : BBCSSCondition A B) : StabilizerCode (BBQubit ℓ m)

A BB code forms a valid stabilizer code under the CSS condition.

Equations

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

Properties of the cyclic shift operators x and y

def BivariateBicycle.xShift {ℓ m : ℕ} [NeZero ℓ] [NeZero m] : BBMonomial ℓ m

The x-shift operator: multiplication by x = x^1 y^0 in the group algebra. Maps coefficient at (a, b) to (a-1, b), i.e., shifts the first coordinate.

Equations

• BivariateBicycle.xShift = (1, 0)

def BivariateBicycle.yShift {ℓ m : ℕ} [NeZero ℓ] [NeZero m] : BBMonomial ℓ m

The y-shift operator: multiplication by y = x^0 y^1 in the group algebra. Maps coefficient at (a, b) to (a, b-1), i.e., shifts the second coordinate.

Equations

• BivariateBicycle.yShift = (0, 1)

@[simp]

theorem BivariateBicycle.xShift_pow_ℓ {ℓ m : ℕ} [NeZero ℓ] [NeZero m] : ℓ • xShift = 0

x^ℓ = 1: shifting by ℓ in the first coordinate is the identity (mod ℓ).

@[simp]

theorem BivariateBicycle.yShift_pow_m {ℓ m : ℕ} [NeZero ℓ] [NeZero m] : m • yShift = 0

y^m = 1: shifting by m in the second coordinate is the identity (mod m).

theorem BivariateBicycle.xShift_yShift_comm {ℓ m : ℕ} [NeZero ℓ] [NeZero m] : xShift + yShift = yShift + xShift

x and y commute: the monomial group is abelian.

Transpose as variable inversion

theorem BivariateBicycle.bbTranspose_eq_neg {ℓ m : ℕ} (p : BBGroupAlgebra ℓ m) (γ : BBMonomial ℓ m) : bbTranspose p γ = p (-γ)

The transpose satisfies A^T(γ) = A(-γ), which corresponds to substituting x → x⁻¹ = x^{ℓ-1} and y → y⁻¹ = y^{m-1}.

theorem BivariateBicycle.bbTranspose_monomial_neg {ℓ m : ℕ} [NeZero ℓ] [NeZero m] (a : ZMod ℓ) (b : ZMod m) (γ : BBMonomial ℓ m) : bbTranspose (bbMonomial a b) γ = bbMonomial (-a) (-b) γ

Transpose of a monomial: (x^a y^b)^T = x^{-a} y^{-b}.

Convolution distributes over transposition

theorem BivariateBicycle.bbConvolve_transpose {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (p q : BBGroupAlgebra ℓ m) : bbTranspose (bbConvolve p q) = bbConvolve (bbTranspose q) (bbTranspose p)

The labeling convention

@[reducible, inline]

abbrev BivariateBicycle.leftQubit {ℓ m : ℕ} (γ : BBMonomial ℓ m) : BBQubit ℓ m

Left qubit labeled by γ ∈ M.

Equations

• BivariateBicycle.leftQubit γ = Sum.inl γ

@[reducible, inline]

abbrev BivariateBicycle.rightQubit {ℓ m : ℕ} (δ : BBMonomial ℓ m) : BBQubit ℓ m

Right qubit labeled by δ ∈ M.

Equations

• BivariateBicycle.rightQubit δ = Sum.inr δ

@[reducible, inline]

abbrev BivariateBicycle.xCheckIndex {ℓ m : ℕ} (α : BBMonomial ℓ m) : BBCheckIndex ℓ m

X check labeled by α ∈ M.

Equations

• BivariateBicycle.xCheckIndex α = Sum.inl α

@[reducible, inline]

abbrev BivariateBicycle.zCheckIndex {ℓ m : ℕ} (β : BBMonomial ℓ m) : BBCheckIndex ℓ m

Z check labeled by β ∈ M.

Equations

• BivariateBicycle.zCheckIndex β = Sum.inr β

@[simp]

theorem BivariateBicycle.bbCheck_xCheck {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (α : BBMonomial ℓ m) : bbCheck A B (xCheckIndex α) = bbCheckX A B α

The check at index (α, X) is the X check for α.

@[simp]

theorem BivariateBicycle.bbCheck_zCheck {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (β : BBMonomial ℓ m) : bbCheck A B (zCheckIndex β) = bbCheckZ A B β

The check at index (β, Z) is the Z check for β.

The CSS condition is equivalent to AB^T = BA^T

theorem BivariateBicycle.bbCSSCondition_iff {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) : BBCSSCondition A B ↔ ∀ (γ : BBMonomial ℓ m), ∑ α : BBMonomial ℓ m, A α * B (α - γ) = ∑ α : BBMonomial ℓ m, B α * A (α - γ)

The CSS condition states that A * B^T = B * A^T in the group algebra. This ensures the parity check matrices H_X and H_Z satisfy H_X · H_Z^T = 0. Equivalently: for every γ ∈ M, Σ_α A(α) · B(α - γ) = Σ_α B(α) · A(α - γ).

Pauli notation properties

theorem BivariateBicycle.pauliXBB_pure_X {ℓ m : ℕ} (p q : BBGroupAlgebra ℓ m) : (pauliXBB p q).zVec = 0

X(p, q) is pure X-type.

theorem BivariateBicycle.pauliZBB_pure_Z {ℓ m : ℕ} (p q : BBGroupAlgebra ℓ m) : (pauliZBB p q).xVec = 0

Z(p, q) is pure Z-type.

@[simp]

theorem BivariateBicycle.pauliXBB_zero {ℓ m : ℕ} : pauliXBB 0 0 = 1

X(0, 0) is the identity operator.

@[simp]

theorem BivariateBicycle.pauliZBB_zero {ℓ m : ℕ} : pauliZBB 0 0 = 1

Z(0, 0) is the identity operator.

theorem BivariateBicycle.pauliXBB_mul {ℓ m : ℕ} (p₁ q₁ p₂ q₂ : BBGroupAlgebra ℓ m) : pauliXBB p₁ q₁ * pauliXBB p₂ q₂ = pauliXBB (p₁ + p₂) (q₁ + q₂)

X(p₁, q₁) · X(p₂, q₂) = X(p₁ + p₂, q₁ + q₂) as Pauli operators (since X-type operators multiply by adding their binary vectors).

theorem BivariateBicycle.pauliZBB_mul {ℓ m : ℕ} (p₁ q₁ p₂ q₂ : BBGroupAlgebra ℓ m) : pauliZBB p₁ q₁ * pauliZBB p₂ q₂ = pauliZBB (p₁ + p₂) (q₁ + q₂)

Z(p₁, q₁) · Z(p₂, q₂) = Z(p₁ + p₂, q₁ + q₂).

theorem BivariateBicycle.pauliXBB_pauliXBB_commute {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (p₁ q₁ p₂ q₂ : BBGroupAlgebra ℓ m) : (pauliXBB p₁ q₁).PauliCommute (pauliXBB p₂ q₂)

Two X-type Pauli operators always commute.

theorem BivariateBicycle.pauliZBB_pauliZBB_commute {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (p₁ q₁ p₂ q₂ : BBGroupAlgebra ℓ m) : (pauliZBB p₁ q₁).PauliCommute (pauliZBB p₂ q₂)

Two Z-type Pauli operators always commute.

theorem BivariateBicycle.symplecticInner_pauliXBB_pauliZBB {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (p₁ q₁ p₂ q₂ : BBGroupAlgebra ℓ m) : (pauliXBB p₁ q₁).symplecticInner (pauliZBB p₂ q₂) = ∑ γ : BBMonomial ℓ m, p₁ γ * p₂ γ + ∑ δ : BBMonomial ℓ m, q₁ δ * q₂ δ

The symplectic inner product of X(p₁,q₁) and Z(p₂,q₂) equals Σ_γ p₁(γ)·p₂(γ) + Σ_δ q₁(δ)·q₂(δ), which is ⟨p₁,p₂⟩ + ⟨q₁,q₂⟩ where ⟨·,·⟩ is the standard inner product in ZMod 2.

X check is exactly X(shift_α A, shift_α B)

theorem BivariateBicycle.bbCheckX_eq_pauliXBB {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (α : BBMonomial ℓ m) : bbCheckX A B α = pauliXBB (bbShift α A) (bbShift α B)

theorem BivariateBicycle.bbCheckZ_eq_pauliZBB {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (β : BBMonomial ℓ m) : bbCheckZ A B β = pauliZBB (bbShift β (bbTranspose B)) (bbShift β (bbTranspose A))

Z check is exactly Z(shift_β B^T, shift_β A^T).

Monomial group cardinality

theorem BivariateBicycle.bbMonomial_card {ℓ m : ℕ} [NeZero ℓ] [NeZero m] : Fintype.card (BBMonomial ℓ m) = ℓ * m

The monomial group has ℓm elements.

Check acts on qubit characterization

theorem BivariateBicycle.bbCheckX_acts_on_left {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (α γ : BBMonomial ℓ m) : (bbCheckX A B α).xVec (Sum.inl γ) = A (γ - α)

X check (α, X) acts on L qubit γ iff A(γ - α) = 1, i.e., γ is in the support of the shifted polynomial αA.

theorem BivariateBicycle.bbCheckX_acts_on_right {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (α δ : BBMonomial ℓ m) : (bbCheckX A B α).xVec (Sum.inr δ) = B (δ - α)

X check (α, X) acts on R qubit δ iff B(δ - α) = 1, i.e., δ is in the support of the shifted polynomial αB.

theorem BivariateBicycle.bbCheckZ_acts_on_left {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (β γ : BBMonomial ℓ m) : (bbCheckZ A B β).zVec (Sum.inl γ) = B (β - γ)

Z check (β, Z) acts on L qubit γ iff B^T(γ - β) = B(β - γ) = 1, i.e., γ is in the support of the shifted polynomial β B^T.

theorem BivariateBicycle.bbCheckZ_acts_on_right {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (β δ : BBMonomial ℓ m) : (bbCheckZ A B β).zVec (Sum.inr δ) = A (β - δ)

Z check (β, Z) acts on R qubit δ iff A^T(δ - β) = A(β - δ) = 1, i.e., δ is in the support of the shifted polynomial β A^T.

Self-inverse properties

theorem BivariateBicycle.bbCheckX_mul_self {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (α : BBMonomial ℓ m) : bbCheckX A B α * bbCheckX A B α = 1

X checks are self-inverse: (α, X) · (α, X) = I.

theorem BivariateBicycle.bbCheckZ_mul_self {ℓ m : ℕ} [Fintype (ZMod ℓ)] [Fintype (ZMod m)] (A B : BBGroupAlgebra ℓ m) (β : BBMonomial ℓ m) : bbCheckZ A B β * bbCheckZ A B β = 1

Z checks are self-inverse: (β, Z) · (β, Z) = I.