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

Quantum Information / Quantum Information

Quantum Information

Exercise PLAN-005

intermediate · counterexample · 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

      Call a bipartite state a product state if it factorizes as a single tensor product of local states, and separable if it is a probabilistic mixture of product states. (a) Show that in a product state the outcomes of any two local measurements are statistically independent (the joint expectation factorizes). (b) Exhibit a concrete separable two-qubit state that is NOT a product state and compute a pair of local measurements whose outcomes are correlated, demonstrating that separable states can carry classical correlation even though each term in the mixture is uncorrelated. (c) Reconcile this with the textbook remark that a PURE separable state is automatically a product state - i.e. explain why your correlated example must be mixed.

      Hint: mathematical route

      Product states give independent local outcomes, but separable mixtures can be classically correlated; purity forces a separable state to be a single uncorrelated product, so correlated separable states are necessarily mixed.

      1. In a product state the joint expectation factorizes: tr[(omega tensor sigma)(E tensor F)] = tr(omega E) tr(sigma F).
      2. The equal mixture of |00><00| and |11><11| is separable, not a product (rank 2 vs full-rank marginal product), and perfectly correlated.
      3. A pure separable state is extreme, hence a single product term and uncorrelated, so correlated separable states are mixed.
      Reference solution

      (a) For a product state omega tensor sigma and local measurement effects E on the first system and F on the second, the joint probability is tr[(omega tensor sigma)(E tensor F)] = tr(omega E) tr(sigma F), the product of the two marginal probabilities. Hence the two outcomes are independent and uncorrelated. (b) Take the classically correlated state rho = (1/2)(|0><0| tensor |0><0|) + (1/2)(|1><1| tensor |1><1|). It is separable (an equal mixture of the two product states |00><00| and |11><11|) but it is not a single product omega tensor sigma: its marginals are both the maximally mixed (1/2)I, whose product (1/4)I is full rank, while rho has rank 2, so rho != marginal tensor marginal. Measuring the first qubit in the computational basis (outcome a in {0,1}) and the second likewise (outcome b) gives joint probabilities Pr(0,0)=Pr(1,1)=1/2, Pr(0,1)=Pr(1,0)=0. The outcomes are perfectly correlated (a = b always) even though Pr(a=0)=Pr(b=0)=1/2, so Pr(a,b) != Pr(a)Pr(b); the correlation is exactly the shared classical index of the mixture. (c) A pure separable state is by definition an extreme point that is also a mixture of products; being extreme, the mixture must be trivial, so it equals one product term omega tensor sigma, and by part (a) it is uncorrelated. Therefore any separable state exhibiting correlation must be a nontrivial mixture, i.e. mixed - consistent with the example, whose rank is 2 and which is a genuine average over two distinct product states.

      Assessment rubric
      1. Proves factorization tr[(omega tensor sigma)(E tensor F)] = tr(omega E) tr(sigma F) and concludes local independence in a product state (1 weight)
      2. Gives an explicit separable non-product state (e.g. equal mixture of |00><00| and |11><11|) and argues it is not a single product via a marginal/rank comparison (1 weight)
      3. Computes local measurements with correlated outcomes (Pr(0,0)=Pr(1,1)=1/2) showing Pr(a,b) != Pr(a)Pr(b) (1 weight)
      4. Explains that a pure separable state is extreme hence a single product (uncorrelated), so a correlated separable state must be mixed (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)
      • Probability and sampling (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: b57ccb106115ecf08f7441c3c5ce83b7e9044addf5be5c1e5f5a06b808454dd6

      Item digest: 75bdc7610d7bf3c2c4c4a2fb21a151bdd2966bb54443b4426e310f9b67f38bf5

      Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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