slug: ganardi-2022-negativity-ppt-distance bibkey: ganardi2022hierarchy doi: 10.22331/q-2022-02-16-654 url: https://arxiv.org/abs/2111.11887v2 triage: theorem motivation_gids:
- D5/S3/Quantum/Entanglement/NegativityPartialTransposeDistanceRefutation.result
Negativity and the partial transpose distance to the PPT states
Problem
R. Ganardi, M. Miller, T. Paterek, M. Żukowski, Hierarchy of correlation quantifiers comparable to negativity, Quantum 6, 654 (2022), arXiv:2111.11887v2, Conjecture 1:
Let be a density matrix. Then .
Here is the partial transpose distance, is the negativity, is the partial transpose on the second system, and PPT is the set of states with . The triangle inequality gives , so the conjecture asserts the reverse inequality.
Motivation
The conjecture would make the negativity a member of a family of
distance-based correlation measures built from one distance, so that
entanglement measured by negativity could be compared with discord and total
correlations measured by the same distance. The paper proves the equality
for states of positive binegativity (), which
include all pure states and all two-qubit states. The frozen declaration
D5/S3/Quantum/Entanglement/NegativityPartialTransposeDistanceRefutation.result
shows that the equality fails in general.
Gap
Issue #12452 classifies the conjecture as Tier 1 and records the checks made before any Lean:
- arXiv:2111.11887 v2 is the latest version and states the conjecture; the authors report random states of two qudits for each without a counterexample, and R. Ganardi’s thesis (Gdańsk 2022) calls the general case open;
- Zaw, arXiv:2403.16441v2 (Phys. Rev. Lett. 133, 050201 (2024)), keeps the equality as a conjecture; the other citing works listed by Quantum do not address it;
- a gap between the κ-entanglement and the logarithmic negativity does not refute the conjecture: the paper reports agreement for such states, and the Wang–Wilde state of arXiv:1809.09592v2 satisfies the equality;
- the counterexample state belongs to the punch-card family of Lami–Mele–Regula, arXiv:2405.09613v2 (Phys. Rev. Lett. 134, 090202 (2025)), Eq. (15), introduced there for the additivity of the κ-entanglement, a different question.
These are seat-reported and orchestrator-reported readings,
not-found-in-searched-scope; they do not establish exhaustive worldwide
novelty.
Route
- on two qutrits, with $R=|v\rangle\langle v|+4(|02\rangle \langle02|+|20\rangle\langle20|+|12\rangle\langle12|+|21\rangle\langle21|)$ and .
- with , , and an explicit sum of positive rank-one and diagonal terms; and , so and .
- The signed permutation matrices (diagonal signs, and the swaps of and of ) are unitary, so ; with , $\mathrm{Re},\mathrm{Tr}(FX)\le |X|_1$.
- , and for every matrix , $\mathrm{Tr}(F\sigma^{T_B})=\frac13\mathrm{Tr},\sigma-\frac13\langle b| \sigma|b\rangle-\frac43\langle c|\sigma^{T_B}|c\rangle$ with ; for a PPT state both quadratic forms are nonnegative, so $\mathrm{Re},\mathrm{Tr}(F\sigma^{T_B})\le \frac13$.
- Hence for every PPT state , and the infimum, over a nonempty set, is at least .
Falsifier
The kernel-checked result is the negation of the statement that for every
and every density matrix on
(IsDensity, positive semidefinite with trace one), the infimum of
over the density matrices
with positive semidefinite equals
. The partial transpose is the frozen
partialTransposeB (on the second factor) and the trace norm is the frozen
FiniteTraceDistance.traceNorm, .
The equal-dimension statement is a special case of Conjecture 1, so its
failure refutes the conjecture.
Evidence
Exact recomputation (SymPy, issue #12452): has spectrum , so ; ; ; $F=\frac13I-(\frac13|b\rangle\langle b|)^{T_B}-\frac43|c\rangle \langle c|\mathrm{Tr}(U_k\rho^{T_B})=-\frac1{17},-\frac1{17}, \frac{15}{17}9\times9$ matrix. The literature seat recomputed all values independently.
The canonical source is
D5/S3/Quantum/Entanglement/NegativityPartialTransposeDistanceRefutation.lean.
Its public declarations are claim, witness and result; the partial
transposition and IsDensity are frozen in
D5/S3/Quantum/Entanglement/StructuredNegativityCoincidenceRefutation, and
the trace norm with its unitary characterization, triangle inequality and
value on positive matrices in D5/S3/Quantum/Foundation/FiniteTraceDistance.
The frozen module state has statement identity
sha256:31daa626b61549aff782cc922e91c9c221ed234b9ae3b8ae49abf57c324684cf. The
result declaration has statement identity
sha256:6e60470ff4128cd1ee4254cc12b96181b07ab9450ba2e609d807f31c574156cc. The
Freeze event is
sha256:91e2571bb81a148bd8d8e313a964edb4bb62a1c181700c24db1bf44497bdaaeb; its
project-level frozen prerequisites are the Freeze events of
D5/S3/Quantum/Entanglement/StructuredNegativityCoincidenceRefutation and
D5/S3/Quantum/Foundation/FiniteTraceDistance. The
proof uses only the standard axioms propext, Classical.choice and
Quot.sound; no sorry, native_decide, or new axiom.
Triage
Tier 1 conjecture of a 2022 journal article; resolution Refuted by
D5/S3/Quantum/Entanglement/NegativityPartialTransposeDistanceRefutation.result.
proof_shape: bind-only (the settlement of the named conjecture is the new
content; no escape witness); admission_basis: open-problem-resolution
(issue #12452). Utility kind certified-instance, basis refutes the
module’s claim.
What the settlement shows
- Proved by
result: Conjecture 1 fails for a rank-five two-qutrit state, whose negativity is at most while its partial transpose distance to every PPT state is at least . - Proved inside the proof of
result, for this state only: , and for every PPT state . - Computed, not stated in Lean (orchestrator, high-precision check of the literature seat’s certificates): the exact distance is , attained by an explicit PPT state supported on the same blocks and certified by a member of the same witness family, so the gap to is about .
- Mechanism (literature seat, 席位自报; not stated in Lean): by the paper’s alternative form (Appendix B), the equality holds iff some PPT state satisfies . In the family $R_t=|v_t\rangle\langle v_t|+t\sum_{ij\in{02,20,12,21}}|ij\rangle\langle ij|v_t=|00\rangle+|11\rangle+t|22\rangle$, the largest trace of a PPT is , which reaches exactly when ; the state here is . The orchestrator checked the endpoint , the unfiltered punch-card state of Lami–Mele–Regula: an explicit PPT state attains , so that state satisfies the equality and the failure comes from the local filtering.
- Follows from it (orchestrator check of the witness): the mixtures with are full-rank counterexamples, since gives and ; so the failure is not confined to rank-deficient states, and counterexamples form an open set.
- Effect on the paper’s other conclusions (checked by reading the v2
source):
- Refuted: the identification of the negativity with the PPT member of the distance-based family (l. 342–345, l. 554); only holds in general (the triangle-inequality bound of l. 246–249 applied to for PPT , l. 342), and the alternative form of Appendix B (l. 637–638) fails for this state: no PPT state lies below .
- Unaffected: the definition of and the ordering , which follow from (l. 347–361); the equality for states of positive binegativity (§2.2, l. 301–310), hence the pure-state results (l. 385–389) and the pure-state subadditivity (l. 439–470); and the non-decomposability bound (l. 477–520), which uses only .
- Needs another justification: the non-Markovianity witness (l. 541–545) chooses closest to in the PPT set and uses , which is Conjecture 1 and fails in general. The conclusion that an increase of under witnesses non-Markovianity still holds by a standard argument (not stated in Lean): the propagator of CP-divisible dynamics acts on only, so it commutes with and does not increase the trace norm of ; this is the monotonicity of the negativity under local operations (Vidal–Werner, Phys. Rev. A 65, 032314 (2002)). The analogous witness for uses only the contractivity of and is unaffected.
- Open here: the smallest local dimensions in which the equality fails (two qubits satisfy it by positive binegativity; qubit–qutrit systems were not examined); the largest possible gap between the PPT distance and the negativity; and the relation of the PPT distance to the exact PPT entanglement cost.
ASSUMED-UNVERIFIED
The literature checks do not establish worldwide priority, and a complete forward-citation graph was not obtained; the citing-work readings are seat-reported. The Lean kernel verifies the encoded statement and its axiom closure; its correspondence to the paper, including the restriction to equal local dimensions and the second-system partial transpose, is checked by reading the source and the definitions.