Bravyi--Smith--Smolin: $\chi(|H^{\otimes 6}\rangle)\le 7$

Proved

StabilizerRank.stabRank_hState_six_le_seven

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

quantum-circuit-simulationquantum-informationstabilizer-rank

The six-fold tensor power of the magic state admits a decomposition into only seven stabilizer states:

\chi\bigl(|H^{\otimes 6}\rangle\bigr)\;\le\;7 .

The trivial bound for six qubits is $2^6=64$ , so this is a substantial saving, and it is the source of the best known asymptotic upper bound: applying it blockwise to $6k$ qubits gives $\chi(|H^{\otimes n}\rangle)\le 7^{\,n/6}\le 2^{\,0.468\,n}$ , which is what makes stabilizer-rank simulation of Clifford-plus-magic-state circuits competitive in practice.

The statement is finite and fully explicit: establishing it amounts to exhibiting seven stabilizer states of six qubits and seven complex coefficients, then verifying $2^6=64$ coordinate identities. It therefore requires no asymptotic analysis, only a concrete witness.

Preamble

import Definitions.Def_StabilizerRank

Formal statement

namespace StabilizerRank

theorem stabRank_hState_six_le_seven : stabRank (hState 6) ≤ 7 := 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: "Bravyi, Smith and Smolin [7] proved that chi(H^{ox 6}) <= 7 which implies that chi(H^{ox n}) <= 7^{n/6} <= 2^{0.468n}". Cited there as reference [7]; the bound is due to Bravyi, Smith and Smolin, and is quoted here from Peleg-Shpilka-Volk rather than from the original paper.

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

Bravyi--Smith--Smolin: χ(∣H⊗6⟩)≤7\chi(|H^{\otimes 6}\rangle)\le 7χ(∣H⊗6⟩)≤7

Bravyi--Smith--Smolin: $\chi(|H^{\otimes 6}\rangle)\le 7$