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

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

  • d>=1; M>=N>=1; X positive semidefinite
  • Haar pure-power projector identity as stated; fixed ancillary basis for Kraus insertions

    Question

    Let H=C^d with d>=1, and integers M>=N>=1. Let Pi_L project onto the symmetric subspace of H tensor L and d_L its dimension. Define T(X)=(d_N/d_M)Pi_M(X tensor I^{tensor(M-N)})Pi_M. Prove T is completely positive and derive the exact trace formula tr T(X)=tr(X Pi_N) for every positive X. You may use Pi_L=d_L times the Haar average of|phi><phi| tensor L over unit vectors. Characterize trace preservation for positive X and show why it includes more than mixtures of pure tensor powers.

    Hint: mathematical route

    Symmetric cloning map complete positivity via multi-Kraus identity extension and exact trace pairing; trace preserved on all symmetric support, not only separable pure-power mixtures.

    1. Ancillary identity extension has Kraus maps v->v tensor e_j; compression and positive scaling preserve complete positivity.
    2. Taking a partial trace in the Haar projector identity gives Q=(d_M/d_N)Pi_N.
    3. Cyclicity and the partial-trace pairing give trT(X)=tr(XPi_N)<=trX.
    4. The Hilbert-Schmidt square identifies equality exactly with symmetric support.
    5. A symmetric entangled pure state shows equality is broader than mixtures of pure powers.
    Reference solution

    Choose an orthonormal basis e_j of the ancillary tensor factors and insertion maps K_j:v->v tensor e_j. Then sum_j K_j X K_j dagger=X tensor I, so this map is completely positive; generally it needs several Kraus maps, not one isometry. Compression Y->Pi_M Y Pi_M is also completely positive, and positive scaling preserves that property. Let Q be the partial trace of Pi_M over the last M-N factors. The given Haar identity gives Q=d_M integral |phi><phi| tensor N=(d_M/d_N)Pi_N, because each traced pure projector has trace1. Cyclicity and Pi_M squared=Pi_M yield tr T(X)=(d_N/d_M)tr[(X tensor I)Pi_M]=(d_N/d_M)tr(XQ)=tr(X Pi_N)<=tr X. Equality holds exactly when tr[X(I-Pi_N)]=0. For X>=0 this is equivalent to support(X) contained in the symmetric subspace: the positive square-root identity tr[X(I-Pi_N)]=||(I-Pi_N)X^(1/2)||_HS^2 gives the equivalence. Every mixture of pure powers lies there, but not every symmetric state is such a mixture. For d2,N2, the entangled vector(|01>+|10>)/sqrt2 is symmetric, so its projector preserves trace under T, yet it is not a mixture of pure powers (a pure entangled state cannot be a convex combination of product pure states). Thus support in Sym^N, not separability into pure powers, is the correct equality condition.

    Assessment rubric
    1. Use a sum of insertion Kraus maps, not a single isometry for tensoring with identity (1 weight)
    2. Derive partial trace of Pi_M using Haar average with correct dimension ratio (1 weight)
    3. Exact trace formula and positive support equality condition (1 weight)
    4. Valid symmetric entangled counterexample to pure-power-mixture equality characterization (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)
    • Harmonic analysis (frozen curriculum anchor; see graph registry)
    • Tensor networks (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: c45c9baa937d20bca01fd856e1db05f5d179ae5d34b6afb933d1ab61c813e46e

    Item digest: 759b3d5a55c7fb2b6fdecb9196f4d8a053109e944bb8a426cdefc98a5cc0a376

    Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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