QuantumComputinglib learn · inspect · formalize
Checked on this commit 4,524 public declarations commit 4e2c5b2c0be5 Build record

Quantum Information / Quantum Information Apps

Quantum Information Apps

Exercise PLAN-409

advanced · proof · test_public

primary source nl only. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.

Assumptions and conventions

      Question

      Let |psi>_AB be an arbitrary pure bipartite state. Prove that any state rho_{A B B'} with tr_{B'} rho_{A B B'} = psi_AB (the projector |psi><psi|_AB) must have the product form rho_{A B B'} = psi_AB tensor omega_{B'} for some state omega_{B'}. Use a purification of rho_{A B B'} and a Schmidt decomposition across the bipartition (AB : B'C). Conclude, as a corollary, that a pure entangled state is not 2-extendible.

      Hint: mathematical route

      A purification Schmidt-decomposed across (AB : B'C) whose AB-marginal is the rank-one psi_AB must collapse to a single term, forcing rho_{A B B'} = psi_AB tensor omega_{B'} and ruling out 2-extensions of pure entangled states.

      1. A purification Schmidt-decomposed across (AB : B'C) has AB-marginal sum_j q_j |u_j><u_j|.
      2. Equaling a rank-one projector forces a single Schmidt term with |u_1> = |psi>.
      3. Hence rho_{A B B'} = psi_AB tensor omega_{B'}, so pure entangled states have no 2-extension.
      Reference solution

      Let |chi>_{A B B' C} be a purification of rho_{A B B'}, with C a purifying system. Consider the bipartition (AB) versus (B' C) and write the Schmidt decomposition |chi> = sum_j sqrt(q_j) |u_j>_{AB} |w_j>_{B'C} with q_j > 0, {|u_j>} orthonormal in AB and {|w_j>} orthonormal in B'C. Tracing out B' and C gives the AB-marginal tr_{B'C} |chi><chi| = sum_j q_j |u_j><u_j|_{AB}. By hypothesis this marginal equals psi_AB = |psi><psi|_{AB}, a rank-one projector. A convex combination sum_j q_j |u_j><u_j| of mutually orthonormal rank-one projectors with q_j > 0 is rank one only if there is a single term; hence the Schmidt rank across (AB : B'C) is 1, q_1 = 1, and |u_1>_{AB} = |psi>_{AB} up to a phase. The Schmidt decomposition collapses to |chi> = |psi>_{AB} tensor |w>_{B'C} for a single |w>_{B'C}. Therefore rho_{A B B'} = tr_C |chi><chi| = |psi><psi|_{AB} tensor tr_C |w><w|_{B'C} = psi_AB tensor omega_{B'}, where omega_{B'} = tr_C |w><w| is a valid state. This is the claimed product form. Corollary: if |psi>_AB is entangled, a 2-extension rho_{A B B'} (with tr_{B'} rho = psi_AB and tr_B rho = psi_{A B'} = psi_AB as a state on A and a B-copy) would, by the above, be forced to equal psi_AB tensor omega_{B'}; but then its A B'-marginal is psi_A tensor omega_{B'}, which is uncorrelated across A : B' and therefore cannot equal the correlated psi_AB. The contradiction shows a pure entangled state has no 2-extension.

      Assessment rubric
      1. Introduces a purification |chi>_{A B B' C} and Schmidt-decomposes across (AB : B'C) (1 weight)
      2. Computes the AB-marginal as sum_j q_j |u_j><u_j| and equates it to the rank-one projector psi_AB (1 weight)
      3. Argues a mixture of orthonormal projectors is rank one only if a single Schmidt term survives, forcing |chi> = |psi>_{AB} |w>_{B'C} (1 weight)
      4. Concludes rho_{A B B'} = psi_AB tensor omega_{B'} and derives that a pure entangled state is not 2-extendible (1 weight)

      Graph-grounded prerequisites

      These are support/source anchors, not an automatically extracted theorem-dependency proof.

      • Operator and semigroup theory (frozen curriculum anchor; see graph registry)
      • Matrix analysis (frozen curriculum anchor; see graph registry)
      • Tensor networks (frozen curriculum anchor; see graph registry)

      Download the shared core registry

      Lean view and evidence boundary

      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

      Sources and provenance

      Contract: 45c329d4644e1bf87c1ecdcf179000fc25fd6ab75c7b29cfb131b49d61bdfde4

      Item digest: a64a1d8b27cf0fe3a7a66f8b4bf60d7ebf0a288ef911b5e8cdcc2fdaac26500a

      Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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