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

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

      The optimal N -> M approximate cloner achieves worst-case fidelity F*(T) = d_N/d_M where d_L = dim Sym^L(H) = binom(d + L - 1, L) with d = dim H. It is stated that F*(T) >= 1 - Kd/N with K = M - N. (a) Prove the lower bound F*(T) >= 1 - Kd/N from the binomial ratio and conclude that for fixed K the optimal worst-case fidelity tends to 1 as N -> infinity. (b) The worst-case fidelity F(T) = inf_psi F(psi^{tensor M}, T(psi^{tensor N}))^2 and the Haar-average fidelity F_avg(T) satisfy a universal ordering for every map T; state and justify that ordering, and explain why nevertheless the same optimal map is simultaneously optimal for both criteria.

      Hint: mathematical route

      The optimal cloner's fidelity d_N/d_M exceeds 1 - Kd/N (tending to 1 for fixed K), and because it is input-independent its worst-case and Haar-average fidelities coincide, making it optimal for both.

      1. The symmetric-subspace dimension ratio satisfies d_N/d_M >= 1 - Kd/N.
      2. Fixed K gives asymptotically perfect cloning as N -> infinity.
      3. Worst-case fidelity never exceeds the average, with equality for the input-independent optimal map.
      Reference solution

      (a) With d_N = binom(d+N-1, N) and d_M = binom(d+M-1, M) and M = N + K, the ratio d_N/d_M after cancelling common factors is a quotient of two products of K consecutive integers: d_N/d_M = [(N+1)(N+2)...(N+K)] / [(N+d)(N+d+1)...(N+d+K-1)]. Each of the K factors has the form (N + j)/(N + d - 1 + j) = 1 - (d-1)/(N + d - 1 + j) >= 1 - (d-1)/N >= 1 - d/N. Multiplying K such factors and using the elementary inequality prod (1 - a_j) >= 1 - sum a_j for a_j in [0,1], we get d_N/d_M >= 1 - K(d-1)/N >= 1 - Kd/N. Hence F*(T) = d_N/d_M >= 1 - Kd/N. For fixed K and d, Kd/N -> 0 as N -> infinity, so F*(T) -> 1: cloning with a fixed number of extra copies becomes asymptotically perfect. (b) Universal ordering: F(T) <= F_avg(T) for every map T, because the infimum over pure inputs of a nonnegative quantity never exceeds its Haar average: inf_psi g(psi) <= integral g(psi) dpsi. So the worst-case criterion is the stronger (harder to maximize) one. Nevertheless the optimal symmetric cloner satisfies tr(phi^{tensor M} T(phi^{tensor N})) = d_N/d_M for EVERY pure input phi -- a constant independent of phi -- so its infimum and its average both equal d_N/d_M; and since d_N/d_M is also the universal upper bound for F_avg(T) over all maps, this map saturates both the worst-case and the average optima at once. The input-independence of its fidelity is exactly what collapses the ordering gap to equality for this particular map.

      Assessment rubric
      1. Proves F*(T) = d_N/d_M >= 1 - Kd/N via the K-consecutive-factor ratio and prod(1 - a_j) >= 1 - sum a_j (1 weight)
      2. Concludes F*(T) -> 1 as N -> infinity for fixed K (1 weight)
      3. States and justifies F(T) <= F_avg(T) for all maps because inf <= average (1 weight)
      4. Explains the optimal map has input-independent fidelity d_N/d_M, so its worst-case and average coincide and both are optimal (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)
      • Matrix analysis (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: ed08a89ba3f9c70ce368b233c9184a72a96bece564d0a443574c356413d0731f

      Item digest: 8bf1b28a875f6ad1991b903518a8f3aba4204087b064b579c744440afa5614ca

      Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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