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-201

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

  • Each U_i is a (beta,a)-block-encoding of sqrt(P_i) with common a and common beta
  • The output register is prepared in the exact uniform superposition over 2^m labels
  • |psi> is a normalized pure system state
  • sqrt(P_i) denotes the unique positive semidefinite square root of the PSD effect P_i
  • Postselection on 0^a means projecting the ancilla onto |0^a> and renormalizing

Question

A POVM P = {P_i : i in [2^m]} is implemented through block encodings as follows. For each outcome i we are given a unitary U_i that is a (beta, a)-block-encoding of sqrt(P_i), all sharing the SAME ancilla size a and the SAME subnormalization factor beta > 0, so that U_i |0^a> |psi> = (1/beta) |0^a> sqrt(P_i) |psi> + |perp_i>, where (<0^a| tensor I)|perp_i> = 0. Define the controlled unitary W = sum_i |i><i| tensor U_i acting on an output register in the uniform superposition |u> = (1/sqrt(2^m)) sum_i |i>, an ancilla register |0^a>, and the system register |psi>. After applying W one measures the ancilla register and postselects on the outcome 0^a. Starting from |u> |0^a> |psi>, derive in full the probability P(succ) of obtaining 0^a on the ancilla, show that it equals exactly 1/(beta^2 2^m) independent of the input state |psi>, and identify precisely where the POVM completeness relation sum_i P_i = I and the mutual orthogonality of the output-register basis states are used.

Hint: mathematical route

Implementing a POVM through shared-beta block encodings of sqrt(P_i) gives postselection success probability exactly 1/(beta^2 2^m), with completeness collapsing the state-dependent sum.

  1. W acts block-diagonally, so W|u>|0^a>|psi> = (1/sqrt(2^m)) sum_i |i> U_i|0^a>|psi>.
  2. Substituting the block-encoding action gives a clean branch (1/(beta sqrt(2^m))) sum_i |i>|0^a> sqrt(P_i)|psi> plus |perp> with zero 0^a-overlap.
  3. Postselection on 0^a annihilates |perp> because each (<0^a| tensor I)|perp_i> = 0.
  4. Orthonormality of the |i> makes the squared norm a sum of per-outcome squared norms, with no cross terms.
  5. sum_i ||sqrt(P_i)|psi>||^2 = sum_i <psi|P_i|psi> using sqrt(P_i)^dagger sqrt(P_i)=P_i for PSD P_i.
  6. Completeness sum_i P_i = I collapses the sum to <psi|psi> = 1, giving P(succ)=1/(beta^2 2^m) independent of |psi>.
Reference solution

Apply W to the uniform-superposition input. Because W is block-diagonal in the output register, W |u> |0^a> |psi> = (1/sqrt(2^m)) sum_i |i> (U_i |0^a> |psi>) = (1/(beta sqrt(2^m))) sum_i |i> |0^a> sqrt(P_i)|psi> + |perp>, where |perp> = (1/sqrt(2^m)) sum_i |i> |perp_i> satisfies (I tensor <0^a| tensor I)|perp> = 0 because each (<0^a| tensor I)|perp_i> = 0. Postselecting the ancilla on 0^a projects out |perp> entirely, since |perp> has zero overlap with the subspace spanned by |0^a> on the ancilla. The unnormalized postselected vector is therefore (1/(beta sqrt(2^m))) sum_i |i> |0^a> sqrt(P_i)|psi>. Its squared norm is the success probability. The output-register states |i> are mutually orthonormal, so the cross terms vanish and the norm squared factorizes outcome by outcome: P(succ) = (1/(beta^2 2^m)) sum_i || sqrt(P_i)|psi> ||^2 = (1/(beta^2 2^m)) sum_i <psi| sqrt(P_i)^dagger sqrt(P_i) |psi> = (1/(beta^2 2^m)) sum_i <psi| P_i |psi>. Here we used sqrt(P_i)^dagger sqrt(P_i) = P_i because each P_i is positive semidefinite and sqrt(P_i) is its unique PSD square root. Finally, by POVM completeness sum_i P_i = I, so sum_i <psi| P_i |psi> = <psi| I |psi> = 1 for any normalized |psi>. Hence P(succ) = 1/(beta^2 2^m), which is manifestly independent of |psi>. Completeness is what collapses the state-dependent sum to the constant 1; the orthogonality of the |i> is what prevents interference between different outcomes so the sum of norms (not a norm of a sum) appears.

Assessment rubric
  1. Applies W to |u>|0^a>|psi>, obtains the branch (1/(beta sqrt(2^m))) sum_i |i>|0^a> sqrt(P_i)|psi> plus an orthogonal remainder annihilated by <0^a| (1 weight)
  2. Shows postselection on 0^a removes the perpendicular part and computes P(succ) as the squared norm of the surviving vector (1 weight)
  3. Uses orthonormality of the |i> to get sum_i ||sqrt(P_i)|psi>||^2 = sum_i <psi|P_i|psi> (PSD square root), and completeness sum_i P_i = I to reduce it to 1 (1 weight)
  4. Concludes P(succ) = 1/(beta^2 2^m) and states it is independent of |psi>, correctly attributing the two uses (completeness -> constant; orthogonality -> no interference) (1 weight)

Graph-grounded prerequisites

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

  • Block Encoding (frozen curriculum anchor; see graph registry)
  • Probability and sampling (frozen curriculum anchor; see graph registry)
  • Operator and semigroup theory (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: db7927ae752445a09cc86d847d8ebff42c41736377498fbb92ed55888f67117e

Item digest: 5432c2b2b9dea37c3425626c4e2f81de0bc5efe924d1f09178943b56ade40d74

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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