2 The Pauli group
Everything begins with the group \(\mathcal{P}_n\) of \(n\)-qubit Pauli operators with phases. The formalization splits an element into a phase exponent in \(\mathbb {Z}_4\) and a phase-free operator \(\mathrm{Fin}\, n \to \{ I,X,Y,Z\} \). The split is what makes multiplication computable: the operator part multiplies qubitwise, and the phases that fall out of products such as \(XZ = -iY\) accumulate separately.
The four single-qubit Pauli *operators* \(I\), \(X\), \(Y\), \(Z\), taken without a phase. This is the operator part of a Pauli group element; the phase is tracked separately by definition 2.
An element of the single-qubit Pauli group \(\mathcal{P}_1 = \{ \, i^a P : a \in \mathbb {Z}_4,\ P \in \{ I,X,Y,Z\} \, \} \), represented as a pair of a phase exponent \(a \in \mathbb {Z}_4\) and an operator \(P\) (definition 1). Splitting the phase off from the operator is what makes the \(n\)-qubit multiplication rule computable.
An \(n\)-qubit Pauli *operator* is a function \(\mathrm{Fin}\, n \to \{ I,X,Y,Z\} \), i.e. one single-qubit Pauli per qubit. Again this is the phase-free part.
An element of the \(n\)-qubit Pauli group \(\mathcal{P}_n\) is a phase exponent in \(\mathbb {Z}_4\) together with an \(n\)-qubit Pauli operator (definition 3), i.e. a tensor product \(i^a\, P_1 \otimes \cdots \otimes P_n\). Every operator statement in this development is ultimately a statement about elements of \(\mathcal{P}_n\).
The syntactic representation is tied to actual operators on a Hilbert space by a matrix interpretation; without it the development would be a study of a finite group with no quantum content.
The unitary matrix \(i^a\, P_1 \otimes \cdots \otimes P_n\) on \((\mathbb {C}^2)^{\otimes n}\) represented by a Pauli group element. This is the semantic anchor of the formalization: it is what makes the syntactic bookkeeping over \(\mathbb {Z}_4 \times \{ I,X,Y,Z\} ^n\) a statement about operators on a Hilbert space.
Multiplication of two phase-free \(n\)-qubit Pauli operators, returning a full group element: multiplying qubitwise produces a Pauli operator together with an accumulated phase in \(\mathbb {Z}_4\), since e.g. \(XZ = -iY\).
Multiplication on \(\mathcal{P}_n\) is associative. Together with the unit \(I^{\otimes n}\) and the inverse \(g^{-1} = i^{-a}P\) this makes definition 4 a group.
Both sides have the same operator part, since qubitwise multiplication on \(\{ I,X,Y,Z\} \) is associative. For the phase part the accumulated exponents agree in \(\mathbb {Z}_4\); this is checked qubitwise by exhausting the triples of single-qubit operators.
2.1 Weight
Code distance is a statement about how many qubits an operator touches, so support and weight are the measures everything else is phrased in.
The support of \(g \in \mathcal{P}_n\) is the set of qubits on which its operator part is not \(I\).
The weight \(\operatorname {wt}(g)\) of a Pauli group element is the cardinality of its support (definition 8) — the number of qubits it acts on nontrivially. Code distance is a statement about weights.
2.2 Commutation
The single most used fact in the development is that commutation in \(\mathcal{P}_n\) is a parity condition. Two Paulis pick up a sign \(-1\) for each qubit where they disagree nontrivially, so the global sign is \((-1)^k\) and there is no third possibility between commuting and anticommuting.
Two \(n\)-qubit Pauli operators *anticommute at qubit \(i\)* if their \(i\)-th single-qubit operators are distinct and neither is \(I\). This is the local test whose global parity governs commutation.
Two elements of \(\mathcal{P}_n\) commute if and only if the number of qubits at which they anticommute (definition 10) is even.
Each qubit contributes a factor \(\pm 1\) when the two operators are swapped: \(+1\) where they commute locally, \(-1\) where they anticommute. The global sign is the product, hence \((-1)^k\) where \(k\) is the number of anticommuting positions, and the two elements commute exactly when \(k\) is even.
\(p\) and \(q\) *anticommute* when \(pq = -qp\). Anticommutation with a stabilizer generator is the syndrome signal that detects an error.
Any two elements of \(\mathcal{P}_n\) either commute or anticommute — there is no third case.
By theorem 11 the sign picked up on swapping is \((-1)^k\) for \(k\) the number of locally anticommuting qubits, and this is either \(+1\) or \(-1\).