QuantumInfo.Finite.Qubit.Basic

The type `Qubit` is defined as the set of indices $\{0, 1\}$, represented by the finite type $\text{Fin } 2$. In the context of quantum information, this serves as the index set for the computational basis states of a two-level south-system (a qubit).

`matrix_expand` is a tactic designed to prove equalities between small matrices. It operates by expanding matrix products into their individual entries and then simplifying the resulting expressions using standard real-number arithmetic. The tactic optionally accepts a list of simplification lemmas (via `[...]`) and a pattern for case-splitting/recursion (via `with ...`).

The Pauli $Z$ gate is a unitary operator $\sigma_z$ acting on the Hilbert space of a single qubit, represented in the computational basis by the $2 \times 2$ matrix: $$\sigma_z = \begin{pmatrix} 1 & 0 \\ 0 & -1 \end{pmatrix}$$ This operator maps the basis state $\ket{0}$ to $\ket{0}$ and the basis state $\ket{1}$ to $-\ket{1}$.

The Pauli $X$ gate is a unitary operator $\sigma_x$ acting on the Hilbert space of a single qubit, represented in the computational basis by the $2 \times 2$ matrix: $$\sigma_x = \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}$$ This operator performs a bit-flip, mapping the basis state $\ket{0}$ to $\ket{1}$ and the basis state $\ket{1}$ to $\ket{0}$.

The Pauli $Y$ gate is a unitary operator acting on the Hilbert space of a qubit, represented in the computational basis by the $2 \times 2$ matrix: $$\sigma_y = \begin{pmatrix} 0 & -i \\ i & 0 \end{pmatrix}$$ where $i$ is the imaginary unit.

The Hadamard gate $H$ is a unitary operator acting on the Hilbert space of a qubit. In the computational basis $\{|0\rangle, |1\rangle\}$ (indexed by `Qubit`), it is represented by the matrix: $$H = \frac{1}{\sqrt{2}} \begin{pmatrix} 1 & 1 \\ 1 & -1 \end{pmatrix}$$

The $S$ gate (also known as the Phase gate) is a unitary operator acting on the Hilbert space of a single qubit. In the computational basis $\{|0\rangle, |1\rangle\}$, it is represented by the $2 \times 2$ matrix: $$S = \begin{pmatrix} 1 & 0 \\ 0 & i \end{pmatrix}$$ where $i$ is the imaginary unit. This operator corresponds to a rotation about the $z$-axis of the Bloch sphere by an angle of $\pi/2$, i.e., $R_z(\pi/2)$ (up to a global phase).

The $T$ gate is a unitary operator on a single qubit, defined by the matrix $$T = \begin{pmatrix} 1 & 0 \\ 0 & \frac{1+i}{\sqrt{2}} \end{pmatrix}$$ This corresponds to a rotation about the $z$-axis of the Bloch sphere by an angle of $\pi/4$, i.e., $R_z(\pi/4)$ (up to a global phase).

The square of the Pauli $Z$ operator is equal to the identity operator, i.e., $Z^2 = I$.

For the single-qubit Pauli-$X$ gate, the square of the operator is equal to the identity operator, i.e., $X^2 = I$.

The square of the Pauli $Y$ gate $\sigma_y$ is equal to the identity operator $\mathbb{1}$ on the qubit Hilbert space, meaning $\sigma_y \sigma_y = \mathbb{1}$.

The square of the Hadamard gate $H$ is equal to the identity operator $I$ on the qubit Hilbert space, i.e., $H^2 = I$.

The square of the $S$ gate (phase gate) is equal to the Pauli $Z$ gate, expressed as $S^2 = Z$, where $S$ and $Z$ are unitary operators acting on the single-qubit Hilbert space.

In the context of qubit operations, the square of the $T$ gate is equal to the $S$ gate ($T^2 = S$). Here, $T$ and $S$ denote the standard single-qubit phase gates.

The Pauli $X$ and $Y$ gates anticommute, satisfying the relation $XY = -YX$.

Let $Y$ and $Z$ be the Pauli-$Y$ and Pauli-$Z$ gates acting on the Hilbert space of a qubit. These operators satisfy the anticommutation relation $ZY = -YZ$.

Let $Z$ and $X$ be the Pauli-$Z$ and Pauli-$X$ gates acting on the Hilbert space of a qubit. These operators satisfy the anticommutation relation $ZX = -XZ$, or equivalently, the anticommutator $\{Z, X\} = ZX + XZ$ is zero.

Let $H$, $X$, and $Z$ be the Hadamard gate, the Pauli-$X$ gate, and the Pauli-$Z$ gate acting on a qubit, respectively. Then the following operator identity holds: $$H X = Z H$$

Let $H$, $Z$, and $X$ be the Hadamard gate, the Pauli-$Z$ gate, and the Pauli-$X$ gate acting on a qubit, respectively. Then the following operator identity holds: $$H Z = X H$$

Let $S$ be the phase gate and $Z$ be the Pauli-$Z$ gate acting on a qubit. Then these operators commute, satisfying the identity: $$Z S = S Z$$

The single-qubit phase gate $T$ and the Pauli $Z$ gate commute, such that $Z T = T Z$.

For the single-qubit gates $S$ and $T$, the commutation relation $S T = T S$ holds.

