Pauli group, weights, quantum codes, stabilizers, CSS codes, r-filters

Pauli group, weights, quantum codes, stabilizers, CSS codes, r-filters

QAlgorithms.opsWeight

For $n\in\mathbb{N}$ and a tuple $o=(o_1,\dots,o_n)$ of Pauli labels from $\{I,X,Y,Z\}$, the weight is the number of positions $q$ with $o_q \ne I$:

$$\mathrm{wt}(o) = \#\{q : o_q \neq I\}.$$

For $n=0$ the weight is $0$.

QAlgorithms.Stabilizer.PauliString.weight

A Pauli string on $n$ qubits is a pair $(c, o)$, where $c\in\mathbb{Z}/4$ is a phase exponent and $o=(o_1,\dots,o_n)$ is a tuple of labels in $\{I,X,Y,Z\}$. Its weight is $\mathrm{wt}(o)=\#\{q : o_q\ne I\}$. The phase $c$ is ignored.

QAlgorithms.pauliOps

For a tuple $o=(o_1,\dots,o_n)$ of Pauli labels, this is the $2^n\times 2^n$ complex matrix of the Pauli string with phase exponent $0$. Its entries, for $y, z \in\{0,1\}^n$, are

$$\big(\sigma_{o}\big)_{y,z} = \prod_{q} \sigma_{o_q}(y_q, z_q),$$

that is, $\sigma_{o_1}\otimes\cdots\otimes\sigma_{o_n}$. The single-qubit matrices, with row and column index $0$ meaning $|0\rangle$, are

$$\sigma_I = I,\qquad \sigma_X=\begin{pmatrix}0&1\\1&0\end{pmatrix},\qquad \sigma_Y=\begin{pmatrix}0&-i\\ i&0\end{pmatrix},\qquad \sigma_Z=\begin{pmatrix}1&0\\0&-1\end{pmatrix}.$$

For $n=0$ the result is the $1\times1$ matrix $(1)$.

QAlgorithms.pauliSpan

For $n,t\in\mathbb{N}$, this is the complex linear span, inside the space of $2^n\times 2^n$ complex matrices, of all Pauli-string matrices of weight at most $t$:

