Clifford generators conjugate Paulis to Paulis (GK-2: the Gottesman–Knill mechanism)

Category: 1-Mathlib (CSD-free).

Glossary: https://glossary.constraintsurfacedynamics.com/gottesman-knill/ Plain-language, CSD-role and formal statements of the Gottesman–Knill theorem, with this module as its Lean anchor. Kept symmetric by scripts/check-glossary.sh.

The three Clifford generator families as concrete coordinate operators — cnotGate j k (controlled-NOT), sGate j (the phase gate), hGate j (the single-qubit Hadamard) — and the theorem family that IS the Gottesman–Knill mechanism: conjugation by each generator maps every Pauli operator to a phase times a Pauli operator, with the label map explicit and 𝔽₂-linear (plan specs/gottesman-knill-plan.md, brick GK-2):

• ★ cnotGate_conj_pauliOp — CNOT_{jk} · X^a Z^b · CNOT_{jk} = X^{σa} Z^{σᵀb} with σ = cnotFlip j k (add bit j into bit k), σᵀ = cnotFlip k j; no phase.
• ★ sGate_conj_pauliOp — S_j · X^a Z^b · S_j† = i^{a_j} · X^a Z^{b + a_j e_j}.
• ★ hGate_conj_pauliOp — H_j · X^a Z^b · H_j = (−1)^{a_j b_j} · X^{a[j↦b_j]} Z^{b[j↦a_j]} (swap a_j ↔ b_j).

Why this is Gottesman–Knill. In the Heisenberg picture a Pauli is 2n bits and a phase, and each generator updates the bits by the explicit 𝔽₂-linear maps above — so a stabiliser description of a state (n commuting Paulis) is carried through any circuit of these gates by linear algebra over 𝔽₂. That closure is proved here in full. Honest scope: the "classically simulable in polynomial time" reading is a complexity claim about that update rule; the corpus has no computation model and does not state it — no circuit datatype, no gate count, no measurement-update rule (the stabiliser-measurement layer is GK-3 in the plan, gated). hGate j is the single-qubit sibling of Hadamard.lean's all-qubits H^⊗n, not a replacement for it.

Update helpers on the bitstring group

def QuantumInfo.cnotFlip {n : ℕ} (j k : Fin n) (z : Fin n → Fin 2) : Fin n → Fin 2

σ_{jk}: add bit j into bit k. Self-inverse for j ≠ k; the label map of CNOT.

Equations

• QuantumInfo.cnotFlip j k z = Function.update z k (z k + z j)

theorem QuantumInfo.cnotFlip_apply_ne {n : ℕ} (j k : Fin n) (z : Fin n → Fin 2) {i : Fin n} (hik : i ≠ k) : cnotFlip j k z i = z i

theorem QuantumInfo.cnotFlip_apply_k {n : ℕ} (j k : Fin n) (z : Fin n → Fin 2) : cnotFlip j k z k = z k + z j

theorem QuantumInfo.cnotFlip_add {n : ℕ} (j k : Fin n) (z w : Fin n → Fin 2) : cnotFlip j k (z + w) = cnotFlip j k z + cnotFlip j k w

The flip is additive.

theorem QuantumInfo.cnotFlip_invol {n : ℕ} (j k : Fin n) (hjk : j ≠ k) (z : Fin n → Fin 2) : cnotFlip j k (cnotFlip j k z) = z

The flip is an involution (j ≠ k).

theorem QuantumInfo.update_add_right {n : ℕ} (z a : Fin n → Fin 2) (j : Fin n) (v : Fin 2) : Function.update z j v + a = Function.update (z + a) j (v + a j)

Updating then translating is translating then updating (with the shifted value).

theorem QuantumInfo.add_update_right {n : ℕ} (z a : Fin n → Fin 2) (j : Fin n) (v : Fin 2) : z + Function.update a j v = Function.update (z + a) j (z j + v)

Translating by an update.

The CNOT gate

noncomputable def QuantumInfo.cnotGate {n : ℕ} (j k : Fin n) (ψ : QReg n) : QReg n

The controlled-NOT CNOT_{jk} (control j, target k): the permutation operator of cnotFlip j k.

Equations

• QuantumInfo.cnotGate j k ψ = (WithLp.equiv 2 ((Fin n → Fin 2) → ℂ)).symm fun (z : Fin n → Fin 2) => ψ.ofLp (QuantumInfo.cnotFlip j k z)

@[simp]

theorem QuantumInfo.cnotGate_apply {n : ℕ} (j k : Fin n) (ψ : QReg n) (z : Fin n → Fin 2) : (cnotGate j k ψ).ofLp z = ψ.ofLp (cnotFlip j k z)

theorem QuantumInfo.cnotGate_cnotGate {n : ℕ} (j k : Fin n) (hjk : j ≠ k) (ψ : QReg n) : cnotGate j k (cnotGate j k ψ) = ψ

CNOT is self-inverse (j ≠ k).

