No-Cloning: no quantum operation copies every state

Proved

QAlgorithms.GottesmanIntro.noCloning

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

gottesman-introlecture-notesquantum-information

This is the No-Cloning theorem.

Let $\mathcal H$ be a finite-dimensional Hilbert space with $\dim\mathcal H\ge 2$ . A quantum operation from $\mathcal H$ to $\mathcal H\otimes\mathcal H$ is a map on operators of the form

\rho\mapsto\sum_i E_i\,\rho\,E_i^\dagger,\qquad \sum_i E_i^\dagger E_i=I,

with finitely many operators $E_i:\mathcal H\to\mathcal H\otimes\mathcal H$ . No quantum operation $\Phi$ satisfies

\Phi\big(|\psi\rangle\langle\psi|\big)=\big(|\psi\rangle\otimes|\psi\rangle\big)\big(\langle\psi|\otimes\langle\psi|\big)

for every unit vector $|\psi\rangle\in\mathcal H$ .

The theorem shows that a quantum repetition code $|\psi\rangle\mapsto|\psi\rangle^{\otimes 3}$ cannot exist, which motivates the subspace codes of the following sections.

Formalization Note States enter as density matrices, so the copy is required only up to a global phase. The class of operations is the source's general quantum operation, eq. (23). It contains the unitary-with-blank-ancilla operations of the proof. The hypothesis $\dim\mathcal H\ge2$ excludes the one-dimensional space, where the identity map clones.

Preamble

import Definitions.Def_QAlgorithms_Defs_FTCircuit
set_option autoImplicit false

Formal statement

namespace QAlgorithms.GottesmanIntro

open scoped Matrix

open QAlgorithms Stabilizer

/-- Gottesman intro p.2, Theorem 1 (No-Cloning): on a Hilbert space of dimension at least 2,
no quantum operation (eq. (23), p.4–5) maps `|ψ⟩⟨ψ|` to `(|ψ⟩ ⊗ |ψ⟩)(⟨ψ| ⊗ ⟨ψ|)` for every
state `|ψ⟩`. -/
theorem noCloning {ι : Type*} [Fintype ι] [DecidableEq ι] (hι : 2 ≤ Fintype.card ι)
    (Φ : Superop ι (ι × ι)) (hΦ : IsChannel Φ) :
    ¬ ∀ ψ : EuclideanSpace ℂ ι, IsState ψ → Φ (pureDensity ψ) = pureDensity (tensorVec ψ ψ) := by
  sorry




end QAlgorithms.GottesmanIntro

Source

Daniel Gottesman, An Introduction to Quantum Error Correction and Fault-Tolerant Quantum Computation, 2009, v1, PDF p. 2, Theorem 1. https://arxiv.org/pdf/0904.2557v1

Read-back

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

Setting. Let $\iota$ be a finite index set with decidable equality and at least two elements, $|\iota| \ge 2$ . A state space is $\mathbb{C}^\iota$ with the standard Euclidean norm.

Hypothesis on $\Phi$ . $\Phi$ is a map sending $\iota\times\iota$ complex matrices to $(\iota\times\iota)\times(\iota\times\iota)$ complex matrices, i.e. an operator on $\mathbb{C}^\iota$ goes to an operator on $\mathbb{C}^\iota\otimes\mathbb{C}^\iota$ . It is assumed to be a channel in Kraus form: there exist $m\in\mathbb{N}$ and matrices $E_1,\dots,E_m$ of size $(\iota\times\iota)\times\iota$ such that

\sum_{j} E_j^\dagger E_j = I_\iota \quad\text{and}\quad \Phi(\rho)=\sum_j E_j\,\rho\,E_j^\dagger \ \text{ for every matrix } \rho.

Notation. For a vector $\psi$ , write $|\psi\rangle\langle\psi|$ for the matrix with entries $(a,b)\mapsto \psi_a\overline{\psi_b}$ . Write $\psi\otimes\psi$ for the vector on $\iota\times\iota$ with entries $(a,b)\mapsto\psi_a\psi_b$ .

Conclusion. It is not the case that every unit vector $\psi\in\mathbb{C}^\iota$ (with $\|\psi\|=1$ ) satisfies

\Phi\big(|\psi\rangle\langle\psi|\big)=|\psi\otimes\psi\rangle\langle\psi\otimes\psi|.

The channel maps $\iota$ directly to $\iota\times\iota$ . No separate blank input register or ancilla appears in the statement.

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