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

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 finite; fixed common orthonormal basis defines transpose, conjugation and maximally entangled vector
  • U is unitary; X arbitrary linear operator

    Question

    Let |Phi+> = (1/sqrt(d)) sum_{i=1}^d |i>_A |i>_B be the standard maximally entangled state on C^d tensor C^d. (a) Prove the transpose trick: for every operator X in L(C^d), (X_A tensor I_B)|Phi+> = (I_A tensor X^T_B)|Phi+>, where X^T is the transpose of X in the fixed computational basis. (b) Deduce that |Phi+> is invariant under every unitary of the form U tensor conj(U) (U_A tensor the complex conjugate of U on B). Carefully state the role of the computational basis in defining the transpose and conjugate.

    Hint: mathematical route

    Transpose trick and exact U tensor bar U invariance in a fixed basis, with explicit counterexample and source discrepancy for un-conjugated U tensor U.

    1. Expand both tensor actions and relabel the finite double sum to prove the transpose trick.
    2. Conjugating UU dagger=I yields bar U U^T=I.
    3. Combine the two identities to prove U tensor bar U invariance.
    4. The diagonal phase example refutes U tensor U invariance without conjugation.
    Reference solution

    Expand the left side: (X tensor I)|Phi>=(1/sqrt d)sum_{i,j}X(j,i)|j> tensor|i>. Expanding (I tensor X^T)|Phi> gives(1/sqrt d)sum_{i,j}X(i,j)|i> tensor|j>; interchanging dummy indices yields the same vector. For a unitary U, apply that identity with X=U and then apply I tensor bar U: (U tensor bar U)|Phi>=(I tensor bar U U^T)|Phi>. Since UU dagger=I, taking entrywise complex conjugates gives bar U U^T=I. The vector is therefore unchanged. Both transpose and bar refer to the same fixed orthonormal basis used to define|Phi>. In contrast U tensor U does not generally fix this vector: for d2 and U=diag(1,i), (|00>+|11>)/sqrt2 becomes(|00>-|11>)/sqrt2. Thus conjugation on the second factor is essential, not a removable notation convention.

    Assessment rubric
    1. Correct finite-index transpose calculation with no false intermediate identity (1 weight)
    2. Correct bar U U^T=I from unitary identity (1 weight)
    3. Same fixed basis for transpose/conjugation and entangled vector (1 weight)
    4. Valid diag(1,i) counterexample to missing conjugation (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)
    • 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: 25ebf86129a685cdd72ea268f14e557b7b70330522d7a81da17503db805da6a6

    Item digest: 05e0d2384e44696ebe45e9477ead16e724d11c08a081759a128d460e2e821847

    Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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