$$\operatorname{span}_{\mathbb{C}}\Big\{\, i^{c}\,\sigma_{o_1}\otimes\cdots\otimes\sigma_{o_n} \;:\; c\in\mathbb{Z}/4,\ \#\{q: o_q\ne I\}\le t \,\Big\}.$$

Here $i^c$ means $i$ raised to the representative of $c$ in $\{0,1,2,3\}$. The case $t=0$ gives the scalar multiples of the identity.

QAlgorithms.pauliGroup

For $n\in\mathbb{N}$, this is the subgroup of the unitary group $U(2^n)$ generated by every unitary whose matrix equals some Pauli-string matrix

$$i^{c}\,\sigma_{o_1}\otimes\cdots\otimes\sigma_{o_n}, \qquad c\in\mathbb{Z}/4,\ o\in\{I,X,Y,Z\}^n,$$

with $c$ taken as its representative in $\{0,1,2,3\}$. The Pauli matrices are as given under pauliOps.

QAlgorithms.IsStabilizerGroup

For $n\in\mathbb{N}$ and a subgroup $S$ of the unitary group $U(2^n)$, the predicate holds exactly when all three of the following hold:

1. $S$ is contained in the $n$-qubit Pauli group, i.e. the subgroup of $U(2^n)$ generated by all matrices $i^c\,\sigma_{o_1}\otimes\cdots\otimes\sigma_{o_n}$;
2. $S$ is abelian: $ab=ba$ for all $a,b\in S$;
3. no element of $S$ has matrix equal to $-I$.

QAlgorithms.stabilizedSpace

For $n\in\mathbb{N}$ and any subgroup $S$ of the unitary group $U(2^n)$, this is the complex subspace of $\mathbb{C}^{2^n}$ (indexed by $\{0,1\}^n$) given by

$$V_S=\bigcap_{M\in S}\ker(M-I)=\{\psi\in\mathbb{C}^{2^n} : M\psi=\psi \text{ for all } M\in S\}.$$

No hypothesis on $S$ is imposed, for example that it is a stabilizer group. If $S$ is the trivial group, $V_S$ is all of $\mathbb{C}^{2^n}$. If $S$ contains $-I$, then $V_S=\{0\}$.

QAlgorithms.pauliCentralizer

For $n\in\mathbb{N}$ and any subgroup $S$ of $U(2^n)$, this is the subgroup

$$\mathcal{P}_n\cap C_{U(2^n)}(S)=\{U\in\mathcal{P}_n : UM=MU \text{ for all } M\in S\}.$$

Here $\mathcal{P}_n$ is the subgroup of $U(2^n)$ generated by all matrices $i^c\,\sigma_{o_1}\otimes\cdots\otimes\sigma_{o_n}$, with $c\in\mathbb{Z}/4$ and $o\in\{I,X,Y,Z\}^n$.

QAlgorithms.phaseMultiples

For $n\in\mathbb{N}$ and any subgroup $S$ of $U(2^n)$, this is the set of unitaries $U\in U(2^n)$ for which there exist $c\in\mathbb{Z}/4$ and $M\in S$ with

$$U = i^{c}\,M,$$

where $c$ is taken as its representative in $\{0,1,2,3\}$. Equivalently, it is the set of all $\pm M$ and $\pm iM$ for $M\in S$. It is defined only as a set, not as a subgroup.

QAlgorithms.pauliSyndrome

Inputs.

• $n, a \in \mathbb{N}$.
• A family $g = (g_0, \dots, g_{a-1})$ of $2^n \times 2^n$ unitary matrices. Rows and columns are indexed by $n$-bit strings $\{0,1\}^n$.
• A single unitary $E$ of the same size.

Output. The function returns a vector $s \in (\mathbb{Z}/2)^a$ whose $i$-th entry is

$$s_i = \begin{cases} 0 & \text{if } g_i E = E g_i,\\ 1 & \text{otherwise.}\end{cases}$$

Remarks.

• The test is literal matrix commutation, with no allowance for phases. Entry $1$ is assigned whenever $g_i$ and $E$ fail to commute exactly, whether they anticommute or stand in any other relation.
• Nothing is assumed about the $g_i$ or $E$ beyond unitarity. In particular, they need not be Pauli operators.
• When $a = 0$ the result is the empty vector.

QAlgorithms.ActsWithin

Inputs.

• $n \in \mathbb{N}$.
• A finite set $F \subseteq \{0, \dots, n-1\}$ of wires.
• An arbitrary complex $2^n \times 2^n$ matrix $E$, indexed by $n$-bit strings.

Definition. The predicate holds iff there exist:

• some $k \in \mathbb{N}$,
• an injective map $w : \{0,\dots,k-1\} \to \{0,\dots,n-1\}$ whose image is contained in $F$, and
• an arbitrary complex $2^k \times 2^k$ matrix $M$ (not required to be unitary, Hermitian, or anything else),

such that $E$ is the embedding of $M$ on the wires $w$. Entrywise, for $y, z \in \{0,1\}^n$,

$$E_{y,z} = \begin{cases} M_{y\circ w,\; z\circ w} & \text{if } y_a = z_a \text{ for every wire } a \notin \operatorname{im} w,\\ 0 & \text{otherwise.}\end{cases}$$

Here $y \circ w$ is the $k$-bit string $(y_{w(0)}, \dots, y_{w(k-1)})$. In words, $E$ is $M$ acting on the wires $w(0), \dots, w(k-1)$, in that order, tensored with the identity on all remaining wires.

Degenerate case. $k = 0$ is allowed. Then $M$ is a $1 \times 1$ scalar $c$ and $E = c\, I$. So every scalar multiple of the identity satisfies the predicate for every $F$, including $F = \emptyset$.

QAlgorithms.ActsOnAtMost

Inputs.

• $n, t \in \mathbb{N}$.
• An arbitrary complex $2^n \times 2^n$ matrix $E$.

Definition. The predicate holds iff there is a set $F$ of wires with $|F| \le t$ such that $E$ acts within $F$. Expanding the previous definition, this means:

$$E = M \otimes I_{\text{rest}}$$

for some arbitrary complex matrix $M$ placed, via an injective wire map, on wires lying in $F$, with $E$ acting as the identity on every other wire.

Remarks.

• For $t = 0$ the predicate holds exactly for the scalar multiples of the identity.
• For $t \ge n$ it holds for every $E$. One can take $F$ to be all wires and $w$ the identity map, which gives $E = M$.

QAlgorithms.Corrects

Inputs.

• A finite index type $\iota$ with decidable equality.
• A complex linear subspace $C \subseteq \mathbb{C}^\iota$.
• An arbitrary set $S$ of complex $\iota \times \iota$ matrices. These need not be unitary.

Definition. The predicate holds iff there exists a map $R$ from $\iota\times\iota$ matrices to $\iota\times\iota$ matrices satisfying two conditions.

1. $R$ is a channel. There exist $m \in \mathbb{N}$ and matrices $K_0, \dots, K_{m-1}$ with

$$\sum_j K_j^\dagger K_j = I \quad\text{and}\quad R(\rho) = \sum_j K_j \rho K_j^\dagger \ \text{ for every matrix } \rho.$$

2. $R$ corrects every error in $S$. For every $E \in S$ and every $\psi \in C$ with $\|\psi\| = 1$,

$$R\big(|E\psi\rangle\langle E\psi|\big) = \|E\psi\|^2 \, |\psi\rangle\langle\psi| .$$

Here $|\phi\rangle\langle\phi|$ denotes the matrix with entries $\phi_a \overline{\phi_b}$.

Edge cases.

• If $E\psi = 0$, both sides of the condition are $0$.
• If $C = \{0\}$ or $S = \emptyset$, the second condition is vacuous. The predicate then only requires that some channel exist.

QAlgorithms.IsDetectable

Inputs.

• A finite index type $\iota$.
• A complex subspace $C \subseteq \mathbb{C}^\iota$.
• An arbitrary complex $\iota \times \iota$ matrix $E$.

Definition. The predicate holds iff there is a single complex number $c$ such that every unit vector $\psi \in C$ satisfies

$$\langle \psi, E\psi\rangle = c.$$

The inner product is $\langle u, v\rangle = \sum_i \overline{u_i}\, v_i$, conjugate-linear in the first slot.

Remarks.

• Only these diagonal expectation values are constrained. No condition on $\langle\phi, E\psi\rangle$ for distinct $\phi, \psi$ is stated explicitly.
• If $C = \{0\}$, the predicate holds vacuously.

QAlgorithms.IsQCode

Inputs.

• $n, k, d \in \mathbb{N}$.
• A complex subspace $C$ of the $n$-qubit space $\mathbb{C}^{\{0,1\}^n}$.

Definition. $C$ satisfies the predicate iff both of the following hold.

1. Dimension. $\dim_{\mathbb{C}} C = 2^k$.

2. Detection. Every complex $2^n\times 2^n$ matrix $E$ that acts on at most $d - 1$ qubits is detectable on $C$. Concretely:

   • "Acts on at most $d-1$ qubits" means $E = M \otimes I$ with an arbitrary complex matrix $M$ on at most $d-1$ wires.
   • "Detectable on $C$" means there is a constant $c_E$ with $\langle\psi, E\psi\rangle = c_E$ for all unit $\psi \in C$.

Edge cases.

• $d - 1$ is truncated subtraction, so $d = 0$ is treated like $d = 1$. In both cases only scalar multiples of $I$ are required to be detectable, which always holds.
• If $d - 1 \ge n$, every $2^n \times 2^n$ matrix must be detectable.
• Only this one-sided requirement is imposed. Nothing says some matrix acting on $d$ qubits fails to be detectable, so the predicate is monotone downward in $d$.
• $k = 0$ means $C$ is one-dimensional.

QAlgorithms.HasDistance

Inputs.

• $n, d \in \mathbb{N}$.
• A complex subspace $C \subseteq \mathbb{C}^{\{0,1\}^n}$.

Definition. The predicate holds iff both of the following hold.

1. Detection below $d$. Every arbitrary complex $2^n\times 2^n$ matrix $E$ acting on at most $d-1$ qubits (truncated subtraction) is detectable on $C$. That is, $\langle\psi, E\psi\rangle$ takes the same value for all unit $\psi\in C$.

2. Failure at $d$. There exists some complex matrix $E$ acting on at most $d$ qubits (that is, $E = M\otimes I$ with $M$ on at most $d$ wires) that is not detectable on $C$. That is, there are unit vectors $\psi, \psi' \in C$ with

$$\langle\psi, E\psi\rangle \ne \langle\psi', E\psi'\rangle.$$

Edge case $d = 0$.

• The first clause concerns only scalar multiples of $I$.
• The second clause asks for a non-detectable matrix acting on $0$ qubits. Such a matrix is a scalar multiple of $I$, and those are always detectable.
• So the predicate is false for $d = 0$.

QAlgorithms.IsNondegenerate

Inputs.

• $n, t \in \mathbb{N}$.
• A complex subspace $C \subseteq \mathbb{C}^{\{0,1\}^n}$.

Pauli operators. Consider all assignments $o : \{0,\dots,n-1\} \to \{I, X, Y, Z\}$ of weight at most $t$. The weight of $o$ is the number of wires $q$ with $o(q) \ne I$. Each such $o$ gives the operator

$$P_o = \sigma_{o(0)} \otimes \cdots \otimes \sigma_{o(n-1)}, \qquad (P_o)_{y,z} = \prod_q \big(\sigma_{o(q)}\big)_{y_q, z_q},$$

with phase factor $1$. The single-qubit matrices, in basis order $(0, 1)$, are

$$\sigma_I = \begin{pmatrix}1&0\\0&1\end{pmatrix}, \quad \sigma_X = \begin{pmatrix}0&1\\1&0\end{pmatrix}, \quad \sigma_Y = \begin{pmatrix}0&-i\\ i&0\end{pmatrix}, \quad \sigma_Z = \begin{pmatrix}1&0\\0&-1\end{pmatrix}.$$

Definition. The predicate holds iff for every $\psi \in C$ with $\|\psi\| = 1$, the Gram matrix

$$G^{\psi}_{a,b} = \langle P_a \psi,\; P_b \psi\rangle,$$

indexed by pairs of such weight-$\le t$ assignments $a, b$, has nonzero determinant.

Edge cases.

• For $t = 0$ the index set is the single all-$I$ assignment, and $G^\psi = (\|\psi\|^2) = (1)$.
• If $C = \{0\}$, the predicate holds vacuously.

QAlgorithms.binDual

Input. A linear subspace $C \subseteq \mathbb{F}_2^n$, where $\mathbb{F}_2 = \mathbb{Z}/2$.

Definition. This is the subspace

$$C^\perp = \{\, x \in \mathbb{F}_2^n \;:\; c \cdot x = 0 \text{ for all } c \in C \,\}, \qquad c\cdot x = \sum_{i=0}^{n-1} c_i x_i \pmod 2,$$

that is, the dual code with respect to the standard dot product over $\mathbb{F}_2$.

The accompanying proof obligations only verify that this set contains $0$ and is closed under addition and scalar multiplication.

QAlgorithms.bitsOfZMod

Input. A vector $v \in \mathbb{F}_2^n$.

Output. The $n$-bit string whose bit on wire $q$ is $1$ (true) exactly when $v_q = 1$, and $0$ (false) when $v_q = 0$.

This is the identification $\mathbb{F}_2 \ni 0 \mapsto 0$, $1 \mapsto 1$, applied coordinatewise. Wire $q$ of the string corresponds to coordinate $q$ of $v$, and wire $0$ is the most significant bit.

QAlgorithms.cssCosetState

Inputs.

• A linear subspace $C_2 \subseteq \mathbb{F}_2^n$.
• A vector $u \in \mathbb{F}_2^n$.

Output. The $n$-qubit vector

$$|u + C_2^\perp\rangle \;=\; \sum_{w \in C_2^\perp} \big|\, u + w \,\big\rangle .$$

Here:

• $C_2^\perp = \{x : c\cdot x = 0\ \forall c \in C_2\}$ is the dual code over $\mathbb{F}_2$.
• $u + w$ is computed in $\mathbb{F}_2^n$, i.e. bitwise XOR.
• $|b\rangle$ is the computational-basis vector of the bit string $b$.

Remarks.

• The vector is not normalized. Since the terms $u + w$ are distinct, its squared norm is $|C_2^\perp|$.
• No hypothesis relates $u$ to any other code.

QAlgorithms.cssCode

Inputs. Two arbitrary linear subspaces $C_1, C_2 \subseteq \mathbb{F}_2^n$.

Definition. This is the complex subspace of the $n$-qubit space

$$\operatorname{span}_{\mathbb{C}}\Big\{ \textstyle\sum_{w \in C_2^\perp} |u + w\rangle \;:\; u \in C_1 \Big\},$$

the linear span of the unnormalized coset states $|u + C_2^\perp\rangle$ as $u$ ranges over all of $C_1$. Here $C_2^\perp$ is the $\mathbb{F}_2$ dual of $C_2$, and $|b\rangle$ is the computational-basis vector of the bit string $b$.

Remarks.

• No hypothesis such as $C_2^\perp \subseteq C_1$ is imposed.
• Different $u$ may give the same coset state, namely when they differ by an element of $C_2^\perp$.
• $C_1 = \{0\}$ is allowed, giving the span of the single vector $\sum_{w\in C_2^\perp}|w\rangle$.

QAlgorithms.cssZeroState

Setting.

• $n$ is a natural number, the number of qubits.
• $C_2$ is any $\mathbb{F}_2$-linear subspace of $\mathbb{F}_2^n$.
• The state space is $\mathbb{C}^{\{0,1\}^n}$ with the standard inner product. For a bit string $y$, $|y\rangle$ is the standard basis vector at $y$.

Definition. The vector is

$$\mathrm{cssZero}(C_2) \;=\; \sum_{w \in C_2^{\perp}} |\,\bar w\,\rangle ,$$

where:

• $C_2^{\perp} = \{x \in \mathbb{F}_2^n : c\cdot x = \sum_q c_q x_q = 0 \text{ in } \mathbb{F}_2 \text{ for all } c\in C_2\}$ is the binary dual of $C_2$.
• $\bar w \in \{0,1\}^n$ is the bit string with $\bar w_q = 1$ exactly when $w_q = 1 \in \mathbb{F}_2$.

This is the coset-state construction evaluated at the offset $u = 0$.

Edge cases.

• The sum runs over the dual $C_2^\perp$, not over $C_2$ itself.
• There is no normalization factor: the vector has norm $\sqrt{|C_2^\perp|}$, which is not $1$ in general. It equals $1$ only when $C_2^\perp=\{0\}$, i.e. $C_2=\mathbb{F}_2^n$, in which case the vector is $|0\cdots0\rangle$.
• For $n=0$ the vector is the single basis vector of the one-dimensional space.

QAlgorithms.cssPlusState

Setting.

• $n$ is a natural number.
• $C_1$ is any $\mathbb{F}_2$-linear subspace of $\mathbb{F}_2^n$.

Definition. The vector in $\mathbb{C}^{\{0,1\}^n}$ is

$$\mathrm{cssPlus}(C_1) \;=\; \sum_{u \in C_1} |\,\bar u\,\rangle ,$$

where $\bar u\in\{0,1\}^n$ has $\bar u_q = 1$ iff $u_q = 1$ in $\mathbb{F}_2$.

Edge cases.

• The sum runs over $C_1$ itself, not over a dual.
• No Hadamard transform is involved.
• There is no normalization: the norm is $\sqrt{|C_1|}$. This is $1$ only when $C_1=\{0\}$, giving $|0\cdots 0\rangle$.

QAlgorithms.errorSpace

Setting.

• $n$ is a natural number.
• $C$ is any complex linear subspace of $\mathbb{C}^{\{0,1\}^n}$.
• $F \subseteq \{0,\dots,n-1\}$ is a finite set of wire indices (wire $i$ is qubit $i+1$; wire $0$ is the most significant).

Definition. $\mathrm{errorSpace}(C,F)$ is the complex linear span of all vectors $E c$ such that:

• $c \in C$, and
• $E$ is a $2^n\times 2^n$ complex matrix that "acts within $F$".

"Acts within $F$". This means there exist:

• some $k\ge 0$,
• an injective map $w:\{0,\dots,k-1\}\to\{0,\dots,n-1\}$ with image contained in $F$, and
• an arbitrary complex $2^k\times 2^k$ matrix $M$,

such that $E$ is $M$ placed on wires $w$. Explicitly:

$$E_{y,z} = \begin{cases} M_{\,y\circ w,\; z\circ w} & \text{if } y_a = z_a \text{ for every wire } a \notin w(\{0,\dots,k-1\}),\\ 0 & \text{otherwise.}\end{cases}$$

Here $y\circ w$ denotes the $k$-bit string $(y_{w(0)},\dots,y_{w(k-1)})$.

Edge cases.

• $M$, and hence $E$, need not be unitary or invertible. Any matrix, including $0$, is allowed.
• Taking $k=0$ gives $E = M_{\emptyset,\emptyset}\cdot I$, a scalar multiple of the identity, so $C \subseteq \mathrm{errorSpace}(C,F)$ always.
• For $F=\emptyset$, only $k=0$ is possible, and the space equals $C$.
• If $C=\{0\}$, the space is $\{0\}$.

QAlgorithms.errorSpaceWithRef

Setting.

• $n$ is a natural number.
• $R$ is any finite type, serving as a reference system.
• $C$ is a complex subspace of $\mathbb{C}^{\{0,1\}^n}$.
• $F$ is a finite set of wires.

Definition. The subspace of $\mathbb{C}^{\{0,1\}^n\times R}$ (system register first, reference second) is

$$\operatorname{span}_{\mathbb{C}}\{\, v\otimes r \;:\; v \in \mathrm{errorSpace}(C,F),\ r\in\mathbb{C}^R \,\},$$

where:

• $(v\otimes r)(z,\rho) = v_z\, r_\rho$, and
• $\mathrm{errorSpace}(C,F)$ is the span of $\{Ec : c\in C,\ E \text{ an arbitrary (not necessarily unitary) matrix supported on wires in } F\}$, exactly as in the previous entry.

In other words, it is $\mathrm{errorSpace}(C,F)\otimes \mathbb{C}^R$.

Edge case. If $R$ is empty, the ambient space and this subspace are both $\{0\}$.

QAlgorithms.filterSpace

Setting.

• $n$ is a natural number.
• $C$ is a complex subspace of $\mathbb{C}^{\{0,1\}^n}$.
• $r$ is a natural number.

Definition. $\mathrm{filterSpace}(C,r)$ is the complex span of all vectors $P c$ with $c\in C$, where $P$ is the matrix of a Pauli string of weight at most $r$.

Pauli strings. A Pauli string consists of:

• a phase $c\in\mathbb{Z}/4$, and
• single-qubit operators $\sigma_0,\dots,\sigma_{n-1}\in\{I,X,Y,Z\}$.

Its matrix has entries

$$P_{y,z} = i^{c}\prod_{q} (\sigma_q)_{y_q,z_q},$$

i.e. $P = i^c\,\sigma_0\otimes\cdots\otimes\sigma_{n-1}$, using the usual matrices:

$$X=\begin{pmatrix}0&1\\1&0\end{pmatrix},\qquad Y=\begin{pmatrix}0&-i\\ i&0\end{pmatrix},\qquad Z=\operatorname{diag}(1,-1),$$

with index $0$ first. The weight of the string is the number of $q$ with $\sigma_q\neq I$.

Edge cases.

• The phase does not affect the span.
• The weight-$0$ string is $I$, so $C\subseteq\mathrm{filterSpace}(C,r)$ for every $r$, including $r=0$, where the space equals $C$.
• For $r\ge n$, all Pauli strings are allowed.

QAlgorithms.filterProj

Setting.

• $n$ is a natural number.
• $C$ is a complex subspace of $\mathbb{C}^{\{0,1\}^n}$.
• $r$ is a natural number.

Definition. $\mathrm{filterProj}(C,r)$ is the $2^n\times 2^n$ complex matrix, in the standard basis, of the orthogonal projection (with respect to the standard Hermitian inner product) onto $\mathrm{filterSpace}(C,r)$.

$\mathrm{filterSpace}(C,r)$ is the span of $\{P c : c\in C,\ P$ the matrix $i^{c'}\sigma_0\otimes\cdots\otimes\sigma_{n-1}$ of a Pauli string with at most $r$ non-identity factors$\}$, as in the previous entry.

Edge cases.

• If $C=\{0\}$, the matrix is $0$.
• Since $C\subseteq \mathrm{filterSpace}(C,r)$, the projection fixes every vector of $C$.

import Definitions.Def_QAlgorithms_Defs_Channel
/-!
# Pauli group, weights, quantum codes, stabilizers, CSS codes, r-filters
(shared definition layer)

D. Gottesman, *An introduction to quantum error correction and fault-tolerant quantum
computation* (arXiv:0904.2557), cited "Gottesman intro p.N" (PDF pages), §§2–4.

Conventions. The `n`-qubit Pauli operators are the frozen `Stabilizer.PauliString n` (overall
phase `i^c`, factors `I, X, Y, Z` with `Y = [[0, −i], [i, 0]] = iXZ`, intro Table 1; factor `q`
acts on wire `q`). The Pauli group `P_n` is a subgroup of Mathlib's group
`Matrix.unitaryGroup (Qubits n) ℂ`. A quantum code is a `Submodule` of
`EuclideanSpace ℂ (Qubits n)` (intro p.3: "the coding space"); codewords in conditions on
states are normalized (`‖ψ‖ = 1`). Binary vectors are `Fin n → ZMod 2`.
-/

namespace QAlgorithms

open scoped ComplexConjugate Matrix

open Stabilizer

/-- Gottesman intro p.3 (Table 1): the four single-qubit Pauli labels `I, X, Y, Z` form a finite
type (needed to index the Pauli operators of weight at most `t` by `Fin n → Pauli`). -/
instance Stabilizer.instFintypePauli : Fintype Stabilizer.Pauli where
  elems := {.I, .X, .Y, .Z}
  complete := fun p => by cases p <;> simp

/-- Gottesman intro p.4 (§2.1): the weight of the tensor product with factors `o`, "the number of
tensor factors which are not `I`". -/
def opsWeight {n : ℕ} (o : Fin n → Pauli) : ℕ :=
  (Finset.univ.filter fun q => o q ≠ Pauli.I).card

/-- Gottesman intro p.4 (§2.1): the weight `wt(Q)` of a Pauli operator `Q ∈ P_n` (independent of
its overall phase). -/
def Stabilizer.PauliString.weight {n : ℕ} (P : PauliString n) : ℕ :=
  opsWeight P.ops

/-- Gottesman intro p.3 (Table 1): the phase-`+1` Pauli matrix `P_1 ⊗ ⋯ ⊗ P_n` with factors `o`
(factor `q` on wire `q`). -/
noncomputable def pauliOps {n : ℕ} (o : Fin n → Pauli) : Matrix (Qubits n) (Qubits n) ℂ :=
  (⟨0, o⟩ : PauliString n).toMatrix

/-- Gottesman intro pp.4–5 (§2.1) and p.19 (Def. 1): the linear span of the Pauli errors of
weight at most `t` ("the n-qubit Pauli group spans the space of `2^n × 2^n` matrices"; the span is
the space of all operators acting on at most `t` qubits). -/
noncomputable def pauliSpan (n t : ℕ) : Submodule ℂ (Matrix (Qubits n) (Qubits n) ℂ) :=
  Submodule.span ℂ {M | ∃ P : PauliString n, P.weight ≤ t ∧ M = P.toMatrix}

/-- Gottesman intro p.3 (§2): the `n`-qubit Pauli group `P_n`, generated by the tensor products of
`I, X, Y, Z` with overall phases `±1, ±i`, as a subgroup of the unitary group. (The set of the
`4^{n+1}` matrices `i^c P_1 ⊗ ⋯ ⊗ P_n` is already a group; taking the closure keeps the definition
free of proof obligations.) -/
noncomputable def pauliGroup (n : ℕ) : Subgroup (Matrix.unitaryGroup (Qubits n) ℂ) :=
  Subgroup.closure {U | ∃ P : PauliString n, (U : Matrix (Qubits n) (Qubits n) ℂ) = P.toMatrix}

/-- Gottesman intro p.9 (§2.3) and p.12: `S` is a stabilizer: an Abelian subgroup of `P_n` not
containing `−1` ("S must be Abelian and cannot contain −1, or the code is trivial"). -/
def IsStabilizerGroup {n : ℕ} (S : Subgroup (Matrix.unitaryGroup (Qubits n) ℂ)) : Prop :=
  S ≤ pauliGroup n ∧ (∀ a ∈ S, ∀ b ∈ S, a * b = b * a) ∧
    ∀ M ∈ S, (M : Matrix (Qubits n) (Qubits n) ℂ) ≠ -1

/-- Gottesman intro p.9 (§2.3): the code `T(S)`, "the set of states `|ψ⟩` for which `M|ψ⟩ = |ψ⟩`
for all `M ∈ S`". -/
noncomputable def stabilizedSpace {n : ℕ} (S : Subgroup (Matrix.unitaryGroup (Qubits n) ℂ)) :
    Submodule ℂ (EuclideanSpace ℂ (Qubits n)) :=
  ⨅ M ∈ S, LinearMap.ker
    (Matrix.toEuclideanLin ((M : Matrix (Qubits n) (Qubits n) ℂ) - 1))

/-- Gottesman intro p.10 (§2.3): `N(S)`, the normalizer of `S` in the Pauli group, "which is in
this case equal to the centralizer, composed of Pauli operators which commute with `S`". -/
noncomputable def pauliCentralizer {n : ℕ} (S : Subgroup (Matrix.unitaryGroup (Qubits n) ℂ)) :
    Subgroup (Matrix.unitaryGroup (Qubits n) ℂ) :=
  pauliGroup n ⊓ Subgroup.centralizer (S : Set (Matrix.unitaryGroup (Qubits n) ℂ))

/-- Gottesman intro p.3 ("the phase of the operators used is generally not very important") and
p.10 (Thm 5): the elements of `S` up to an overall phase `±1, ±i`. Thm 5's `N(S) \ S` is read as
`N(S)` minus this set: taken literally, `−I ∈ N(S) \ S` has weight `0` and would force `d = 0`. -/
def phaseMultiples {n : ℕ} (S : Subgroup (Matrix.unitaryGroup (Qubits n) ℂ)) :
    Set (Matrix.unitaryGroup (Qubits n) ℂ) :=
  {U | ∃ c : ZMod 4, ∃ M ∈ S,
    (U : Matrix (Qubits n) (Qubits n) ℂ) = Complex.I ^ c.val • (M : Matrix (Qubits n) (Qubits n) ℂ)}

/-- Gottesman intro p.10 (§2.3) and p.12 (proof of Lemma 1): the error syndrome of `E` with
respect to the generators `g_0, …, g_{a−1}`: bit `i` is `0` if the `i`th generator commutes with
`E` and `1` otherwise (for Pauli operators: if it anticommutes). -/
noncomputable def pauliSyndrome {n a : ℕ} (g : Fin a → Matrix.unitaryGroup (Qubits n) ℂ)
    (E : Matrix.unitaryGroup (Qubits n) ℂ) : Fin a → ZMod 2 :=
  open Classical in
  fun i => if g i * E = E * g i then 0 else 1

/-- Gottesman intro p.5 (§2.1: "all t-qubit errors really does apply to all t-qubit errors, not
just unitary ones") and p.28 (Claim 1: errors only on the qubits of a set): the operator `E` acts
only on the qubits in `F`: it is `M ⊗ I` for some operator `M` (not necessarily unitary) on qubits
inside `F` (frozen `embedOp`: the identity on the other qubits). -/
def ActsWithin {n : ℕ} (F : Finset (Fin n)) (E : Matrix (Qubits n) (Qubits n) ℂ) : Prop :=
  ∃ (k : ℕ) (w : Fin k ↪ Fin n) (M : Matrix (Qubits k) (Qubits k) ℂ),
    Set.range w ⊆ (F : Set (Fin n)) ∧ E = embedOp M w

/-- Gottesman intro p.5 (Thm 2) and p.7 (§2.2): `E` is a `t`-qubit error, an operator acting on
at most `t` qubits. -/
def ActsOnAtMost {n : ℕ} (t : ℕ) (E : Matrix (Qubits n) (Qubits n) ℂ) : Prop :=
  ∃ F : Finset (Fin n), F.card ≤ t ∧ ActsWithin F E

/-- Gottesman intro p.4 (§2.1: "determine which error occurred and invert it") and p.6 (§2.2):
the code `C` corrects the errors in `S`: one recovery operation `R` (a quantum operation) maps
`E|ψ⟩⟨ψ|E†` back to `|ψ⟩⟨ψ|` for every error `E ∈ S` and every normalized codeword `ψ`, up to the
weight `‖Eψ‖²` forced by trace preservation (an `E` annihilating `ψ` never arises). -/
def Corrects {ι : Type*} [Fintype ι] [DecidableEq ι] (C : Submodule ℂ (EuclideanSpace ℂ ι))
    (S : Set (Matrix ι ι ℂ)) : Prop :=
  ∃ R : Superop ι ι, IsChannel R ∧ ∀ E ∈ S, ∀ ψ ∈ C, ‖ψ‖ = 1 →
    R (pureDensity (act E ψ)) = ((‖act E ψ‖ ^ 2 : ℝ) : ℂ) • pureDensity ψ

/-- Gottesman intro p.7 (§2.2, eq. (34)): the operator `E` satisfies `⟨ψ|E|ψ⟩ = C′(E)` on the code:
the value is the same for all normalized codewords (`E` is detectable). -/
def IsDetectable {ι : Type*} [Fintype ι] (C : Submodule ℂ (EuclideanSpace ℂ ι))
    (E : Matrix ι ι ℂ) : Prop :=
  ∃ c : ℂ, ∀ ψ ∈ C, ‖ψ‖ = 1 → inner ℂ ψ (act E ψ) = c

/-- Gottesman intro p.7 (§2.2): `C` is an `[[n, k, d]]` code: a subspace of `n` qubits of dimension
`2^k` (it encodes `k` qubits) of distance at least `d`, the distance being "the minimum weight of an
operator `E` that violates equation (34)": every operator on at most `d − 1` qubits is detectable.
(At `d = 0` the condition concerns `0`-qubit operators, i.e. scalars, which are always
detectable.) -/
def IsQCode (n k d : ℕ) (C : Submodule ℂ (EuclideanSpace ℂ (Qubits n))) : Prop :=
  Module.finrank ℂ C = 2 ^ k ∧ ∀ E : Matrix (Qubits n) (Qubits n) ℂ, ActsOnAtMost (d - 1) E →
    IsDetectable C E

/-- Gottesman intro p.7 (§2.2) and p.10 (Thm 5): the code `C` has distance exactly `d`: every
operator on at most `d − 1` qubits is detectable, and some operator on `d` qubits is not. -/
def HasDistance {n : ℕ} (C : Submodule ℂ (EuclideanSpace ℂ (Qubits n))) (d : ℕ) : Prop :=
  (∀ E : Matrix (Qubits n) (Qubits n) ℂ, ActsOnAtMost (d - 1) E → IsDetectable C E) ∧
    ∃ E : Matrix (Qubits n) (Qubits n) ℂ, ActsOnAtMost d E ∧ ¬ IsDetectable C E

/-- Gottesman intro p.7 (§2.2, eq. (30)): the code is nondegenerate for `t` errors: "the matrix
`C_ab` in (30) has maximum rank", where `C_ab = ⟨ψ|E_a†E_b|ψ⟩` with `E_a, E_b` ranging over the basis
of the `t`-qubit errors formed by the tensor products of `I, X, Y, Z` with at most `t` non-identity
factors (phases dropped); full rank is `det ≠ 0`, required at every normalized codeword. -/
def IsNondegenerate {n : ℕ} (C : Submodule ℂ (EuclideanSpace ℂ (Qubits n))) (t : ℕ) : Prop :=
  ∀ ψ ∈ C, ‖ψ‖ = 1 →
    (Matrix.of fun a b : {o : Fin n → Pauli // opsWeight o ≤ t} =>
      inner ℂ (act (pauliOps a.1) ψ) (act (pauliOps b.1) ψ)).det ≠ 0

/-- Gottesman intro p.11 (§2.4, CSS codes): the dual `C⊥` of a binary linear code `C`, "those words
which are orthogonal to the codewords of `C`" under the dot product over `F₂`. -/
def binDual {n : ℕ} (C : Submodule (ZMod 2) (Fin n → ZMod 2)) :
    Submodule (ZMod 2) (Fin n → ZMod 2) where
  carrier := {x | ∀ c ∈ C, c ⬝ᵥ x = 0}
  add_mem' := by
    intro x y hx hy c hc
    rw [dotProduct_add, hx c hc, hy c hc, add_zero]
  zero_mem' := by
    intro c _
    exact dotProduct_zero c
  smul_mem' := by
    intro a x hx c hc
    rw [dotProduct_smul, hx c hc, smul_zero]

/-- Gottesman intro p.11 (§2.4): the computational-basis label `|v⟩` of a binary vector
`v ∈ F₂ⁿ` (bit `q` is `1` iff `v_q = 1`). -/
def bitsOfZMod {n : ℕ} (v : Fin n → ZMod 2) : Qubits n :=
  fun q => decide (v q = 1)

/-- Gottesman intro p.11 (§2.4, eq. (51)): the CSS codeword `Σ_{w ∈ C2⊥} |u + w⟩`, unnormalized
("I omit normalization, which is generally unimportant", p.2). -/
noncomputable def cssCosetState {n : ℕ} (C2 : Submodule (ZMod 2) (Fin n → ZMod 2))
    (u : Fin n → ZMod 2) : EuclideanSpace ℂ (Qubits n) :=
  open Classical in
  ∑ w : binDual C2, ket (bitsOfZMod (u + (w : Fin n → ZMod 2)))

/-- Gottesman intro p.11 (§2.4): the CSS code of the binary codes `C1`, `C2`: the span of the
codewords (51) for `u ∈ C1`. (The construction assumes `C2⊥ ⊆ C1`, a hypothesis of the
statements.) -/
noncomputable def cssCode {n : ℕ} (C1 C2 : Submodule (ZMod 2) (Fin n → ZMod 2)) :
    Submodule ℂ (EuclideanSpace ℂ (Qubits n)) :=
  Submodule.span ℂ (Set.range fun u : C1 => cssCosetState C2 (u : Fin n → ZMod 2))

/-- Gottesman intro p.27 (§4.4, Fig. 3, the phase ancilla of Steane EC): the encoded `|0⟩` of the
CSS code, `Σ_{w ∈ C2⊥} |w⟩` (unnormalized). -/
noncomputable def cssZeroState {n : ℕ} (C2 : Submodule (ZMod 2) (Fin n → ZMod 2)) :
    EuclideanSpace ℂ (Qubits n) :=
  cssCosetState C2 0

/-- Gottesman intro p.27 (§4.4, Fig. 3, the bit-flip ancilla of Steane EC): the encoded
`|0⟩ + |1⟩` of the CSS code, the sum `Σ_{u ∈ C1} |u⟩` of all its coset states (unnormalized). -/
noncomputable def cssPlusState {n : ℕ} (C1 : Submodule (ZMod 2) (Fin n → ZMod 2)) :
    EuclideanSpace ℂ (Qubits n) :=
  open Classical in
  ∑ u : C1, ket (bitsOfZMod (u : Fin n → ZMod 2))

/-- Gottesman intro p.28 (§4.4, Claim 1: "errors only on qubits from `F`"): the span of the states
`E|c⟩` with `c` a codeword and `E` any operator acting only on the qubits of `F`. -/
noncomputable def errorSpace {n : ℕ} (C : Submodule ℂ (EuclideanSpace ℂ (Qubits n)))
    (F : Finset (Fin n)) : Submodule ℂ (EuclideanSpace ℂ (Qubits n)) :=
  Submodule.span ℂ {v | ∃ (E : Matrix (Qubits n) (Qubits n) ℂ) (c : EuclideanSpace ℂ (Qubits n)),
    ActsWithin F E ∧ c ∈ C ∧ v = act E c}

/-- Gottesman intro p.28 (§4.4): `errorSpace C F` tensored with a reference register `R` (the data
block may be entangled with the rest of the computer); the block is the first factor. -/
noncomputable def errorSpaceWithRef {n : ℕ} (R : Type*) [Fintype R]
    (C : Submodule ℂ (EuclideanSpace ℂ (Qubits n))) (F : Finset (Fin n)) :
    Submodule ℂ (EuclideanSpace ℂ (Qubits n × R)) :=
  Submodule.span ℂ {x | ∃ v ∈ errorSpace C F, ∃ r : EuclideanSpace ℂ R, x = tensorVec v r}

/-- Gottesman intro p.19 (Def. 1): the subspace "spanned by all states of the form `Q|ψ⟩`, where
`|ψ⟩` is an arbitrary codeword and `Q` is a Pauli error of weight at most `r`". -/
noncomputable def filterSpace {n : ℕ} (C : Submodule ℂ (EuclideanSpace ℂ (Qubits n))) (r : ℕ) :
    Submodule ℂ (EuclideanSpace ℂ (Qubits n)) :=
  Submodule.span ℂ {v | ∃ (P : PauliString n) (c : EuclideanSpace ℂ (Qubits n)),
    P.weight ≤ r ∧ c ∈ C ∧ v = act P.toMatrix c}

/-- Gottesman intro p.19 (Def. 1): the `r`-filter, the (orthogonal) projector onto
`filterSpace C r`, as a matrix; it acts on a block state `ρ` as `conjSuperop (filterProj C r)`. -/
noncomputable def filterProj {n : ℕ} (C : Submodule ℂ (EuclideanSpace ℂ (Qubits n))) (r : ℕ) :
    Matrix (Qubits n) (Qubits n) ℂ :=
  Matrix.toEuclideanLin.symm
    ((filterSpace C r).starProjection : EuclideanSpace ℂ (Qubits n) →ₗ[ℂ] EuclideanSpace ℂ (Qubits n))

/-! ### Sanity tests -/

example : Fintype.card Stabilizer.Pauli = 4 := rfl

example : opsWeight (![Pauli.X, Pauli.Y, Pauli.I] : Fin 3 → Pauli) = 2 := by decide

example {n : ℕ} (c : ZMod 4) : (⟨c, fun _ => Pauli.I⟩ : PauliString n).weight = 0 := by
  simp [Stabilizer.PauliString.weight, opsWeight]

example : bitsOfZMod (![1, 0] : Fin 2 → ZMod 2) = ![true, false] := by decide

example {n : ℕ} (x : Fin n → ZMod 2) : x ∈ binDual (⊥ : Submodule (ZMod 2) (Fin n → ZMod 2)) := by
  intro c hc
  rw [(Submodule.mem_bot _).1 hc, zero_dotProduct]

example {n : ℕ} (C : Submodule ℂ (EuclideanSpace ℂ (Qubits n))) (c : ℂ) :
    IsDetectable C (c • (1 : Matrix (Qubits n) (Qubits n) ℂ)) := by
  refine ⟨c, fun ψ _ hψ => ?_⟩
  have h : act (c • (1 : Matrix (Qubits n) (Qubits n) ℂ)) ψ = c • ψ := by
    ext z; simp [act, Matrix.smul_mulVec]
  rw [h, inner_smul_right, inner_self_eq_norm_sq_to_K, hψ]
  simp

example {n : ℕ} (E : Matrix (Qubits n) (Qubits n) ℂ) (F : Finset (Fin n)) (hE : ActsWithin F E) :
    ActsOnAtMost F.card E :=
  ⟨F, le_rfl, hE⟩

theorem embedOp_one_mem_actsWithin {n : ℕ} (F : Finset (Fin n)) :
    ActsWithin F (1 : Matrix (Qubits n) (Qubits n) ℂ) :=
  ⟨0, ⟨Fin.elim0, fun a => Fin.elim0 a⟩, 1, by
    rintro _ ⟨a, _⟩; exact Fin.elim0 a, (embedOp_one _).symm⟩

end QAlgorithms