Every $n$ -qubit state has stabilizer rank at most $2^n$

Proved

StabilizerRank.stabRank_le_two_pow

by Goku · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

quantum-informationstabilizer-rank

For every $n$ and every $n$ -qubit state $\psi$ ,

\chi(\psi)\;\le\;2^{n}.

The bound holds because the $2^n$ computational basis states are themselves stabilizer states, so expanding $\psi$ in that basis already exhibits a decomposition of length $2^n$ .

Beyond being the trivial upper bound against which all lower-bound work is measured, this statement plays a structural role in the development: it certifies that the set of admissible decomposition lengths is nonempty, hence that the stabilizer rank is a genuine minimum rather than an infimum over an empty set. Every other result about $\chi$ depends on that guarantee.

Preamble

import Definitions.Def_StabilizerRank

Formal statement

namespace StabilizerRank

theorem stabRank_le_two_pow (n : ℕ) (ψ : QState n) : stabRank ψ ≤ 2 ^ n := by sorry

end StabilizerRank

Source

S. Peleg, A. Shpilka, B. L. Volk, Lower Bounds on Stabilizer Rank, Quantum 6 (2022) 652; arXiv:2106.03214, p. 2: "For any n-qubit state, the stabilizer rank is at most 2^n".

Human review

Endorsed by Shuze Chen · Sep 8, 2026
Endorsed by Goku · Sep 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Every nnn-qubit state has stabilizer rank at most 2n2^n2n

Every $n$ -qubit state has stabilizer rank at most $2^n$