theorem QuantumInfo.cnotGate_conj_pauliOp {n : ℕ} (j k : Fin n) (hjk : j ≠ k) (a b : Fin n → Fin 2) (ψ : QReg n) : cnotGate j k (pauliOp a b (cnotGate j k ψ)) = pauliOp (cnotFlip j k a) (cnotFlip k j b) ψ

★ CNOT conjugation: CNOT_{jk} · X^a Z^b · CNOT_{jk} = X^{σa} Z^{σᵀb} — the X label gains a_j at bit k, the Z label gains b_k at bit j, and there is no phase.

The phase gate

noncomputable def QuantumInfo.sGate {n : ℕ} (j : Fin n) (ψ : QReg n) : QReg n

The phase gate S_j: phase i on the z_j = 1 branch.

Equations

• QuantumInfo.sGate j ψ = (WithLp.equiv 2 ((Fin n → Fin 2) → ℂ)).symm fun (z : Fin n → Fin 2) => Complex.I ^ ↑(z j) * ψ.ofLp z

noncomputable def QuantumInfo.sGateInv {n : ℕ} (j : Fin n) (ψ : QReg n) : QReg n

The inverse phase gate S_j†.

Equations

• QuantumInfo.sGateInv j ψ = (WithLp.equiv 2 ((Fin n → Fin 2) → ℂ)).symm fun (z : Fin n → Fin 2) => (-Complex.I) ^ ↑(z j) * ψ.ofLp z

@[simp]

theorem QuantumInfo.sGate_apply {n : ℕ} (j : Fin n) (ψ : QReg n) (z : Fin n → Fin 2) : (sGate j ψ).ofLp z = Complex.I ^ ↑(z j) * ψ.ofLp z

@[simp]

theorem QuantumInfo.sGateInv_apply {n : ℕ} (j : Fin n) (ψ : QReg n) (z : Fin n → Fin 2) : (sGateInv j ψ).ofLp z = (-Complex.I) ^ ↑(z j) * ψ.ofLp z

theorem QuantumInfo.sGate_sGateInv {n : ℕ} (j : Fin n) (ψ : QReg n) : sGate j (sGateInv j ψ) = ψ

theorem QuantumInfo.sGateInv_sGate {n : ℕ} (j : Fin n) (ψ : QReg n) : sGateInv j (sGate j ψ) = ψ

theorem QuantumInfo.sGate_conj_pauliOp {n : ℕ} (j : Fin n) (a b : Fin n → Fin 2) (ψ : QReg n) : sGate j (pauliOp a b (sGateInv j ψ)) = Complex.I ^ ↑(a j) • pauliOp a (Function.update b j (b j + a j)) ψ

★ Phase-gate conjugation: S_j · X^a Z^b · S_j† = i^{a_j} · X^a Z^{b[j ↦ b_j+a_j]} — the Z label gains a_j at bit j, with phase i^{a_j} (this is S X S† = Y).

The Hadamard gate (single qubit)

noncomputable def QuantumInfo.hGate {n : ℕ} (j : Fin n) (ψ : QReg n) : QReg n

The single-qubit Hadamard H_j: (H_j ψ)(z) = (1/√2) ∑_v (−1)^{z_j·v} ψ(z[j ↦ v]).

Equations

• QuantumInfo.hGate j ψ = (WithLp.equiv 2 ((Fin n → Fin 2) → ℂ)).symm fun (z : Fin n → Fin 2) => (↑√2)⁻¹ * ∑ v : Fin 2, QuantumInfo.signChar (z j * v) * ψ.ofLp (Function.update z j v)

@[simp]

theorem QuantumInfo.hGate_apply {n : ℕ} (j : Fin n) (ψ : QReg n) (z : Fin n → Fin 2) : (hGate j ψ).ofLp z = (↑√2)⁻¹ * ∑ v : Fin 2, signChar (z j * v) * ψ.ofLp (Function.update z j v)

theorem QuantumInfo.sqrt_two_inv_sq : (↑√2)⁻¹ * (↑√2)⁻¹ * 2 = 1

The normalisation constant: (1/√2)·(1/√2)·2 = 1.

theorem QuantumInfo.hGate_hGate {n : ℕ} (j : Fin n) (ψ : QReg n) : hGate j (hGate j ψ) = ψ

H_j is self-inverse.

theorem QuantumInfo.hGate_conj_pauliOp {n : ℕ} (j : Fin n) (a b : Fin n → Fin 2) (ψ : QReg n) : hGate j (pauliOp a b (hGate j ψ)) = signChar (a j * b j) • pauliOp (Function.update a j (b j)) (Function.update b j (a j)) ψ

★ Hadamard conjugation: H_j · X^a Z^b · H_j = (−1)^{a_j b_j} · X^{a[j↦b_j]} Z^{b[j↦a_j]} — the X and Z labels swap at bit j, with sign (−1)^{a_j b_j} (this is HXH = Z, HZH = X, HYH = −Y).