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

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

  • Postselection on 0^a has already succeeded
  • The |i> form an orthonormal computational basis of the output register
  • P_i are PSD effects summing to the identity
  • sqrt(P_i) is the unique PSD square root
  • Mixed-state results are obtained by convex-linear extension of the pure-state map

Question

Continue the POVM-by-block-encoding construction of Lemma 9.15: after applying W = sum_i |i><i| tensor U_i to |u> |0^a> |psi> and successfully postselecting the block-encoding ancilla on 0^a, the (renormalized) joint state of the output register and the system register is proportional to sum_i |i> tensor sqrt(P_i)|psi>. Prove that this joint state is correctly normalized, that measuring the output register in the computational basis yields outcome i with conditional probability P(i | succ) = <psi| P_i |psi>, and that the resulting post-measurement system state is sqrt(P_i)|psi> / sqrt(<psi|P_i|psi>). Then explain how the mixed-state update rule rho -> sqrt(P_i) rho sqrt(P_i) / Tr(P_i rho) follows from the pure-state result, and why the overall outcome probability for i (not conditioned on success) is still proportional to <psi|P_i|psi>.

Hint: mathematical route

After postselection the POVM circuit yields outcome i with probability <psi|P_i|psi> and the correct sqrt(P_i)-update, with the mixed-state rule following by linearity.

  1. Orthonormality + completeness give ||sum_i |i> sqrt(P_i)|psi>||^2 = sum_i <psi|P_i|psi> = 1, so the joint state is normalized.
  2. The weight on label |i> is ||sqrt(P_i)|psi>||^2 = <psi|P_i|psi>, so P(i|succ) = <psi|P_i|psi>.
  3. Collapsing on i leaves the normalized system vector sqrt(P_i)|psi>/sqrt(<psi|P_i|psi>).
  4. The map |psi><psi| -> sqrt(P_i)|psi><psi|sqrt(P_i) is linear, so convex mixing yields rho -> sqrt(P_i) rho sqrt(P_i)/Tr(P_i rho).
  5. Chaining with P(succ) gives unconditional P(i) = (1/(beta^2 2^m)) <psi|P_i|psi>, proportional to the target statistic.
Reference solution

Normalization: the squared norm of sum_i |i> sqrt(P_i)|psi> is, using orthonormality of the |i>, sum_i ||sqrt(P_i)|psi>||^2 = sum_i <psi|P_i|psi> = <psi|(sum_i P_i)|psi> = <psi|psi> = 1 by completeness. So after postselection the normalized joint state is exactly |Phi> = sum_i |i> tensor sqrt(P_i)|psi>. Measuring the output register in the computational basis: the probability of reading label i is the squared norm of the component attached to |i>, namely ||sqrt(P_i)|psi>||^2 = <psi| sqrt(P_i)^dagger sqrt(P_i) |psi> = <psi|P_i|psi> (PSD square root), so P(i|succ) = <psi|P_i|psi>. Conditioned on reading i, the system register collapses to the normalized vector sqrt(P_i)|psi> / || sqrt(P_i)|psi> || = sqrt(P_i)|psi> / sqrt(<psi|P_i|psi>), which is exactly the pure-state version of the generalized-measurement update. Mixed states: for rho = sum_k q_k |psi_k><psi_k|, run the same circuit on each pure branch; the map |psi><psi| -> sqrt(P_i)|psi><psi|sqrt(P_i) is linear in the input operator, and summing with weights q_k and renormalizing by the total weight Tr(P_i rho) gives rho -> sqrt(P_i) rho sqrt(P_i) / Tr(P_i rho). Linearity is what lets the pure-state formula be lifted verbatim to density operators. Unconditional probability: P(outcome i) = P(succ) * P(i|succ) = (1/(beta^2 2^m)) <psi|P_i|psi>, i.e. proportional to <psi|P_i|psi> with the i-independent proportionality constant 1/(beta^2 2^m); amplitude amplification later removes the constant penalty but never changes the relative weights, so the correct POVM statistics Tr(P_i rho) are reproduced.

Assessment rubric
  1. Proves normalization of sum_i |i> sqrt(P_i)|psi> via orthonormality + completeness sum_i P_i = I (1 weight)
  2. Derives P(i|succ) = <psi|P_i|psi> as the squared norm of the |i> component, using the PSD square-root identity (1 weight)
  3. Identifies the collapsed system state sqrt(P_i)|psi>/sqrt(<psi|P_i|psi>) and lifts it to the mixed-state rule by linearity in rho (1 weight)
  4. Explains the unconditional probability is (1/(beta^2 2^m)) <psi|P_i|psi>, i.e. proportional to <psi|P_i|psi> with an outcome-independent constant (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: 6af74a97d08adabaec805770e176dfefb6527c99f8543c5f6d27e02725ac3c8a

Item digest: 4d0389f52f14f202bd366a400d21ee868cd70f95d739c66384d54c616d48666f

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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