Given a Hilbert space $\mathcal{H}_k$ and a unitary operator $U \in \text{U}(\mathcal{H}_k)$, the controllized version of $U$ is a unitary operator acting on the space $\mathbb{C}^2 \otimes \mathcal{H}_k$ (represented as $\text{Qubit} \times k$). The operator acts as the identity on the subspace corresponding to the qubit state $|0\rangle$ and applies $U$ on the subspace corresponding to the qubit state $|1\rangle$. Formally, its matrix elements are defined as: \[ (C(U))_{(q_1, t_1), (q_2, t_2)} = \begin{cases} \delta_{t_1, t_2} & \text{if } q_1 = q_2 = 0 \\ U_{t_1, t_2} & \text{if } q_1 = q_2 = 1 \\ 0 & \text{otherwise} \end{cases} \] where $q_1, q_2 \in \{0, 1\}$ are the control qubit indices and $t_1, t_2$ are indices in the target space $k$.

For a given quantum gate or unitary operator $g$ acting on a $k$-qubit system, $C[g]$ denotes the controlled version of that gate, which is a unitary operator acting on a system of $1 + k$ qubits (the control qubit and the original $k$ qubits).

The Controlled-NOT gate, denoted as $\text{CNOT}$, is a unitary operator acting on a two-qubit system represented by the space $\mathbb{C}^2 \otimes \mathbb{C}^2$ (coordinated here as $\text{Fin } 2 \times \text{Fin } 2$). It is defined by applying the Pauli-$X$ gate (the quantum NOT gate) to the target qubit if and only if the control qubit is in the state $|1\rangle$. Formally, it is the result of the `controllize` operation applied to the single-qubit gate $X$.

The matrix representation of the CNOT (Controlled-NOT) gate, acting on the product space of two qubits and reindexed using the standard equivalence $\text{Fin } 2 \times \text{Fin } 2 \simeq \text{Fin } 4$, is given by the $4 \times 4$ permutation matrix: $$\begin{pmatrix} 1 & 0 & 0 & 0 \\ 0 & 1 & 0 & 0 \\ 0 & 0 & 0 & 1 \\ 0 & 0 & 1 & 0 \end{pmatrix}$$ where the entries are complex numbers $\mathbb{C}$.

Let $g$ be a unitary operator $\mathbf{U}[k]$ acting on a $k$-dimensional Hilbert space. Let $C[g]$ denote the controlled version of $g$, which is a unitary operator acting on the product space of a qubit and the $k$-dimensional space, $\mathbb{C}^2 \otimes k$. For any indices $j_1, j_2$ in the $k$-dimensional space, the matrix element of the controlled gate $C[g]$ corresponding to the control qubit being in state $|0\rangle$ is given by: \[ (C[g])_{(0, j_1), (0, j_2)} = I_{j_1, j_2} \] where $I$ is the identity operator in $\mathbf{U}[k]$. This reflects that when the control qubit is $|0\rangle$, the operation applied to the target system is the identity.

Let $g$ be a unitary operator acting on a system $k$ (denoted as $g \in \mathbf{U}[k]$), and let $C[g]$ denote the controlled version of $g$ where a qubit acts as the control. For any indices $j_1, j_2$ in the state space of $k$, the matrix element of the controlled operator $C[g]$ corresponding to the transition from the control qubit being in state $|1\rangle$ and system $k$ being in state $|j_2\rangle$ to the control qubit being in state $|0\rangle$ and system $k$ being in state $|j_1\rangle$ is zero. In other words, $(C[g])_{(0, j_1), (1, j_2)} = 0$.

Let $g$ be a unitary operator acting on a $k$-dimensional quantum system, denoted by $\mathbf{U}[k]$. Let $C[g]$ denote the controlled version of $g$, acting on the composite system of a control qubit and the $k$-dimensional target system, where the qubit states are indexed by $\{0, 1\}$. For any indices $j_1, j_2$ of the target system, the matrix element of the controlled operator $C[g]$ corresponding to the control qubit being in state $|1\rangle$ and transitioning to $|0\rangle$ is zero. That is, $\langle 1, j_1 | C[g] | 0, j_2 \rangle = 0$.

Let $g$ be a unitary operator acting on a $k$-qubit system, and let $C[g]$ denote its controlled version acting on a $(1+k)$-qubit system where the first qubit is the control. For any basis states $|j_1\rangle$ and $|j_2\rangle$ of the $k$-qubit target system, if the control qubit is in state $|1\rangle$, the matrix elements of the controlled gate satisfy: $$(C[g])_{(1, j_1), (1, j_2)} = g_{j_1, j_2}$$ where $1$ denotes the state of the control qubit being "on".

Let $g_1, g_2 \in \mathbf{U}[k]$ be two unitary operators acting on a $k$-qubit system. Let $C[g]$ denote the controllization of a unitary operator $g$, which is a unitary operator on the combined system of a control qubit and the $k$-qubit target. Then the product of the controllized operators is the controllization of the product of the operators, i.e., $C[g_1] \cdot C[g_2] = C[g_1 \cdot g_2]$.

For any unitary operator $1$ acting on a $k$-qubit system, its controlled version $C[1]$ acting on the combined system of a control qubit and the $k$-qubit target is equal to the identity operator $1$ on the combined system. Use $C[g]$ to denote the controllization of a gate $g$, and $\mathbf{U}[k]$ to denote the space of unitary operators on $k$ qubits.

Let $g$ be a unitary operator acting on a $k$-qubit system, and let $C[g]$ denote the controllized version of $g$, acting on the composite space of a control qubit and the $k$-qubit target. The product of the controllized operator $C[g]$ and the controllized version of its inverse $C[g^{-1}]$ is the identity operator $1$ on the combined system.

Let $X$ be the Pauli-X gate acting on a qubit, and let $g$ be a unitary operator on a $k$-qubit system. Let $C[g]$ denote the controlled version of $g$, where the first qubit acts as the control and the $k$-qubit system is the target. Then the following identity holds: $$(X \otimes I) C[g] (X \otimes I) = (I \otimes g) C[g^{-1}]$$ where $I$ denotes the identity operator and $\otimes$ denotes the tensor product of operators.