41 Rem 19: Bivariate Bicycle Code Notation
The Bivariate Bicycle (BB) code construction uses cyclic permutation matrices and their tensor products to define CSS codes on \(2\ell m\) qubits. This remark introduces the group algebra \(\mathbb {F}_2[x,y]/(x^\ell - 1, y^m - 1)\), defines the X-type and Z-type parity checks, and constructs the BB code as a stabilizer code under the CSS condition \(AB^T = BA^T\).
The monomial group \(M = \mathbb {Z}_\ell \times \mathbb {Z}_m\) represents monomials \(x^a y^b\) with \(a \in \{ 0, \ldots , \ell -1\} \) and \(b \in \{ 0, \ldots , m-1\} \). We use the additive group structure of \(\mathbb {Z}_\ell \times \mathbb {Z}_m\) (addition corresponds to monomial multiplication).
The group algebra \(\mathbb {F}_2[x,y]/(x^\ell - 1, y^m - 1)\). An element is a function \(M \to \mathbb {Z}/2\mathbb {Z}\), where the value at \((a,b)\) is the coefficient of \(x^a y^b\).
The monomial \(x^a y^b\) as an element of the group algebra: the indicator function of the single element \((a, b)\). That is, \(\operatorname {bbMonomial}(a, b)(\gamma ) = 1\) if \(\gamma = (a, b)\) and \(0\) otherwise.
The zero polynomial in the group algebra, mapping every monomial to \(0\).
The unit polynomial \(1 = x^0 y^0\) in the group algebra, defined as \(\operatorname {bbMonomial}(0, 0)\).
Addition in the group algebra, given by pointwise XOR (since coefficients are in \(\mathbb {Z}/2\mathbb {Z}\)). For polynomials \(p, q\), \((p + q)(\gamma ) = p(\gamma ) + q(\gamma )\).
Convolution (polynomial multiplication) in \(\mathbb {F}_2[x,y]/(x^\ell - 1, y^m - 1)\). For polynomials \(p, q\):
where subtraction is taken in \(\mathbb {Z}_\ell \times \mathbb {Z}_m\). This corresponds to matrix multiplication of the associated circulant-like matrices.
The support of a polynomial \(p\): the set of monomials with nonzero coefficient, \(\operatorname {supp}(p) = \{ \alpha \in M \mid p(\alpha ) \neq 0 \} \).
The support of a polynomial as a finite set (decidable version), obtained by filtering the universe of \(M\) for monomials \(\alpha \) with \(p(\alpha ) \neq 0\).
The transpose operation on the group algebra: \(A^T(x,y) = A(x^{-1}, y^{-1})\). Since \(x^{-1} = x^{\ell -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}\). Formally, \(\operatorname {bbTranspose}(p)(\alpha ) = p(-\alpha )\).
For any polynomial \(p\) in the group algebra, \(\operatorname {bbTranspose}(\operatorname {bbTranspose}(p)) = p\).
By extensionality, it suffices to show equality for an arbitrary \(\alpha \). By definition of transpose, \(\operatorname {bbTranspose}(\operatorname {bbTranspose}(p))(\alpha ) = \operatorname {bbTranspose}(p)(-\alpha ) = p(-(-\alpha )) = p(\alpha )\), using \(-(-\alpha ) = \alpha \).
For \(a \in \mathbb {Z}_\ell \) and \(b \in \mathbb {Z}_m\), \(\operatorname {bbTranspose}(\operatorname {bbMonomial}(a,b)) = \operatorname {bbMonomial}(-a, -b)\).
By extensionality on pairs \((c, d)\). We unfold the definitions of transpose and monomial. The condition \(-\alpha = (a, b)\) is equivalent to \(\alpha = (-a, -b)\) by applying \(\operatorname {neg\_ eq\_ iff\_ eq\_ neg}\).
For polynomials \(p, q\) in the group algebra, \(\operatorname {bbTranspose}(p + q) = \operatorname {bbTranspose}(p) + \operatorname {bbTranspose}(q)\).
By extensionality on \(\alpha \). We compute \(\operatorname {bbTranspose}(p + q)(\alpha ) = (p + q)(-\alpha ) = p(-\alpha ) + q(-\alpha ) = \operatorname {bbTranspose}(p)(\alpha ) + \operatorname {bbTranspose}(q)(\alpha )\), using the pointwise addition of functions.
For polynomials \(p, q\) in the group algebra, \(p * q = q * p\) (convolution is commutative because the monomial group is abelian).
By extensionality on \(\gamma \). We unfold the definition of convolution. We reindex the left-hand side sum with \(\beta = \gamma - \alpha \) (so \(\alpha = \gamma - \beta \)) using the equivalence \(\operatorname {Equiv.subLeft}(\gamma )\), obtaining \(\sum _\alpha p(\alpha ) \cdot q(\gamma - \alpha ) = \sum _\beta p(\gamma - \beta ) \cdot q(\beta )\). We then apply commutativity of multiplication in \(\mathbb {Z}/2\mathbb {Z}\) to each term, giving \(\sum _\beta q(\beta ) \cdot p(\gamma - \beta ) = (q * p)(\gamma )\).
The qubit type for a BB code: Left (L) qubits and Right (R) qubits, each indexed by the monomial group \(M = \mathbb {Z}_\ell \times \mathbb {Z}_m\). Formally, \(\operatorname {BBQubit}(\ell , m) = M \oplus M\).
The number of physical qubits in a BB code is \(|\operatorname {BBQubit}(\ell , m)| = 2\ell m\).
By simplification using the cardinality of sum types, product types, and \(|\mathbb {Z}_n| = n\). We have \(|\operatorname {BBQubit}(\ell , m)| = |M| + |M| = 2|M| = 2(\ell \cdot m)\).
The X-type Pauli operator \(X(p, q)\) on a BB code. It acts with \(X\) on L qubit \(\gamma \) iff \(p(\gamma ) = 1\), and on R qubit \(\delta \) iff \(q(\delta ) = 1\). This is a pure X-type operator (\(z\)-vector \(= 0\)). Formally: \(\operatorname {xVec} = \operatorname {Sum.elim}(p, q)\) and \(\operatorname {zVec} = 0\).
The Z-type Pauli operator \(Z(p, q)\) on a BB code. It acts with \(Z\) on L qubit \(\gamma \) iff \(p(\gamma ) = 1\), and on R qubit \(\delta \) iff \(q(\delta ) = 1\). This is a pure Z-type operator (\(x\)-vector \(= 0\)). Formally: \(\operatorname {xVec} = 0\) and \(\operatorname {zVec} = \operatorname {Sum.elim}(p, q)\).
Left-shift a polynomial by monomial \(\alpha \): \((\operatorname {shift}_\alpha \, p)(\gamma ) = p(\gamma - \alpha )\). This corresponds to multiplication by \(x^a y^b\) in the group algebra.
For any polynomial \(p\), \(\operatorname {shift}_0\, p = p\).
By extensionality on \(\gamma \). We have \(\operatorname {shift}_0(p)(\gamma ) = p(\gamma - 0) = p(\gamma )\) by simplification.
For monomials \(\alpha , \beta \) and polynomial \(p\), \(\operatorname {shift}_\alpha (\operatorname {shift}_\beta \, p) = \operatorname {shift}_{\alpha + \beta }\, p\).
By extensionality on \(\gamma \). Unfolding the definition, the left-hand side gives \(p((\gamma - \alpha ) - \beta )\) and the right-hand side gives \(p(\gamma - (\alpha + \beta ))\). These are equal since \((\gamma - \alpha ) - \beta = \gamma - (\alpha + \beta )\) by the associativity of subtraction.
The X-type check indexed by \(\alpha \in M\) for polynomials \(A, B\). Its X-support on L qubits is the support of \(\operatorname {shift}_\alpha A\), and on R qubits is the support of \(\operatorname {shift}_\alpha B\):
The Z-type check indexed by \(\beta \in M\) for polynomials \(A, B\). Its Z-support on L qubits is the support of \(\operatorname {shift}_\beta B^T\), and on R qubits is the support of \(\operatorname {shift}_\beta A^T\):
For any polynomials \(A, B\) and index \(\alpha \in M\), the X check \(\operatorname {bbCheckX}(A, B, \alpha )\) has \(z\)-vector equal to \(0\).
This holds by definitional equality (reflexivity), since the X check is constructed as \(\operatorname {pauliXBB}\) which has \(\operatorname {zVec} = 0\).
For any polynomials \(A, B\) and index \(\beta \in M\), the Z check \(\operatorname {bbCheckZ}(A, B, \beta )\) has \(x\)-vector equal to \(0\).
This holds by definitional equality (reflexivity), since the Z check is constructed as \(\operatorname {pauliZBB}\) which has \(\operatorname {xVec} = 0\).
For any polynomials \(A, B\) and indices \(\alpha _1, \alpha _2 \in M\), \(\operatorname {bbCheckX}(A, B, \alpha _1)\) and \(\operatorname {bbCheckX}(A, B, \alpha _2)\) commute.
Both checks are pure X-type, so their \(z\)-vectors are zero. The symplectic inner product \(\langle P_1, P_2 \rangle = \sum _i (x_1(i) \cdot z_2(i) + z_1(i) \cdot x_2(i))\) vanishes since all \(z\)-components are zero. By simplification using the definition of \(\operatorname {PauliCommute}\) and \(\operatorname {symplecticInner}\) with \(\operatorname {zVec} = 0\), the result follows.
For any polynomials \(A, B\) and indices \(\beta _1, \beta _2 \in M\), \(\operatorname {bbCheckZ}(A, B, \beta _1)\) and \(\operatorname {bbCheckZ}(A, B, \beta _2)\) commute.
Both checks are pure Z-type, so their \(x\)-vectors are zero. The symplectic inner product vanishes since all \(x\)-components are zero. By simplification using the definition of \(\operatorname {PauliCommute}\) and \(\operatorname {symplecticInner}\) with \(\operatorname {xVec} = 0\), the result follows.
The X check at \(\alpha \) commutes with the Z check at \(\beta \) if and only if
This is the condition \(H_X \cdot H_Z^T = 0\), equivalently \(AB^T = BA^T\).
We unfold the definitions of \(\operatorname {PauliCommute}\) and \(\operatorname {symplecticInner}\). For both directions we convert using the sum decomposition over the sum type (L and R qubits), and simplify the components using the definitions of \(\operatorname {bbCheckX}\), \(\operatorname {bbCheckZ}\), \(\operatorname {pauliXBB}\), \(\operatorname {pauliZBB}\), \(\operatorname {bbShift}\), and \(\operatorname {bbTranspose}\).
The CSS condition for a BB code states that \(A * B^T = B * A^T\) as convolutions in the group algebra. This is the necessary and sufficient condition for all X and Z checks to commute, ensuring the parity check matrices satisfy \(H_X \cdot H_Z^T = 0\).
Under the CSS condition \(AB^T = BA^T\), for all \(\alpha , \beta \in M\), the X check at \(\alpha \) commutes with the Z check at \(\beta \). In fact, for BB codes over abelian groups the commutation is automatic: each sum equals the convolution evaluated at \(\beta - \alpha \), and by commutativity of convolution their sum vanishes in characteristic \(2\).
We rewrite using the XZ commutation characterization. We need to show \(\sum _\gamma A(\gamma - \alpha ) \cdot B(-(\gamma - \beta )) + \sum _\delta B(\delta - \alpha ) \cdot A(-(\delta - \beta )) = 0\). We establish that the first sum equals \(\operatorname {bbConvolve}(A, B)(\beta - \alpha )\) by reindexing with \(\delta = \gamma - \alpha \) using \(\operatorname {Equiv.addRight}(\alpha )\) and simplifying \(B(-(\gamma - \beta )) = B((\beta - \alpha ) - \delta )\) by abelian group arithmetic. Similarly, the second sum equals \(\operatorname {bbConvolve}(B, A)(\beta - \alpha )\). Rewriting using commutativity of convolution (\(\operatorname {bbConvolve\_ comm}\)), both sums are equal, so their sum in \(\mathbb {Z}/2\mathbb {Z}\) is \(0\) by \(\operatorname {CharTwo.add\_ self\_ eq\_ zero}\).
The check index type for a BB code: X checks indexed by \(M\) (left summand) and Z checks indexed by \(M\) (right summand). Formally, \(\operatorname {BBCheckIndex}(\ell , m) = M \oplus M\).
The number of checks in a BB code is \(|\operatorname {BBCheckIndex}(\ell , m)| = 2\ell m\).
By simplification using the cardinality of sum types, product types, and \(|\mathbb {Z}_n| = n\). We have \(|\operatorname {BBCheckIndex}(\ell , m)| = |M| + |M| = 2|M| = 2(\ell \cdot m)\).
The check map for a BB code: given polynomials \(A, B\), it maps X check indices (left summand) to \(\operatorname {bbCheckX}(A, B, \alpha )\) and Z check indices (right summand) to \(\operatorname {bbCheckZ}(A, B, \beta )\).
Under the CSS condition \(AB^T = BA^T\), all checks in a BB code pairwise commute. That is, for all check indices \(i, j\), \(\operatorname {PauliCommute}(\operatorname {bbCheck}(A, B, i),\, \operatorname {bbCheck}(A, B, j))\).
We case-split on the check indices \(i\) and \(j\). Case \(i = (\alpha _1, X)\), \(j = (\alpha _2, X)\): This follows from \(\operatorname {bbCheckX\_ commute}\). Case \(i = (\alpha , X)\), \(j = (\beta , Z)\): This follows from \(\operatorname {bbChecksXZ\_ commute\_ of\_ css}\). Case \(i = (\beta , Z)\), \(j = (\alpha , X)\): We apply commutativity of \(\operatorname {PauliCommute}\) and then use \(\operatorname {bbChecksXZ\_ commute\_ of\_ css}\). Case \(i = (\beta _1, Z)\), \(j = (\beta _2, Z)\): This follows from \(\operatorname {bbCheckZ\_ commute}\).
A BB code forms a valid stabilizer code under the CSS condition \(AB^T = BA^T\). Given polynomials \(A, B\) in the group algebra satisfying the CSS condition, the stabilizer code has:
Qubit type: \(\operatorname {BBQubit}(\ell , m) = M \oplus M\),
Check index: \(\operatorname {BBCheckIndex}(\ell , m) = M \oplus M\),
Check map: \(\operatorname {bbCheck}(A, B)\),
Commutation: guaranteed by \(\operatorname {bbChecks\_ commute}\).
The \(x\)-shift operator: the monomial \(x = x^1 y^0\) in the monomial group, represented as \((1, 0) \in \mathbb {Z}_\ell \times \mathbb {Z}_m\). Shifting by this monomial maps the coefficient at \((a, b)\) to \((a-1, b)\).
The \(y\)-shift operator: the monomial \(y = x^0 y^1\) in the monomial group, represented as \((0, 1) \in \mathbb {Z}_\ell \times \mathbb {Z}_m\). Shifting by this monomial maps the coefficient at \((a, b)\) to \((a, b-1)\).
Shifting by \(\ell \) in the first coordinate is the identity modulo \(\ell \): \(\ell \cdot \operatorname {xShift} = 0\) in the monomial group.
By simplification. We compute \(\ell \cdot (1, 0) = (\ell , 0) = (0, 0)\) in \(\mathbb {Z}_\ell \times \mathbb {Z}_m\), using \(\ell \equiv 0 \pmod{\ell }\).
Shifting by \(m\) in the second coordinate is the identity modulo \(m\): \(m \cdot \operatorname {yShift} = 0\) in the monomial group.
By simplification. We compute \(m \cdot (0, 1) = (0, m) = (0, 0)\) in \(\mathbb {Z}_\ell \times \mathbb {Z}_m\), using \(m \equiv 0 \pmod{m}\).
The monomial group is abelian: \(\operatorname {xShift} + \operatorname {yShift} = \operatorname {yShift} + \operatorname {xShift}\).
By simplification. We unfold the definitions to get \((1, 0) + (0, 1) = (0, 1) + (1, 0)\), which holds by commutativity of addition in each component.
The transpose satisfies \(A^T(\gamma ) = A(-\gamma )\), which corresponds to substituting \(x \to x^{-1} = x^{\ell -1}\) and \(y \to y^{-1} = y^{m-1}\).
This holds by definitional equality (reflexivity).
Transpose of a monomial: \((x^a y^b)^T = x^{-a} y^{-b}\). Formally, for all \(\gamma \), \(\operatorname {bbTranspose}(\operatorname {bbMonomial}(a, b))(\gamma ) = \operatorname {bbMonomial}(-a, -b)(\gamma )\).
We unfold the definitions of transpose and monomial and split on the conditional. There are four cases depending on whether \(-\gamma = (a, b)\) and whether \(\gamma = (-a, -b)\). When \(-\gamma = (a, b)\) but \(\gamma \neq (-a, -b)\), we derive a contradiction from \(\gamma = -(-\gamma ) = -(a,b) = (-a, -b)\) by double negation. The symmetric case is handled by applying negation to the pair equality. The two remaining cases (both true or both false) are immediate.
For polynomials \(p, q\) in the group algebra, \(\operatorname {bbTranspose}(p * q) = q^T * p^T\).
By extensionality on \(\gamma \). The left-hand side is \((p * q)(-\gamma ) = \sum _\alpha p(\alpha ) \cdot q(-\gamma - \alpha )\). We reindex with \(\beta = -\gamma - \alpha \) (so \(\alpha = -\gamma - \beta \)) using \(\operatorname {Equiv.subLeft}(-\gamma )\), obtaining \(\sum _\beta p(-\gamma - \beta ) \cdot q(\beta )\). The right-hand side is \(\sum _\alpha q(-\alpha ) \cdot p(-(\gamma - \alpha ))\). We reindex with \(\beta = -\alpha \) (so \(\alpha = -\beta \)) using \(\operatorname {Equiv.neg}\), obtaining \(\sum _\beta q(\beta ) \cdot p(-\gamma - \beta )\). The two expressions are equal by commutativity of multiplication in \(\mathbb {Z}/2\mathbb {Z}\).
Left qubit labeled by \(\gamma \in M\), defined as \(\operatorname {Sum.inl}(\gamma )\) in the qubit type \(M \oplus M\).
Right qubit labeled by \(\delta \in M\), defined as \(\operatorname {Sum.inr}(\delta )\) in the qubit type \(M \oplus M\).
X check labeled by \(\alpha \in M\), defined as \(\operatorname {Sum.inl}(\alpha )\) in the check index type \(M \oplus M\).
Z check labeled by \(\beta \in M\), defined as \(\operatorname {Sum.inr}(\beta )\) in the check index type \(M \oplus M\).
The CSS condition \(AB^T = BA^T\) is equivalent to: for every \(\gamma \in M\),
This ensures the parity check matrices \(H_X\) and \(H_Z\) satisfy \(H_X \cdot H_Z^T = 0\).
We unfold the definitions of \(\operatorname {BBCSSCondition}\), \(\operatorname {bbConvolve}\), and \(\operatorname {bbTranspose}\), and use function extensionality. For both directions, the key step is converting between the convolution form \(\sum _\alpha p(\alpha ) \cdot q(-(\gamma - \alpha ))\) and the stated form \(\sum _\alpha p(\alpha ) \cdot q(\alpha - \gamma )\) by the abelian group identity \(-(\gamma - \alpha ) = \alpha - \gamma \).
For any polynomials \(p, q\), the operator \(X(p, q)\) satisfies \(\operatorname {zVec} = 0\).
This holds by definitional equality (reflexivity).
For any polynomials \(p, q\), the operator \(Z(p, q)\) satisfies \(\operatorname {xVec} = 0\).
This holds by definitional equality (reflexivity).
The operator \(X(0, 0)\) is the identity Pauli operator.
By extensionality on qubit indices. For the \(x\)-vector, we case-split on left and right qubits: in both cases, \(\operatorname {Sum.elim}(0, 0)\) evaluates to \(0\), matching the identity. For the \(z\)-vector, \(\operatorname {pauliXBB}\) has \(\operatorname {zVec} = 0\) by definition, matching the identity.
The operator \(Z(0, 0)\) is the identity Pauli operator.
By extensionality on qubit indices. For the \(x\)-vector, \(\operatorname {pauliZBB}\) has \(\operatorname {xVec} = 0\) by definition. For the \(z\)-vector, we case-split on left and right qubits: in both cases, \(\operatorname {Sum.elim}(0, 0)\) evaluates to \(0\), matching the identity.
\(X(p_1, q_1) \cdot X(p_2, q_2) = X(p_1 + p_2, q_1 + q_2)\) as Pauli operators (X-type operators multiply by adding their binary vectors).
By extensionality on qubit indices \(v\). For the \(x\)-vector, we case-split: for left qubits \(\operatorname {Sum.inl}(\gamma )\), both sides give \(p_1(\gamma ) + p_2(\gamma )\); for right qubits \(\operatorname {Sum.inr}(\delta )\), both sides give \(q_1(\delta ) + q_2(\delta )\). For the \(z\)-vector, we case-split similarly: both sides give \(0 + 0 = 0\) for each qubit, since both operators are pure X-type.
\(Z(p_1, q_1) \cdot Z(p_2, q_2) = Z(p_1 + p_2, q_1 + q_2)\).
By extensionality on qubit indices \(v\). For the \(x\)-vector, we case-split: both sides give \(0 + 0 = 0\) for each qubit, since both operators are pure Z-type. For the \(z\)-vector, we case-split: for left qubits \(\operatorname {Sum.inl}(\gamma )\), both sides give \(p_1(\gamma ) + p_2(\gamma )\); for right qubits \(\operatorname {Sum.inr}(\delta )\), both sides give \(q_1(\delta ) + q_2(\delta )\).
Two X-type Pauli operators always commute: \(\operatorname {PauliCommute}(X(p_1, q_1), X(p_2, q_2))\).
By simplification. Both operators have \(\operatorname {zVec} = 0\), so the symplectic inner product \(\sum _i (x_1(i) \cdot z_2(i) + z_1(i) \cdot x_2(i)) = \sum _i (x_1(i) \cdot 0 + 0 \cdot x_2(i)) = 0\).
Two Z-type Pauli operators always commute: \(\operatorname {PauliCommute}(Z(p_1, q_1), Z(p_2, q_2))\).
By simplification. Both operators have \(\operatorname {xVec} = 0\), so the symplectic inner product \(\sum _i (x_1(i) \cdot z_2(i) + z_1(i) \cdot x_2(i)) = \sum _i (0 \cdot z_2(i) + z_1(i) \cdot 0) = 0\).
The symplectic inner product of \(X(p_1, q_1)\) and \(Z(p_2, q_2)\) equals
which is \(\langle p_1, p_2 \rangle + \langle q_1, q_2 \rangle \) where \(\langle \cdot , \cdot \rangle \) is the standard inner product in \(\mathbb {Z}/2\mathbb {Z}\).
We unfold the definitions of \(\operatorname {symplecticInner}\), \(\operatorname {pauliXBB}\), and \(\operatorname {pauliZBB}\). Since \(X(p_1, q_1)\) has \(\operatorname {zVec} = 0\) and \(Z(p_2, q_2)\) has \(\operatorname {xVec} = 0\), the cross terms vanish. The remaining sum over \(\operatorname {BBQubit}\) decomposes as a sum over left qubits plus a sum over right qubits (using \(\operatorname {Fintype.sum\_ sum\_ type}\)). Simplifying the \(\operatorname {Sum.elim}\) applications gives the stated formula.
The monomial group has \(\ell m\) elements: \(|M| = \ell \cdot m\).
By simplification using the cardinality of product types and \(|\mathbb {Z}_n| = n\).
The X check \((\alpha , X)\) acts on L qubit \(\gamma \) with coefficient \(A(\gamma - \alpha )\), i.e., \(\gamma \) is in the support of the shifted polynomial \(\operatorname {shift}_\alpha A\).
This holds by definitional equality (reflexivity).
The X check \((\alpha , X)\) acts on R qubit \(\delta \) with coefficient \(B(\delta - \alpha )\), i.e., \(\delta \) is in the support of the shifted polynomial \(\operatorname {shift}_\alpha B\).
This holds by definitional equality (reflexivity).
The Z check \((\beta , Z)\) acts on L qubit \(\gamma \) with coefficient \(B(\beta - \gamma )\), i.e., \(\gamma \) is in the support of the shifted polynomial \(\operatorname {shift}_\beta B^T\).
By simplification using the definitions of \(\operatorname {bbCheckZ}\), \(\operatorname {pauliZBB}\), \(\operatorname {bbShift}\), and \(\operatorname {bbTranspose}\), together with the identity \(-(\gamma - \beta ) = \beta - \gamma \).
The Z check \((\beta , Z)\) acts on R qubit \(\delta \) with coefficient \(A(\beta - \delta )\), i.e., \(\delta \) is in the support of the shifted polynomial \(\operatorname {shift}_\beta A^T\).
By simplification using the definitions of \(\operatorname {bbCheckZ}\), \(\operatorname {pauliZBB}\), \(\operatorname {bbShift}\), and \(\operatorname {bbTranspose}\), together with the identity \(-(\delta - \beta ) = \beta - \delta \).
For any polynomials \(A, B\) and index \(\alpha \in M\), \(\operatorname {bbCheckX}(A, B, \alpha ) \cdot \operatorname {bbCheckX}(A, B, \alpha ) = I\).
We rewrite the X check as \(\operatorname {pauliXBB}(\operatorname {shift}_\alpha A, \operatorname {shift}_\alpha B)\) and apply the multiplication rule for X-type operators to get \(X(\operatorname {shift}_\alpha A + \operatorname {shift}_\alpha A, \operatorname {shift}_\alpha B + \operatorname {shift}_\alpha B)\). By extensionality on qubit indices: for the \(x\)-vector, on each qubit (left or right), \(f(\gamma ) + f(\gamma ) = 0\) in \(\mathbb {Z}/2\mathbb {Z}\) by \(\operatorname {CharTwo.add\_ self\_ eq\_ zero}\), matching the identity operator. For the \(z\)-vector, both sides are \(0\).
For any polynomials \(A, B\) and index \(\beta \in M\), \(\operatorname {bbCheckZ}(A, B, \beta ) \cdot \operatorname {bbCheckZ}(A, B, \beta ) = I\).
We rewrite the Z check as \(\operatorname {pauliZBB}(\operatorname {shift}_\beta B^T, \operatorname {shift}_\beta A^T)\) and apply the multiplication rule for Z-type operators to get \(Z(\operatorname {shift}_\beta B^T + \operatorname {shift}_\beta B^T, \operatorname {shift}_\beta A^T + \operatorname {shift}_\beta A^T)\). By extensionality on qubit indices: for the \(x\)-vector, both sides are \(0\). For the \(z\)-vector, on each qubit (left or right), \(f(\gamma ) + f(\gamma ) = 0\) in \(\mathbb {Z}/2\mathbb {Z}\) by \(\operatorname {CharTwo.add\_ self\_ eq\_ zero}\), matching the identity operator.