The most entangled states of four and seven qubits
Antony Lewis
quant-ph
Nov 3, 2026 · v2
TL;DR
Formalizes the four-qubit entropy maximum, its equality case, spectral corollaries, stability estimates and icosahedral-family computations in Lean 4 with Mathlib.
Abstract
Pure states of four and seven qubits cannot be maximally entangled across every balanced bipartition; we determine how entangled they can be on average. For four qubits we prove the conjecture of Higuchi and Sudbery: the mean von Neumann entropy of the three $2|2$ cuts is at most $1+\tfrac12\log_2 3$ bits, with equality exactly on the local-unitary orbits of their state $M_4$ and its complex conjugate. For seven qubits the mean purity of the 35 balanced $3|4$ cuts is at least $121/917$ and their mean entropy is at most $2.965356029\ldots$ bits, each with a unique optimiser up to local unitaries and qubit permutations. The two optimisers are distinct members of one icosahedral family, so minimum purity and maximum entropy select different states. The proofs bound moments of the marginal spectra by positive identities on several copies of the state, some of them spin flipped, and bound the entropy by a polynomial in those moments. The four-qubit maximum has an analytic proof; the seven-qubit proofs, and some of the four-qubit refinements below, are computer-assisted, with exact arithmetic and rigorous error bounds. We also prove the Gour–Wallach conjecture for Rényi entropies of all orders, with the maximiser changing from $M_4$ to cluster states at $q_*\approx1.588$, and obtain sharp Tsallis bounds, mixed-state bounds and quantitative stability.
Problem
Pure states of four and seven qubits cannot be maximally entangled across every balanced bipartition. The question is how large the mean entanglement across balanced cuts can be, including the Higuchi–Sudbery conjecture for four qubits and the Gour–Wallach conjecture for Rényi entropies.
Approach
Moments of the marginal spectra are bounded using positive identities on several copies of the state, some of them spin-flipped. The entropy is then bounded by a polynomial (cubic majorant) in those moments. The seven-qubit proofs are computer-assisted, using exact arithmetic and rigorous error bounds. The four-qubit results were formalized in Lean 4 with Mathlib by AI agents; two finite certificates rely on compiled code.
Results
For four qubits, the mean 2|2 entropy is at most 1+½log₂3, with equality exactly on the local-unitary orbits of M₄ and its conjugate. For seven qubits, the mean 3|4 purity is at least 121/917 and the mean entropy is at most ≈2.965356 bits, with distinct icosahedral optimisers. The Gour–Wallach Rényi conjecture is proved with crossover at q*≈1.588, along with Tsallis, mixed-state and stability bounds.