The standard-form encoding network maps |c⟩ to the encoded basis state (4.8)

Open

QAlgorithms.GottesmanThesis.stabEncoder_encodes

by Goku · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

gottesman-thesislecture-notesquantum-information

Let a stabilizer on $n=m+k$ qubits ( $m=n-k$ generators) be given in the standard form (4.3) of §4.1,

\left(\begin{array}{ccc|ccc} I & A_1 & A_2 & B & C_1 & C_2\\ 0 & 0 & 0 & D & I & E\end{array}\right),

with $r$ rows in the first block, and assume its rows commute: $H_xH_z^{\mathsf T}+H_zH_x^{\mathsf T}=0$ . For a binary row $(a\,|\,b)$ write $P(a|b)=\bigotimes_q \sigma_z^{b_q}\sigma_x^{a_q}$ (the real form, sign $+1$ ). Let $M_i=P(\text{row } i)$ be the generators and let $\bar X_1,\dots,\bar X_k$ be the logical $\sigma_x$ operators in the standard form of p.40: $\bar X_i=P(0\,u_2\,e_i\,|\,v_1\,0\,0)$ with $u_2$ the $i$ -th row of $E^{\mathsf T}$ and $v_1$ the $i$ -th row of $E^{\mathsf T}C_1^{\mathsf T}+C_2^{\mathsf T}$ .

