QuantumComputinglib learn · inspect · formalize
Checked on this commit 4,524 public declarations commit 4e2c5b2c0be5 Build record

Quantum Information / Tensor Symmetry

Tensor Symmetry

Exercise PLAN-320

intermediate · proof · test_public

primary source nl only. Explicit question version 2 with distinct contract-change review; the predecessor question is not equivalent current gold. Core, family and split are retained. No new Lean verification is claimed for this NL view.

Assumptions and conventions

  • The two subsystems have equal local dimension; partial transposition is taken on the second subsystem.
  • Isotropic symmetry conjugates by a unitary tensored with its complex conjugate; Werner symmetry conjugates by a unitary tensored with itself.

This question explicitly revises its historical contract. A Lean companion must bind the current contract hash, not the predecessor hash. This is one reserved core, not two exercises.

Question

Work on C^d tensor C^d in the fixed local bases used for complex conjugation and partial transpose on the second subsystem. Write Gamma(Z)=Z^{T_B}. A state means a positive semidefinite operator of trace1. Call the invariance (U tensor conjugate(U))*Z*(U† tensor U^T)=Z for every unitary U isotropic OPERATOR SYMMETRY, and call (U tensor U)*Z*(U† tensor U†)=Z for every unitary U Werner OPERATOR SYMMETRY. An isotropic state or a Werner state must additionally be a state.

Assess the predecessor's assertion: 'A state is isotropic if and only if its partial transpose on the second subsystem is a Werner state.' Is it true for every allowed local dimension and every state? For d>=2, use the normalized maximally entangled projector Phi_d=|Phi_d><Phi_d|, |Phi_d>=(1/sqrt(d))*sum_{i=1}^d |i,i>, to prove or refute that assertion. Compute Gamma(Phi_d) in terms of the swap F and test positivity on an explicit antisymmetric vector; do not redefine Werner state to mean only an invariant operator.

For arbitrary operators A,B,C,D on C^d and Z on C^d tensor C^d, prove the full sandwich identity Gamma((A tensor B)*Z*(C tensor D))=(A tensor D^T)*Gamma(Z)*(C tensor B^T). Apply it to an actual isotropic conjugation, specifying the distinct left and right factors and all adjoints, to prove the unconditional equivalence: Z has isotropic operator symmetry if and only if Gamma(Z) has Werner operator symmetry. No positivity or nonzero premise may be imposed on this operator statement.

Finally, for an arbitrary density operator rho, prove the correct conditional state-level statement: [rho is isotropic and rho is PPT] if and only if [Gamma(rho) is a Werner state], where PPT means Gamma(rho)>=0. Explain why this is a conditional case, not a standing hypothesis that would silently remove the maximally entangled counterexample. Discuss the zero operator, d=1, and the lack of density states at d=0 without dividing by zero. Distinguish trace/Hermiticity preservation, positivity, and involutivity.

Hint: mathematical route

Partial transpose transports isotropic and Werner OPERATOR symmetries involutively, but may destroy positivity: Phi_d maps to F/d. The state-level equivalence holds exactly for the isotropic PPT case, not for all isotropic states.

  1. The isotropic state Phi_d has partial transpose F/d, whose antisymmetric expectation is-1/d for d>=2; this refutes the original state-level iff while preserving its valid symmetry-transport target.
  2. The full sandwich identity reverses only second-factor multiplication. An isotropic conjugation uses left U tensor conjugate(U) and right U† tensor U^T, yielding Werner conjugation after partial transpose.
  3. Involutivity proves isotropic operator symmetry of any Z iff Werner operator symmetry of Gamma(Z), without positivity or nonzero assumptions.
  4. For a density rho, isotropic symmetry plus PPT is equivalent to Gamma(rho) being a Werner state. Zero is not a state; d=1 is trivial and d=0 has no density states. No hidden PPT premise restores the false predecessor.
Reference solution

The predecessor's state-level iff is false for every d>=2. The maximally entangled vector is normalized, and for any unitary U its coefficient at |a,b> after U tensor conjugate(U) is (1/sqrt(d))*sum_i U_{ai}*conjugate(U_{bi})=delta_{ab}/sqrt(d). Thus Phi_d is an isotropic positive trace-one state. Expanding it gives Phi_d=(1/d)*sum_{i,j}|i><j| tensor |i><j|, so Gamma(Phi_d)=(1/d)*sum_{i,j}|i><j| tensor |j><i|=F/d. For d>=2 the unit vector a=(|1,2>-|2,1>)/sqrt(2) satisfies F*a=-a. Hence <a|Gamma(Phi_d)|a>=-1/d<0. Although F/d is Hermitian, has trace1 because tr F=d, and has Werner operator symmetry, it is not positive and therefore is NOT a Werner state. This exact counterexample preserves the original state domain; it is not merely a failure to find a formal proof. At d=2 the spectrum is1/2,1/2,1/2,-1/2.

For the general identity, expand Z=sum_{i,j} Z_{ij} tensor E_{ij}, where E_{ij}=|i><j| on the second subsystem. Then Gamma((A tensor B)*Z*(C tensor D))=sum_{i,j} A*Z_{ij}*C tensor (B*E_{ij}*D)^T =sum_{i,j} A*Z_{ij}*C tensor D^T*E_{ji}*B^T =(A tensor D^T)*Gamma(Z)*(C tensor B^T). This uses only linearity and reversal of multiplication under ordinary transpose in the second factor. The first-factor multiplication remains in its original order; partial transpose is not an unrestricted anti-homomorphism of the full bipartite operator algebra.

