slug: girard-2017-binegativity-upper-bound bibkey: girard2017binegativity doi: 10.48550/arXiv.1701.02724 url: https://arxiv.org/abs/1701.02724v3 triage: theorem motivation_gids:

• D5/S3/Quantum/Entanglement/TwoQubitBinegativityUpperBoundRefutation.result

The upper binegativity bound for two qubits

Problem

M. W. Girard, G. Gour, The binegativity of two qubits, arXiv:1701.02724v3 (2017), Eq. (9):

In general, based on numerical evidence from randomly generated states, we conjecture that the the binegativity of two-qubit states is bounded by $\nu\frac{(c+\nu)(\nu+1)}{(c+\nu)^2+2c(1-c)}\leq N_2(\sigma)\leq \frac{\nu}{2}\frac{(c+\nu)^2}{c^2+\nu^2}$forallstates$\sigma$ with fixed negativity $N(\sigma )=\nu$ and concurrence $C(\sigma )=c$.

Here $N(\sigma )=2\mathrm{Tr}[({\sigma }^{\Gamma }{)}_{-}]$ and $N_2(\sigma)=\operatorname{Tr}[(\sigma^\Gamma)-]+2\operatorname{Tr}[ (((\sigma^\Gamma)-)^\Gamma)-]$,with$X\pm$ the positive and negative components of a self-adjoint $X$ and $C$ the two-qubit concurrence. The target is the upper inequality; it is a preprint conjecture (no journal version is listed).

Motivation

The binegativity is computable from the spectral decomposition of the partial transpose, vanishes exactly on separable two-qubit states, and is conjectured by the authors to be an entanglement monotone. Eq. (9) would describe the region of possible values of $(C,N,N_2)$, and the paper uses it to argue that the binegativity orders entangled states differently from the concurrence and the negativity. The frozen declaration D5/S3/Quantum/Entanglement/TwoQubitBinegativityUpperBoundRefutation.result shows that the upper surface of that region is not an upper bound.

Gap

Issue #12432 classifies the conjecture as Tier 1 and records the checks made before any Lean:

• arXiv:1701.02724 v3 is the latest version and states the conjecture; INSPIRE lists one citation;
• Sazim–Awasthi, arXiv:1711.03717v2 (Phys. Lett. A 382 (2018) 1852), give $N_2=\frac{N}{2}(1+N({\rho }_{\psi }))$ with ${\rho }_{\psi }$ the normalized negative eigenvector of ${\rho }^{\Gamma }$ and study state families and noise channels, not the fixed-$(C,N)$ bound;
• concurrence–negativity relations (Verstraete et al., quant-ph/0108021; Miranowicz–Grudka, quant-ph/0404053) constrain $(C,N)$ only, and the operator positivity $|{\rho }^{\Gamma }{|}^{\Gamma }\ge 0$ (Ishizaka, quant-ph/0308056) is a different statement.

These are seat-reported and orchestrator-reported readings, not-found-in-searched-scope; they do not establish exhaustive worldwide novelty.

Route

1. $\rho =\frac{1}{26}(v{v}^T+9|00⟩⟨00|)$ with $v=(3,2,2,0)$ in the basis $00,01,10,11$.
2. With $w=(-1,1,1,2)$, ${\rho }^{\Gamma }=({\rho }^{\Gamma }+w{w}^T/91)-w{w}^T/91$; the first part is $\frac{64}{91}{l}_1{l}_1^T+\frac{5}{52}{l}_2{l}_2^T+\frac{4}{65}{l}_3{l}_3^T$ for rational $l_1,l_2,l_3$ and annihilates $w$, so the uniqueness of the positive and negative parts gives $({\rho }^{\Gamma }{)}_{-}=w{w}^T/91$, of trace $1/13$.
3. With $z=(2,3,3,-2)$, the same argument gives $((w{w}^T/91{)}^{\Gamma }{)}_{-}=3z{z}^T/2366$, of trace $3/91$. Hence $N=2/13$ and $N_2=1/7$.
4. In any pure-state decomposition the zero entry ${\rho }_{11,11}$ forces ${\psi }_i(11)=0$ for every ${\psi }_i$ of positive weight, and the triangle inequality gives ${\sum }_i{p}_{i}C({\psi }_i)\ge 2|{\rho }_{01,10}|=4/13$; the decomposition with weights $9/13,1/26,7/26$ and vectors $(-7,-4,-4,0)/9$, $(1,-2,-2,0)/3$, $(1,0,0,0)$ shows the infimum is over a nonempty set. So $C\ge 4/13$.
5. For $\nu =2/13$ and $c\ge 4/13$, $9(c^2+{\nu }^2)-5(c+\nu {)}^2=2(2c-\nu )(c-2\nu )\ge 0$, so the bound is at most $9/65<1/7$.

Falsifier

