Entanglement Cost of Optimal Distributed Quantum State Purification
Jiayi Zhao, Chengkai Zhu, Xin Wang, Ge Bai
quant-ph
Sep 20, 2026 · v1
TL;DR
Formally verifies in Lean 4, using Mathlib and Lean-QIT, that pure resources enabling PPT instruments to attain the purification benchmark have at least one ebit.
Abstract
We determine the preshared entanglement required for spatially separated parties, restricted to local operations and classical communication, to attain globally optimal probabilistic two-copy purification of arbitrary bipartite pure states under depolarizing noise. In every local dimension $d\ge 2$, one shared maximally entangled qubit pair suffices: local controlled-SWAP operations exactly reproduce the globally optimal successful transformation. Conversely, any finite-dimensional preshared resource state that attains the same benchmark, even under a positive-partial-transpose relaxation, must have entanglement of formation at least one ebit. For pure resources with one ebit, or for two-qubit resources including mixed states, attaining the benchmark is possible only for states with exactly two nonzero Schmidt weights, both equal to $1/2$, namely those locally unitarily equivalent to a maximally entangled qubit pair. These findings provide a benchmark for evaluating the entanglement demands of noise management in quantum networks and modular quantum computers.
Problem
The paper asks how much preshared entanglement spatially separated parties need, under LOCC, to match the globally optimal probabilistic two-copy purification of bipartite pure states under depolarizing noise.
Approach
An LOCC algorithm assisted by one EPR pair uses local controlled-SWAP operations, Hadamard gates and measurements to reproduce the optimal global CPTN fidelity gain. Lower bounds are proved under a PPT relaxation, and one-ebit pure and two-qubit resources are characterized. The pure-resource lower bound (E(η) ≥ 1) is formally verified in Lean 4 using Mathlib and the Lean-QIT library.
Results
One EPR pair suffices in every local dimension d ≥ 2. Any finite-dimensional resource attaining the benchmark has entanglement of formation at least one ebit. Among pure one-ebit or two-qubit resources, only states locally unitarily equivalent to an EPR pair attain the benchmark.