Let $U_{\mathrm{enc}}$ be the encoding network of §4.2 (with the author's errata): first, for each $i$ , the controlled-NOTs that apply $\bar X_i$ without its final $\sigma_x$ , controlled on qubit $n-k+i$ ; then, for $i=1,\dots,r$ in turn, the Hadamard $R$ on qubit $i$ , a $\sigma_z$ on qubit $i$ if $B_{ii}=1$ , and $M_i$ without its qubit- $i$ factor, controlled on qubit $i$ (controlled- $\sigma_z^{b}\sigma_x^{a}$ gates). Then for every $c=c_1\dots c_k\in\{0,1\}^k$ ,

U_{\mathrm{enc}}\,|0\dots0\rangle|c_1\dots c_k\rangle=\frac{(I+M_1)\cdots(I+M_{n-k})\,\bar X_1^{c_1}\cdots\bar X_k^{c_k}|0\dots0\rangle}{\big\|(I+M_1)\cdots(I+M_{n-k})\,\bar X_1^{c_1}\cdots\bar X_k^{c_k}|0\dots0\rangle\big\|},

and in particular the vector on the right-hand side is nonzero.

This is the correctness of Gottesman's general encoding circuit for stabilizer codes: the network prepares exactly the encoded basis states, with no leftover global phase.

Formalization Note The errata are built in: the Hadamard on qubit $i$ comes just before that qubit's control operations, controlled- $Y$ gates are controlled- $\sigma_z\sigma_x$ gates in the real form, and every generator has sign $+1$ . The page writes encoded states unnormalized; the unitary network yields the normalized vector. Since the real form $\sigma_z\sigma_x=i\sigma_y$ , a generator with an odd number of $(1|1)$ positions is $i$ times a Hermitian Pauli operator; the identity is the one the page's network computes in this convention.

Preamble

import Definitions.Def_QAlgorithms_Defs_BinaryStabilizer
set_option autoImplicit false

Formal statement

namespace QAlgorithms.GottesmanThesis


/-- Gottesman thesis pp.41–43, §4.2 (unnumbered; equation (4.8)), with the author's errata:
for a stabilizer in standard form (4.3) with rank parameter `r` and commuting rows, and the
logical `X̄` operators in the standard form of p.40 (`U₃ = I`, `V₃ = 0`, `U₂ = Eᵀ`,
`V₁ = EᵀC₁ᵀ + C₂ᵀ`), the encoding network of §4.2 maps the input `|0…0⟩|c₁…c_k⟩` (the first
`n − k` qubits in `|0⟩`, `|c_i⟩` in qubit `n − k + i`) to the normalized encoded basis state
`(I + M₁)⋯(I + M_{n−k}) X̄₁^{c₁}⋯X̄_k^{c_k} |0…0⟩`.

The network (`stabEncoder`) is the controlled-NOT step (each `X̄_i` without its last `σx`,
controlled on qubit `n − k + i`), followed, for `i = 1, …, r` in turn, by `R` on qubit `i`, `σz`
on qubit `i` if `B_ii = 1`, and `M_i` (without its qubit-`i` factor) controlled on qubit `i`
(erratum: Hadamard just before the qubit's control dots). Generators and `X̄`'s are the
real-form Pauli products `σz^b σx^a` with sign `+1` (errata: controlled-`Y` is controlled-`XZ`;
the method needs every generator of sign `+1`). -/
theorem stabEncoder_encodes {m k r : ℕ} (Hx Hz : Matrix (Fin m) (Fin (m + k)) (ZMod 2))
    (hstd : IsStandardForm r Hx Hz) (hcomm : SymplecticCommuting Hx Hz) (c : Qubits k) :
    act (stabEncoder r Hx Hz).unitary (ket (Fin.append (fun _ : Fin m => false) c)) =
      normalizedVec (stabEncodedState r Hx Hz c) := by
  sorry

end QAlgorithms.GottesmanThesis

Source

Daniel Gottesman, Stabilizer Codes and Quantum Error Correction, 1997 thesis, downloaded arXiv v1 PDF; PDF title page now prints 2024, PDF p. 41, §4.2. https://arxiv.org/pdf/quant-ph/9705052v1

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting. Fix natural numbers $m, k, r$ and $m\times(m+k)$ matrices $H_x, H_z$ over $\mathbb{F}_2$ . The register has $m+k$ qubits on wires $0,\dots,m+k-1$ . Basis states $|z\rangle$ are labelled by bit strings $z \in \{0,1\}^{m+k}$ , with wire $0$ the most significant.

Hypotheses.

Standard form with parameter $r$ :
- $r\le m$ ;
- $(H_x)_{ij}=\delta_{ij}$ for $i,j<r$ ;
- row $i$ of $H_x$ is zero for every $i\ge r$ ;
- $(H_z)_{ij}=\delta_{ij}$ for $i\ge r$ and $r\le j<m$ .
Symplectic commutation: $H_xH_z^{\mathsf T}+H_zH_x^{\mathsf T}=0$ over $\mathbb{F}_2$ .

No linear-independence hypothesis is assumed.

Input. Take an arbitrary $c\in\{0,1\}^k$ . The input is the basis state $|0^m c\rangle$ : wires $0,\dots,m-1$ are $0$ and wire $m+i$ carries $c_i$ .

The circuit. The encoder is a list of gates applied in list order, first gate first. If the list is $g_1,\dots,g_L$ , its unitary is $U = E_L\cdots E_1$ . Each $E$ acts as the gate's matrix on its wires (in the listed order) and as the identity on all other wires.

A controlled gate $C(V)$ with control wire $a$ and target wire $b$ acts as

|0\rangle\langle 0|_a\otimes 1 + |1\rangle\langle1|_a\otimes V_b.

Here $X=\begin{pmatrix}0&1\\1&0\end{pmatrix}$ , $Z=\operatorname{diag}(1,-1)$ , and $H$ is the Hadamard gate.

The gate list is the concatenation of two parts.

Part 1. For $i=0,\dots,k-1$ $i = 0, \dots, k - 1$ in order, and within that for $j=0,\dots,m-1$ $j = 0, \dots, m - 1$ in order:
- if $j\ge r$ and $(H_z)_{j,m+i}=1$ , apply $C(X)$ with control wire $m+i$ and target wire $j$ .
Part 2. For $i=0,\dots,m-1$ $i = 0, \dots, m - 1$ in order, and only when $i<r$ $i < r$ :
1. apply $H$ on wire $i$ ;
2. then, if $(H_z)_{ii}=1$ , apply $Z$ on wire $i$ ;
3. then, for $q=0,\dots,m+k-1$ in order with $q\ne i$ and $\big((H_x)_{iq},(H_z)_{iq}\big)\ne(0,0)$ , apply $C(V_{iq})$ with control wire $i$ and target wire $q$ , where

V_{iq}=Z^{(H_z)_{iq}}X^{(H_x)_{iq}}.

Rows $i\ge r$ contribute no gates.

The target vector. For $a,b\in\mathbb{F}_2^{m+k}$ , define the unphased Pauli operator

P(a,b)=\bigotimes_{q}Z^{b_q}X^{a_q}.

In particular, $Y$ appears as $ZX$ .

For each $i<k$ , the logical operator is $\bar X_i=P(a^{(i)},b^{(i)})$ , where:

for $j<m$ :

a^{(i)}_j=\begin{cases}(H_z)_{j,m+i} & j\ge r,\\ 0 & j<r;\end{cases}

for $j\ge m$ : $a^{(i)}_j=1$ if $j=m+i$ , and $0$ otherwise;
for $j<r$ :

b^{(i)}_j=\sum_{r\le l<m}(H_z)_{l,m+i}(H_z)_{jl}+(H_z)_{j,m+i},

computed in $\mathbb{F}_2$ ;

for $j\ge r$ : $b^{(i)}_j=0$ .

Define

\Psi_c=\Big(\prod_{i=m-1}^{0}\big(1+P(\text{row}_i H_x,\text{row}_i H_z)\big)\Big)\Big(\prod_{i=k-1}^{0}\bar X_i^{\,c_i}\Big)|0^{m+k}\rangle.

In each product the factor with index $0$ is applied first. The factors $1+P$ carry no $\tfrac12$ .

Conclusion.

U\,|0^m c\rangle=\frac{\Psi_c}{\|\Psi_c\|}.

The normalization uses the convention $\|0\|^{-1}=0$ . So if $\Psi_c=0$ , the right-hand side is the zero vector.

Degenerate case. When $m=0$ the circuit is empty, so $U=1$ .

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Goku · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph