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

Quantum Scientific Computing / Scientific Algorithms

Scientific Algorithms

Exercise PLAN-205

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

  • |c| < 1 and both states normalized
  • <phi|psi> = c*, <psi|phi> = c
  • |psi_perp>, |phi_perp> are the unit complements from the text
  • Positivity of P_? is checked on span{|psi>,|phi>} since it acts as identity off that plane

Question

For the unambiguous-discrimination POVM with P_psi = (1/(1+|c|)) |phi_perp><phi_perp|, P_phi = (1/(1+|c|)) |psi_perp><psi_perp|, P_? = I - P_psi - P_phi, where c = <psi|phi>, |c| < 1, and |psi_perp>, |phi_perp> are defined as in the text, prove the three properties that make it a legitimate unambiguous POVM for state discrimination: (i) P_psi, P_phi, P_? are all positive semidefinite; (ii) P_psi + P_phi + P_? = I; (iii) the conclusive outcomes are unambiguous, i.e. <phi|P_psi|phi> = 0 and <psi|P_phi|psi> = 0. For (i) you must actually verify that P_? >= 0, not merely assert it, by diagonalizing I - P_psi - P_phi on the two-dimensional space span{|psi>,|phi>}.

Hint: mathematical route

The two-conclusive-one-inconclusive discrimination POVM is valid: P_? = I - P_psi - P_phi stays PSD because P_psi+P_phi has operator norm exactly 1.

  1. P_psi+P_phi+P_? = I holds by definition of P_?.
  2. <phi|phi_perp> = (c* - c*)/sqrt(1-|c|^2) = 0 and <psi|psi_perp> = 0, giving unambiguity <phi|P_psi|phi> = <psi|P_phi|psi> = 0.
  3. P_psi, P_phi are nonnegative scalings of rank-one projectors, hence PSD.
  4. In basis {|phi_perp>,|psi_perp>} with Gram overlap |c|, S = P_psi+P_phi has eigenvalues {1, (1-|c|)/(1+|c|)}.
  5. Thus ||S|| = 1 and I - S = P_? has eigenvalues 0 and 2|c|/(1+|c|), both >= 0 for |c|<1.
Reference solution

Property (ii) is immediate from the definition P_? := I - P_psi - P_phi, so P_psi + P_phi + P_? = I exactly, with no assumption on c. Property (iii): compute <phi|phi_perp>. Since |phi_perp> = (|psi> - c*|phi>)/sqrt(1-|c|^2), we get <phi|phi_perp> = (<phi|psi> - c*<phi|phi>)/sqrt(1-|c|^2) = (c* - c*)/sqrt(1-|c|^2) = 0 (using <phi|psi> = c* and <phi|phi>=1). Hence <phi|P_psi|phi> = (1/(1+|c|))|<phi|phi_perp>|^2 = 0. Symmetrically, <psi|psi_perp> = (<psi|phi> - c<psi|psi>)/sqrt(1-|c|^2) = (c - c)/sqrt(1-|c|^2) = 0, so <psi|P_phi|psi> = 0. The conclusive outcomes never fire on the wrong state. Property (i): P_psi, P_phi are nonnegative multiples of rank-one projectors |phi_perp><phi_perp|, |psi_perp><psi_perp|, hence PSD. For P_?, restrict to span{|psi>,|phi>} (off this plane I - P_psi - P_phi acts as the identity, which is PSD). Both |phi_perp> and |psi_perp> are unit vectors; a direct computation of their overlap gives |<phi_perp|psi_perp>| = |c|. In the (non-orthogonal) spanning pair {|phi_perp>, |psi_perp>}, the operator S := P_psi + P_phi = (1/(1+|c|))(|phi_perp><phi_perp| + |psi_perp><psi_perp|) is a scaled sum of two unit rank-one projectors with Gram overlap |c|; such a sum has eigenvalues (1 +/- |c|) times the scalar 1/(1+|c|), i.e. eigenvalues 1 and (1-|c|)/(1+|c|). Hence ||S|| = 1 (attained) and the smaller eigenvalue is (1-|c|)/(1+|c|) >= 0. Therefore P_? = I - S has eigenvalues 1 - 1 = 0 and 1 - (1-|c|)/(1+|c|) = 2|c|/(1+|c|), both >= 0 for |c| in [0,1). So P_? >= 0 (with a zero eigenvalue, showing the weight 1/(1+|c|) is the largest that keeps P_? PSD). All three properties hold, so the family is a valid unambiguous-discrimination POVM.

Assessment rubric
  1. States (ii) P_psi+P_phi+P_? = I holds by definition of P_? (1 weight)
  2. Proves (iii) by computing <phi|phi_perp> = 0 and <psi|psi_perp> = 0 explicitly, hence <phi|P_psi|phi> = <psi|P_phi|psi> = 0 (1 weight)
  3. Argues P_psi, P_phi >= 0 as nonnegative scalings of rank-one projectors (1 weight)
  4. Verifies P_? >= 0 by diagonalizing S = P_psi+P_phi on the 2D span, finding eigenvalues {1, (1-|c|)/(1+|c|)} so I - S has eigenvalues {0, 2|c|/(1+|c|)} >= 0 (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)
  • 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: 8d70086c8fec9c4218bd65b05d959f758514571d1b36b8def11eb6dd122066a1

Item digest: ac1b3b3d96f318f7409e0ff115c76d8ac4d471ea0f8b8acf2b79810e14205eb7

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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