The kernel-checked result is the negation of the statement that every two-qubit density matrix $\sigma$ (IsDensity, positive semidefinite with trace one) with positive negativity satisfies $N_2(\sigma )\le \frac{N}{2}\frac{(C+N{)}^2}{C^2+N^2}$. The negativity is the paper’s $N(\sigma )=2\mathrm{Tr}[({\sigma }^{\Gamma }{)}_{-}]$, written out in the claim with the frozen partialTransposeB (partial transposition on the second qubit) and Mathlib’s negative part, which the binegativity also uses; the concurrence is the infimum over finite decompositions into unit vectors with nonnegative weights. The refutation uses only a lower bound on the concurrence, since the bound decreases in $c$ for $c>\nu$.

Evidence

Exact recomputation (SymPy, issue #12432): $13{\rho }^{\Gamma }$ has eigenvalues $2,-1,6\pm 2\sqrt{7}$; Wootters’ formula gives $C(\rho )=4/13$ (so the convex-roof bound is attained); $N=2/13$, $N_2=1/7$; the upper bound is $9/65$ (gap $2/455$) and the lower bound $5/39$ holds. A second independent recomputation by the literature seat (characteristic polynomials, Gram certificates, the spin-flip product) agrees.

The canonical source is D5/S3/Quantum/Entanglement/TwoQubitBinegativityUpperBoundRefutation.lean. Its public declarations are binegativity, pureConcurrence, concurrence, claim, vec4, witness and result, on the two-qubit matrices Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ; the partial transposition and IsDensity are frozen in D5/S3/Quantum/Entanglement/StructuredNegativityCoincidenceRefutation. The frozen module state has statement identity sha256:07b1c3c99e9d5590b1af730376d46694569510a56e1abb12cc7af8529dfb1030. The result declaration has statement identity sha256:797223f7896ecb504da3573b596cab0819aedc8da21c22c10e588861af289ec0. The Freeze event is sha256:a6519b47341a84496f313b7d83b6ad8f81e15a670ca7eac60a6e1b067a9a10c7; its project-level frozen prerequisite is the Freeze event of D5/S3/Quantum/Entanglement/StructuredNegativityCoincidenceRefutation. The proof uses only the standard axioms propext, Classical.choice and Quot.sound; no sorry, native_decide, or new axiom.

Triage

Tier 1 preprint conjecture; resolution Refuted by D5/S3/Quantum/Entanglement/TwoQubitBinegativityUpperBoundRefutation.result. proof_shape: bind-only (the settlement of the named conjecture is the new content; no escape witness); admission_basis: open-problem-resolution (issue #12432). Utility kind certified-instance, basis refutes the module’s claim.

What the settlement shows

• Proved by result: the upper inequality of Eq. (9) fails for a rank-two two-qubit state, with $N_2=1/7$ against a bound of at most $9/65$.
• Proved inside the proof of result, for the state $\rho$ only: the negative parts $({\rho }^{\Gamma }{)}_{-}=w{w}^T/91$ and $(({\rho }^{\Gamma }{)}_{-}^{\Gamma }{)}_{-}=3z{z}^T/2366$, which give $N(\rho )=2/13$; and the convex-roof bound $C(\rho )\ge 2|{\rho }_{01,10}|=4/13$ from ${\rho }_{11,11}=0$.
• Follows from the same steps (not stated in Lean): $C(\sigma )\ge 2|{\sigma }_{01,10}|$ for every two-qubit state with ${\sigma }_{11,11}=0$.
• Mechanism (computed, not stated in Lean): by the Sazim–Awasthi identity $N_2=\frac{N}{2}(1+N({\rho }_{\psi }))$, the upper bound of Eq. (9) is equivalent to $N({\rho }_{\psi })\le 2CN/(C^2+N^2)$ for the negative eigenvector $\psi$ of ${\rho }^{\Gamma }$. Here $\psi =w/\sqrt{7}$ has $N({\rho }_{\psi })=6/7$, while $2CN/(C^2+N^2)=4/5$: the negative eigenvector is more entangled than the surface allows. The paper’s family $\sigma (p,q,r)$ of Appendix B, at the same $(c,\nu )$, ranges exactly over $[5/39,9/65]$ (endpoints $p=7/13$ and $p=3/13$), so the state lies outside the family that motivated the bound.
• Checked by reading (orchestrator, issue #12432): Appendix B, Eq. (appconc1) (l. 533–535), prints the lower bound with the prefactor $\nu /2$ instead of the $\nu$ of Eq. (9); the family’s endpoint $5/39$ matches Eq. (9).
• Follows from it (not stated in Lean): by continuity of $N$, $N_2$ and $C$, full-rank states near $\rho$ (for instance $(1-\varepsilon)\rho+ \varepsilon I/4$forsmall$\varepsilon$) also violate the bound.
• Open here: the true largest binegativity at fixed $(C,N)$; whether the lower inequality of Eq. (9) holds for all states; and the conjecture that the binegativity is an entanglement monotone under LOCC or PPT channels.

ASSUMED-UNVERIFIED

The literature checks do not establish worldwide priority, and a complete forward-citation graph was not obtained; the Sazim–Awasthi and other readings are seat-reported. The Lean kernel verifies the encoded statement and its axiom closure; its correspondence to the paper, including the convex-roof reading of the concurrence and the use of the second-qubit partial transposition, is checked by reading the source and the definitions.