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

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

      Let rho be a state on A^{tensor n}, and let rhobar = (1/n!) sum_{pi in S_n} Q_pi rho Q_pi^dagger be its symmetrization (Q_pi the permutation operators). Let Pi_n be the projector onto the symmetric subspace Sym^n(H_A). Prove the identity Pi_n rhobar Pi_n = Pi_n rho Pi_n. In your proof establish and use the intertwining relation Pi_n Q_pi = Pi_n = Q_pi Pi_n for every pi (the symmetric projector absorbs permutations), and be explicit about why the 1/n! average collapses.

      Hint: mathematical route

      Because the symmetric projector absorbs permutations (Pi_n Q_pi = Pi_n), the symmetrization average collapses and Pi_n rhobar Pi_n = Pi_n rho Pi_n, so symmetric-subspace compression cannot distinguish a state from its symmetrization.

      1. Pi_n absorbs permutations: Pi_n Q_pi = Pi_n = Q_pi Pi_n.
      2. Each averaged term becomes Pi_n rho Pi_n independent of pi.
      3. The 1/n! average collapses to a single Pi_n rho Pi_n.
      Reference solution

      First establish Pi_n Q_pi = Pi_n for all pi. The symmetric subspace Sym^n(H_A) is by definition the set of vectors fixed by every Q_pi, and Pi_n is the orthogonal projector onto it. For any vector |w>, Q_pi |w> and |w> have the same component in Sym^n because Q_pi acts as the identity on Sym^n and permutes the orthogonal complement among itself (the decomposition into isotypic components is Q_pi-invariant, and the trivial/symmetric isotype is pointwise fixed). Concretely, Pi_n = (1/n!) sum_sigma Q_sigma (the projector onto the trivial isotype equals the group average), and Q_sigma Q_pi = Q_{sigma pi} ranges over all of S_n as sigma does, so Pi_n Q_pi = (1/n!) sum_sigma Q_{sigma pi} = (1/n!) sum_tau Q_tau = Pi_n; likewise Q_pi Pi_n = Pi_n and Pi_n is self-adjoint with Q_pi^dagger = Q_{pi^{-1}}, giving Pi_n Q_pi^dagger = Pi_n too. Now compute Pi_n rhobar Pi_n = Pi_n [ (1/n!) sum_pi Q_pi rho Q_pi^dagger ] Pi_n = (1/n!) sum_pi (Pi_n Q_pi) rho (Q_pi^dagger Pi_n). Using Pi_n Q_pi = Pi_n and Q_pi^dagger Pi_n = Pi_n for every pi, each summand becomes Pi_n rho Pi_n, independent of pi. Hence Pi_n rhobar Pi_n = (1/n!) sum_pi Pi_n rho Pi_n = (1/n!)(n!) Pi_n rho Pi_n = Pi_n rho Pi_n. The 1/n! average collapses precisely because the permutations are absorbed by the flanking symmetric projectors, leaving n! identical copies of Pi_n rho Pi_n. This shows that, as far as the symmetric-subspace compression is concerned, a state and its symmetrization are indistinguishable.

      Assessment rubric
      1. Establishes Pi_n Q_pi = Q_pi Pi_n = Pi_n using Pi_n = (1/n!) sum_sigma Q_sigma and the group reshuffle Q_sigma Q_pi = Q_{sigma pi} (1 weight)
      2. Writes Pi_n rhobar Pi_n = (1/n!) sum_pi (Pi_n Q_pi) rho (Q_pi^dagger Pi_n) (1 weight)
      3. Reduces each summand to Pi_n rho Pi_n via the absorption identity (including Q_pi^dagger Pi_n = Pi_n) (1 weight)
      4. Collapses the n! identical terms to conclude Pi_n rhobar Pi_n = Pi_n rho Pi_n (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)

      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: 5f9b00f9eef7b7b85ea81cf919c3102526b3d01decc38f5077a4a521caee2040

      Item digest: e2e13bbb34865744a0e5a9f2ab454f606e78c8144fe0237f4ed4c708ddceebdc

      Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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