A sum-of-squares proof of the four-qubit Higuchi–Sudbery entropy bound

Dev D. Goyal

A sum-of-squares proof of the four-qubit Higuchi–Sudbery entropy bound

Dev D. Goyal · 2026 · Research preprint, not externally peer reviewed

Problem and result

Problem: Higuchi–Sudbery problem: maximal average two-qubit marginal entropy of four qubits
Posed in: Higuchi and Sudbery, 'How entangled can two couples get?', Physics Letters A 273 (2000), 213–217, which proposed the candidate maximizing state
Status: Proved
Result: For every pure four-qubit state the average von Neumann entropy of the three two-qubit marginals ρ_AB, ρ_AC, ρ_AD is at most log 2 + (1/2) log 3 (natural logarithms), and the Higuchi–Sudbery state attains it.

Abstract

The average von Neumann entropy of the three two-qubit marginals of a pure four-qubit state is at most log(2) + log(3)/2. The Higuchi–Sudbery state attains this bound.

The proof uses all sixteen complex amplitudes, actual reduced-matrix eigenvalues, an exact sum-of-squares identity, and an explicit maximizing state.

Details

Year: 2026
Discipline: Mathematical physics
Area: Quantum information
Subject: Quantum information
Result type: Four-qubit entropy bound with attainment
Formal proof: Standalone Lean package
Family: higuchi-sudbery
Keywords: Higuchi–Sudbery, Higuchi-Sudbery state, four-qubit entanglement, marginal entropy, maximally entangled four qubits, sum of squares

Statement and scope

Formal scope. The proof uses all sixteen complex amplitudes, actual reduced-matrix eigenvalues, an exact sum-of-squares identity, and an explicit maximizing state.

A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.

Manuscript

PDF on this site: manuscript.pdf 348 KB
PDF on GitHub: papers/physics/higuchi-sudbery/manuscript.pdf
LaTeX source: papers/physics/higuchi-sudbery/manuscript.tex

Formal proof

This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.

Proof package

papers/physics/higuchi-sudbery/ 51 Lean files

Lakefile

papers/physics/higuchi-sudbery/lakefile.lean

Toolchain

leanprover/lean4:v4.35.0

Library roots

Reproduce

The commands below are quoted from papers/physics/higuchi-sudbery/README.md, which gives their context and working directory.

Reproduce the proof

lake exe cache get
lake build
lake env lean -DwarningAsError=true HS/Audit.lean

README: papers/physics/higuchi-sudbery/README.md
Verification record: papers/physics/higuchi-sudbery/VERIFICATION.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Priority and subsequent correspondence. On 30 October 2026, through correspondence with Dr. Jef Pauwels, I learned that the Omega Institute had registered this problem on 5 October 2026 and publicly committed a claimed Lean proof on 7 October 2026. Our 272-term sum-of-squares certificates are algebraically equivalent, and I make no originality or priority claim. Priority and novelty record.

Source. Higuchi and Sudbery, 2000. The Omega Institute publicly registered this problem on 5 October 2026 and committed a claimed Lean proof on 7 October 2026, with an algebraically equivalent sum-of-squares certificate; I make no originality or priority claim. See PRIORITY_AND_NOVELTY.md.

Questions and answers

Is the Higuchi–Sudbery state the global maximizer of average two-qubit entropy?

This preprint proves that the average von Neumann entropy of the three two-qubit marginals of any pure four-qubit state is at most log 2 + (1/2) log 3, about 1.79248 bits, and that the Higuchi–Sudbery state attains it, with no restriction on the one-qubit marginals. It does not classify all maximizers.

Has this bound appeared in earlier work?

Yes. The Omega Institute publicly registered this problem on 5 October 2026 and committed a claimed Lean proof on 7 October 2026, before this preprint's release on 27 October 2026, and the two 272-term sum-of-squares certificates are algebraically equivalent; the author makes no originality or priority claim. Gour and Wallach had proved the bound on the restricted family with maximally mixed one-qubit marginals.

Is the proof formally verified?

The Lean 4 formalization covers all sixteen complex amplitudes, the actual reduced-matrix eigenvalues, the exact sum-of-squares identity and an explicit maximizing state. The Omega Institute's Lean proof has not been independently checked, and this work is an unrefereed preprint.

Cite

Citation file papers/physics/higuchi-sudbery/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@misc{goyal2026higuchisudbery,
  author = {Goyal, Dev D.},
  title = {A sum-of-squares proof of the four-qubit Higuchi–Sudbery entropy bound},
  year = {2026},
  howpublished = {Preprint},
  url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/physics/higuchi-sudbery},
  note = {Fully autonomous agentic research generated by AI systems.}
}