Math and TheoryNo universal finite collapse of the upper PPT entanglement-cost hierarchy
Selected result in this collection
Problem and result
- Problem
- Finite collapse of the Lami–Mele–Regula upper PPT entanglement-cost hierarchy
- Posed in
- Lami, Mele and Regula, Physical Review Letters 134, 090202 (2025), Supplemental Material (the finite-collapse question accompanying Conjecture S33); left open for the upper κ hierarchy by Brinster, Kondra, Kampermann, Bruß and Wyderka (arXiv:2609.20698)
- Status
- Answered negatively
- Result
- For every q ≥ 1 a full-rank product-Bell-diagonal state in local dimension 2^((2q+4)4^q) has κ_{q+1}(ρ) < κ_q(ρ), so no fixed finite level of the upper PPT entanglement-cost hierarchy is exact for all states.
Abstract
For every integer q ≥ 1 there is a bipartite density matrix ρ_q with κ_{q+1}(ρ_q) < κ_q(ρ_q) in the upper hierarchy of semidefinite programs of Lami, Mele and Regula, whose logarithms converge to the exact entanglement cost under PPT operations. The witnesses are full-rank product-Bell-diagonal states in local dimension 2^((2q+4)4^q), and the auxiliary matrices are unrestricted. Hence no fixed finite upper level is exact for all states. The proof builds arbitrarily long strictly positive reverse orbits of the absolute partial transpose by a weighted-sign argument and converts full support into a quantitative gap for every shorter chain. Brinster et al. had proved the corresponding all-depth statement for the lower χ hierarchy and left the upper question open. The theorem does not give one fixed state or dimension with infinitely many strict levels.
Details
- Year
- 2026
- Discipline
- Mathematical physics
- Area
- Quantum information
- Subject
- Quantum information
- Result type
- Theorem resolving an open question and reproducible proof package
- Formal proof
- Standalone Lean package
- Family
upper-ppt-hierarchy- Keywords
- entanglement cost, PPT operations, semidefinite hierarchy, partial transpose, exact PPT entanglement cost, Bell-diagonal states, Lami–Mele–Regula
Statement and scope
Formal scope. The strict separation at every adjacent level, for the actual semidefinite programs with unrestricted complex auxiliaries and positive-definite trace-one states with positive Bell coefficients, and the absence of a universal finite collapse are formalized in 17 Lean modules. The operational exact-cost and tensor-multiplicativity consequences use published theorems of Lami, Mele and Regula.
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.pdf367 KB- PDF on GitHub
papers/physics/ upper-ppt-hierarchy/ manuscript.pdf - LaTeX source
papers/physics/ upper-ppt-hierarchy/ 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/ upper-ppt-hierarchy/ - Lean project
papers/19 Lean filesphysics/ upper-ppt-hierarchy/ lean/ - Lakefile
papers/physics/ upper-ppt-hierarchy/ lean/ lakefile.lean - Toolchain
leanprover/lean4:v4.19.0 - Library roots
Reproduce
The commands below are quoted from papers/, which gives their context and working directory.
lake exe cache get
python3 verify_release.py --lean-home "$(lean --print-prefix)" \
--mathlib .lake/packages/mathlib --packages-dir .lake/packages --out /tmp/upper-ppt-verification- README
papers/physics/ upper-ppt-hierarchy/ README.md - Verification guide
papers/physics/ upper-ppt-hierarchy/ verification/ README.md - Verification record
papers/physics/ upper-ppt-hierarchy/ VERIFICATION.md - Authorship
papers/physics/ upper-ppt-hierarchy/ AUTHORSHIP.md - Repository guide
verification/README.md - Unfinished proofs
UNFINISHED.md
Source and prior work
Prior work. Lami, Mele and Regula, 2025; Brinster, Kondra, Kampermann, Bruß and Wyderka, 2026.
Questions and answers
Does the Lami–Mele–Regula upper hierarchy collapse at a finite level?
No fixed level works for all states: for every q ≥ 1 there is a full-rank product-Bell-diagonal state ρ with κ_{q+1}(ρ) < κ_q(ρ). The witness dimension 2^((2q+4)4^q) grows with q, so the result does not give one fixed state or dimension with infinitely many strict levels, and it does not rule out other single-letter formulas for exact PPT cost.
What was known before this result?
Brinster, Kondra, Kampermann, Bruß and Wyderka (arXiv:2609.20698, September 2026) proved all-depth noncollapse of the lower χ hierarchy and left the upper κ question open; their Bell-transform formalism and telescoping dual identity are used here. Historical priority is not certified.
Is the proof formally verified?
The strict separation at every adjacent level, for the actual semidefinite programs with unrestricted complex auxiliaries, is formalized in 17 Lean 4 modules. The operational consequences for exact PPT cost and tensor multiplicativity rely on published theorems of Lami, Mele and Regula and are not formalized.
Cite
Citation file papers/. For the whole collection, use CITATION.cff or CITATION.bib.
@misc{goyal2026upperppthierarchy,
author = {Goyal, Dev D.},
title = {No Universal Finite Collapse of the Upper {PPT} Entanglement-Cost Hierarchy},
year = {2026},
month = oct,
note = {Preprint. Fully autonomous agentic research; publication responsibility: Dev D. Goyal},
url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/physics/upper-ppt-hierarchy}
}