Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help


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

  1. on two qutrits, with $R=|v\rangle\langle v|+4(|02\rangle \langle02|+|20\rangle\langle20|+|12\rangle\langle12|+|21\rangle\langle21|)$ and .
  2. with , , and an explicit sum of positive rank-one and diagonal terms; and , so and .
  3. The signed permutation matrices (diagonal signs, and the swaps of and of ) are unitary, so ; with , $\mathrm{Re},\mathrm{Tr}(FX)\le |X|_1$.
  4. , 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$.
  5. 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.