An actual isotropic conjugation has A=U, B=conjugate(U), C=U† and D=(conjugate(U))†=U^T. Thus D^T=U and B^T=U†, giving Gamma((U tensor conjugate(U))*Z*(U† tensor U^T))=(U tensor U)*Gamma(Z)*(U† tensor U†). The two right factors are the adjoints of the two left factors, not another copy of them. Setting A=C=U and B=D=conjugate(U), as the predecessor answer did, is not this conjugation for a general unitary.

Since Gamma^2=id, it is injective. If the isotropic conjugation fixes Z for every U, the displayed identity shows the Werner conjugation fixes Gamma(Z) for every U. Conversely, if that Werner conjugation fixes Gamma(Z), the same identity makes Gamma of the isotropic conjugation equal Gamma(Z); applying Gamma again gives equality with Z. Therefore isotropic operator symmetry of Z is equivalent to Werner operator symmetry of Gamma(Z), for EVERY operator Z, including nonpositive, non-Hermitian and zero operators. No state-preservation conclusion follows solely from this linear symmetry transport.

For the conditional theorem, let rho be any density operator; no PPT assumption has yet been imposed. Gamma preserves trace, Hermiticity and involutivity. If rho is isotropic AND PPT, Gamma(rho) has Werner symmetry by the operator equivalence, is positive by PPT, and has trace1, so it is a Werner state. Conversely, if Gamma(rho) is a Werner state, it is positive, so rho is PPT, and its Werner symmetry transports back to isotropic symmetry of the already-given state rho. This proves [rho isotropic and PPT] iff [Gamma(rho) Werner state]. The positivity condition is a conclusion/condition within this equivalence, not a standing premise restricting the earlier universal assessment. Phi_d is isotropic but not PPT for d>=2, exactly explaining why it refutes the old forward implication. The old reverse implication is valid when rho is already known to be a state; the universal iff fails through the forward positivity assertion.

The zero operator and its partial transpose satisfy both operator symmetries, but have trace0 and are not states. For d=1 the operator space consists of scalars, Gamma is the identity, and both conjugations act trivially. The unique density operator is1, is PPT, and satisfies both state symmetries; the nontrivial negative antisymmetric sector is absent. The source's nontrivial Werner family is presented for d>=2; this is its natural one-dimensional symmetry/state boundary, not a use of a parametrization with denominator d^2-1. At d=0 the bipartite space is zero-dimensional and its only operator is0: the operator identities are vacuous/trivial, but trace0 prevents any density state. Phi_d and its1/sqrt(d) normalization are not defined or used there.

This is an explicitly changed question contract: it replaces a demand to prove a false state iff by refuting it and proving the correct symmetry transport and conditional PPT case. The source's Eq6.46 supports the sandwich identity, while Eq6.45's overbroad state wording does not prove positivity. Static source inspection and this mathematical reconstruction are not a newly executed Lean theorem, a native formal view, or successor approval.

Assessment rubric
  1. Explicitly assesses/refutes the predecessor's unconditional state iff for d>=2: proves Phi_d is an isotropic density operator, computes Gamma(Phi_d)=F/d and exhibits a normalized antisymmetric vector with expectation-1/d. Distinguishes Werner symmetry from a positive trace-one Werner state. (1 weight)
  2. Proves the full sandwich formula for arbitrary A,B,C,D,Z by second-factor matrix units or an equivalent complete argument. Uses A=U,B=conjugate(U),C=U†,D=U^T for an actual conjugation and retains all right adjoints; does not silently set U†=U. (1 weight)
  3. Uses the correct sandwich identity and Gamma^2=id to prove both directions of the unconditional operator-symmetry equivalence for every Z, without a positivity, nonzero or PPT standing premise. (1 weight)
  4. For arbitrary density rho proves [isotropic and PPT] iff [Gamma(rho) Werner state], explaining the role of trace/Hermiticity versus positivity and why PPT is a conditional case rather than a hidden restriction. Handles zero operator, d=1 and absence of d=0 density states without invalid normalization or a false claim of equivalence to the predecessor's requested proof. (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: 7e02133d768c2c2525f000b0e7671e0665919c75600a3eea91edd0e774260b7f

Item digest: 056dd88e06eb9de507f9c3064a6a097706e63fa9d5bb73c135b3cdafbd7b3a9f

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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

Question revision lineage

{ "question_version": 2, "predecessor_key": "qcb-core-plan-320-isotropic-partial-transpose", "predecessor_item_digest": "ba9009dea18f4b0ac26f611f7313943bc82ce7ea5ef58a3f0bf6bd28263b2916", "predecessor_contract_hash": "0164cb961b1796b8988514c3091185d2f45c0172e0dd169d8dbfb24b646861e7", "current_contract_hash": "7e02133d768c2c2525f000b0e7671e0665919c75600a3eea91edd0e774260b7f", "changed_contract_fields": [ "question" ], "repair_record": "shared/repairs/plan-320-partial-transpose-state-successor.json", "repair_record_digest": "c597c3868f09a50231b7f2be997a94e9a1cabc30ccae49277cd65f19c08f9004", "review_record": "reports/textbook-v1/repairs/plan-320-partial-transpose-state-successor-migration-revalidation-review.json", "review_digest": "57674a28884a2e86c41fa959e7cf0863ee3b0e08f93741827f4fba94b6c55cbe", "equivalence_to_predecessor_claimed": false, "additional_core_count": 0 }