Exercise PLAN-007

The two-qubit Werner state is entangled exactly for negative swap overlap. Its partial transpose has eigenvalue x/2, while the separable converse follows by twirling an explicit product state with overlap x and identifying the unique Werner state, not by reversing swap-overlap positivity.

1. Partial transpose gives rho(x)^{T_B}=((2-x)/6)I+((2x-1)/3)P_+, using F^{T_B}=2P_+.
2. The Bell-basis partial-transpose eigenvalues are x/2 and three copies of (2-x)/6; negative x therefore proves entanglement by the necessary partial-transpose test.
3. For every x in [0,1], the product of |0> and sqrt(x)|0>+sqrt(1-x)|1> has swap overlap x; its U tensor U twirl preserves that overlap, is the unique Werner rho(x), and stays in the closed convex separable set. This proves the separable converse, whereas overlap positivity alone proves only separable implies x>=0.

The exact threshold is x=0: rho(x) is entangled for -1<=x<0 and separable for 0<=x<=1. Write a=(2-x)/6 and b=(2x-1)/6. Since swap F has eigenvalue +1 on the three-dimensional symmetric subspace and -1 on the antisymmetric line, rho itself has eigenvalues a+b=(1+x)/6 with multiplicity three and a-b=(1-x)/2 with multiplicity one; these are nonnegative on the stipulated interval and sum to one.

For the entangled direction, F^{T_B}=2P_+ and I^{T_B}=I give rho(x)^{T_B}=a I+2b P_+. In the Bell basis its eigenvalue on P_+ is a+2b=(2-x)/6+(2x-1)/3=x/2, while each of the three orthogonal Bell states has eigenvalue a=(2-x)/6. Thus x<0 produces a negative partial-transpose eigenvalue, so rho(x) is entangled: partial transpose of every product positive operator is positive, and convex mixtures preserve positivity. For x>=0 this calculation shows only PPT, not separability; no PPT-sufficiency theorem is used.

The swap identity tr[F(omega tensor sigma)]=tr(omega sigma)>=0 extends to mixtures and proves separable implies nonnegative swap overlap. It does not prove the converse for arbitrary bipartite states; Werner symmetry must be used to establish the required converse.

For each x in [0,1], choose |a>=|0> and |b>=sqrt(x)|0>+sqrt(1-x)|1>, and twirl the product projector tau=|a><a| tensor |b><b| by normalized Haar averaging of (U tensor U)tau(U tensor U)^dagger: the average is Werner by Haar invariance, preserves swap overlap |<a|b>|^2=x because F commutes with U tensor U, and hence equals the specified rho(x), which is the unique two-qubit Werner state with that overlap. Each integrand is a product state and finite convex approximations converge to the average; the finite-dimensional separable set is closed (the convex hull of the compact set of pure product projectors is compact), so this proves separability including x=0 and x=1 without the low-dimensional PPT shortcut, and the product-twirl argument, unlike these particular qubit coefficients and eigenvalue multiplicities, extends to local dimension at least two.

1. States the exact restricted-family threshold: entangled for -1<=x<0 and separable for 0<=x<=1, including the x=0 boundary. (1 weight)
2. Computes rho^{T_B}=((2-x)/6)I+((2x-1)/3)P_+, with Bell eigenvalues x/2 once and (2-x)/6 three times; does not confuse this spectrum with rho's original spectrum. (1 weight)
3. Uses the negative eigenvalue for x<0 and necessary positivity of partial transpose for separable states to prove entanglement. Does not infer separability merely from nonnegative partial-transpose eigenvalues. (1 weight)
4. For x>=0 supplies a product state with squared local overlap x and twirls it; establishes preserved swap overlap and Werner invariance/uniqueness, and uses convexity plus closedness of finite-dimensional separable states to conclude the twirl equals rho(x) and is separable. Swap-overlap positivity extended to mixtures alone proves only the opposite implication and is not a valid converse proof; no PPT-sufficiency shortcut is accepted. (1 weight)

No aligned Lean view has been admitted for this native core in this textbook checkpoint. This is not a claim that the underlying mathematics lacks a formal proof. Contributions must preserve this exact target contract and split.

Read the Lean track and existing diagnostic warmups

• website/research/sources.json

  leditzky-2025-repth-qit

  Source SHA-256: 9f85f45f20ed5a46931ad0dec3b94ee09748bc56e39fae29b0aefe910440b0ae · MIT metadata only
• Primary source

Contract: d2196fd968d517f6f9d4f870dab30d7bd70e0344eddb4b3ad19e6ff0464a6874

Item digest: 07e6df25bb07479718e7bef8a988827de01d56b685ab5fb591320d335c56ad67

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

Authored support steps: 3. This is not measured graph distance or model difficulty.

{ "predecessor_item_digest": "e04084fe7f2ef7232f2d953cffe7f86e11665744ae6669b27b5f0ff5fa232312", "predecessor_key": "qcb-core-plan-007-werner-entanglement-threshold", "repair_record": "shared/repairs/plan-007-werner-converse-repair.json", "repair_record_digest": "f6638980d6a9548f92155a420a8362adb0e3b5f9a6e3e6f7840e36dd3c167999", "review_record": "reports/textbook-v1/repairs/plan-007-werner-converse-repair-migration-revalidation-review.json", "review_digest": "efb45db65c7902d860705bec4851463e25f1c957716c59c835b3b56becf8eeb7" }