Basis states are exactly tensor products of single-qubit basis states

Proved

QAlgorithms.Nannicini.basisState_iff_prod_basisStates

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

lecture-notesnanniciniquantum-information

Let $q>1$ and let $|\psi\rangle\in(\mathbb C^2)^{\otimes q}$ be a $q$ -qubit quantum state, i.e. a unit vector. Recall (Def. 1.16) that $|\psi\rangle$ is a basis state if $|\psi\rangle=\alpha_k|\vec k\rangle$ for some $\vec k\in\{0,1\}^q$ and some $\alpha_k\in\mathbb C$ with $|\alpha_k|^2=1$ . Then $|\psi\rangle$ is a basis state if and only if there are single-qubit states $|\psi_1\rangle,\dots,|\psi_q\rangle\in\mathbb C^2$ , each of which is a basis state, such that

|\psi\rangle=|\psi_1\rangle\otimes|\psi_2\rangle\otimes\cdots\otimes|\psi_q\rangle .

The statement shows that basis states are always product states, in contrast with superpositions, which can be entangled.

Formalization Note The $q$ -qubit register is indexed by $\{0,1\}^q$ with the first qubit as the most significant bit; the tensor product of the single-qubit states is the vector whose $\vec z$ -coordinate is $\prod_{i}\langle z_i|\psi_i\rangle$ , with qubit $i$ of the source being the $i$ -th factor. Being a basis state already forces unit norm, so the unit-norm hypotheses are stated for fidelity to the source but are redundant.

Preamble

import Definitions.Def_QAlgorithms_Defs_Measurement
set_option autoImplicit false

Formal statement

namespace QAlgorithms.Nannicini


/-- Nannicini p.14, Proposition 1.19: a `q`-qubit register, `q > 1`, is in a basis state
(Def. 1.16: `|ψ⟩ = α_k |k⟩` with `|α_k|² = 1`) if and only if its state is the tensor product
`|ψ_1⟩ ⊗ ⋯ ⊗ |ψ_q⟩` of `q` single-qubit states each of which is a basis state. Wire `i` is the
source's qubit `i + 1` (the first qubit is the most significant). -/
theorem basisState_iff_prod_basisStates {q : ℕ} (hq : 1 < q)
    (ψ : EuclideanSpace ℂ (Qubits q)) (hψ : IsState ψ) :
    IsBasisState ψ ↔ ∃ φ : Fin q → EuclideanSpace ℂ Bool,
      (∀ i, IsState (φ i) ∧ IsBasisState (φ i)) ∧ ψ = prodState φ := by
  sorry




end QAlgorithms.Nannicini

Source

Giacomo Nannicini, Quantum algorithms for optimizers, 2025, v5; notes dated 9 July 2025, PDF p. 14, Proposition 1.19. https://arxiv.org/pdf/2408.07086v5

Read-back

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

Let $q$ be a natural number with $q > 1$ (so $q \ge 2$ ). Index an $q$ -qubit vector by bit strings $z = (z_0,\dots,z_{q-1}) \in \{0,1\}^q$ . Let $\psi \in \mathbb{C}^{\{0,1\}^q}$ be a unit vector, $\|\psi\| = 1$ .

Call a vector a basis state if it equals $\alpha\, e_k$ for some index $k$ and some complex $\alpha$ with $|\alpha| = 1$ . Here $e_k$ is the standard basis vector at $k$ .

For a family $\varphi_0,\dots,\varphi_{q-1}$ of single-qubit vectors in $\mathbb{C}^{\{0,1\}}$ , define the product vector $\varphi_0\otimes\cdots\otimes\varphi_{q-1}$ by

(\varphi_0\otimes\cdots\otimes\varphi_{q-1})_z = \prod_{i=0}^{q-1} (\varphi_i)_{z_i}.

The theorem states that $\psi$ is a basis state if and only if there exist single-qubit vectors $\varphi_0,\dots,\varphi_{q-1}$ with both of the following properties:

each $\varphi_i$ has unit norm and is itself a basis state of $\mathbb{C}^{\{0,1\}}$ , i.e. of the form $\beta_i e_{b_i}$ with $|\beta_i| = 1$ and $b_i \in \{0,1\}$ ;
$\psi = \varphi_0\otimes\cdots\otimes\varphi_{q-1}$ .

The cases $q = 0$ and $q = 1$ are excluded by the hypothesis.

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