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

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

      Question

      Consider the candidate N -> M cloning map T(X) = (d_N/d_M) Pi_M (X tensor I^{tensor (M-N)}) Pi_M, where Pi_M projects onto Sym^M(H), I is the identity on H, and d_L = dim Sym^L(H). Prove that this map achieves the worst-case fidelity bound with equality: for every pure input |phi>, tr(phi^{tensor M} T(phi^{tensor N})) = d_N/d_M, so that F(T) = d_N/d_M saturates the upper bound F(T) <= d_N/d_M. Justify each projector manipulation and the use of phi^{tensor M} being supported on Sym^M.

      Hint: mathematical route

      The symmetric-projection cloner has input-independent fidelity d_N/d_M for every pure state, because phi^{tensor M} is Pi_M-invariant and |phi><phi| is an idempotent of unit trace, so it saturates the optimal-cloning bound.

      1. Trace cyclicity sandwiches Pi_M around phi^{tensor M}.
      2. phi^{tensor M} lies in Sym^M so Pi_M fixes it; |phi><phi| is idempotent of unit trace.
      3. The fidelity equals d_N/d_M for every input, saturating the bound.
      Reference solution

      Fix any normalized |phi> in H and compute tr(phi^{tensor M} T(phi^{tensor N})). Insert the definition: tr(phi^{tensor M} T(phi^{tensor N})) = (d_N/d_M) tr( phi^{tensor M} Pi_M (phi^{tensor N} tensor I^{tensor (M-N)}) Pi_M ). Use cyclicity of the trace to move one Pi_M next to phi^{tensor M}: = (d_N/d_M) tr( Pi_M phi^{tensor M} Pi_M (phi^{tensor N} tensor I^{tensor (M-N)}) ). Now phi^{tensor M} = |phi>^{tensor M}><phi|^{tensor M} is a rank-one operator supported entirely on Sym^M(H), because |phi>^{tensor M} is a symmetric vector; therefore Pi_M phi^{tensor M} Pi_M = phi^{tensor M} (the projector acts as the identity on it). This gives = (d_N/d_M) tr( phi^{tensor M} (phi^{tensor N} tensor I^{tensor (M-N)}) ). Factor the operators across the first N and last M - N tensor factors: phi^{tensor M} = phi^{tensor N} tensor phi^{tensor (M-N)}, and phi^{tensor N} tensor I^{tensor (M-N)} acts as phi^{tensor N} on the first N factors and I on the last M - N. Hence the product on the first N factors is phi^{tensor N} phi^{tensor N} = phi^{tensor N} (idempotent, since |phi><phi| is a projector), and on the last M - N factors it is phi^{tensor (M-N)} I = phi^{tensor (M-N)}. Taking the trace factorizes: tr = (d_N/d_M) [tr(phi^{tensor N})] [tr(phi^{tensor (M-N)})] = (d_N/d_M)(1)(1) = d_N/d_M, using tr(phi) = 1. This holds for every |phi>, so the infimum over inputs is also d_N/d_M, i.e. F(T) = d_N/d_M, saturating the upper bound F(T) <= d_N/d_M proved for every map. The two key facts used are: (1) phi^{tensor M} lives in Sym^M so Pi_M leaves it unchanged, and (2) |phi><phi| is an idempotent of unit trace.

      Assessment rubric
      1. Writes tr(phi^{tensor M} T(phi^{tensor N})) with the explicit map and uses trace cyclicity to sandwich Pi_M around phi^{tensor M} (1 weight)
      2. Uses that phi^{tensor M} is supported on Sym^M so Pi_M phi^{tensor M} Pi_M = phi^{tensor M} (1 weight)
      3. Factorizes across the first N and last M - N tensor factors using idempotency of |phi><phi| and tr(phi)=1 (1 weight)
      4. Concludes the fidelity equals d_N/d_M for every input, so F(T) = d_N/d_M saturates the bound (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: 37bc921bf0cc761c6f64717bb0164077db1e5f9b574bab6998a1522303a94576

      Item digest: 50dfc466512f79d99c0a65bb7de21f90ba787a46dcb487bff9fd4a9c81908c17

      Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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