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

Quantum Information / Representation Qit

Representation Qit

Exercise PLAN-107

intermediate · proof · test_public

primary source nl only. Additive answer successor with distinct content-bound review; historical rejected answer retained only for audit. No new Lean verification is claimed for this NL view.

Assumptions and conventions

      Question

      Let rho be any single-qubit density matrix (a 2x2 positive semidefinite operator with trace 1). Using the fact that the Pauli operators {1, X, Y, Z} generate an irreducible representation of the single-qubit Pauli group acting on C^2, prove that (1/4)(rho + X rho X + Y rho Y + Z rho Z) = (1/2) 1. Base your argument on Schur's Lemma / the commutant-is-scalars corollary and on the trace, not on a brute-force coordinate computation.

      Hint: mathematical route

      Pauli conjugation permutes operator-conjugation terms modulo phases only when the right adjoint is retained; Schur and trace then give the maximally mixed output on C^2.

      1. Each P in {I,X,Y,Z} is Hermitian-unitary, so P*rho*P^dagger=P*rho*P; a scalar phase cancels only against its adjoint phase.
      2. Q*T*Q^dagger=(1/4)sum_P (QP)*rho*(QP)^dagger; QP permutes the Pauli classes modulo unit phases, so the correctly conjugated sum is T.
      3. Unitary Q then gives Q*T=T*Q, and hence commutation with the entire irreducible Pauli representation.
      4. The scalar Schur corollary applies on finite-dimensional C^2 and gives T=lambda*I.
      5. Cyclicity gives tr(T)=1=2*lambda, so T=I/2 independently of the density matrix entries.
      Reference solution

      Let S={I,X,Y,Z} and T=(1/4) sum over P in S of P*rho*P^dagger. Each of these four matrices is Hermitian and unitary, so this is the operator in the question. For Q in {X,Y,Z}, the conjugation expansion is Q*T*Q^dagger=(1/4) sum_P (Q*P)*rho*(Q*P)^dagger. The rightmost factor is P^dagger*Q^dagger=P*Q, not Q*P. Products of distinct Hermitian Paulis need not themselves be Hermitian, so that adjoint cannot be dropped.

      Left multiplication by Q permutes the four Pauli classes modulo scalar phases. More explicitly, for each P there are a unit-modulus scalar omega_P and a uniquely associated R_P in S such that Q*P=omega_P*R_P, and P->R_P is a permutation. In each conjugation term the scalar cancels with its complex conjugate: (omega_P R_P)*rho*(omega_P R_P)^dagger=R_P*rho*R_P^dagger. Relabeling this finite sum therefore proves Q*T*Q^dagger=T. Since Q is unitary, multiplying on the right by Q gives Q*T=T*Q. The same follows for all products of the generators and scalar central phases, so T commutes with the irreducible Pauli representation.

      Now use Schur's commutant-is-scalars corollary on the finite-dimensional complex space C^2: T=lambda*I. The hypotheses needed for its scalar conclusion are present, not silently assumed for a general field or an infinite-dimensional representation. Cyclicity of trace and P^dagger*P=I give tr(P*rho*P^dagger)=tr(rho)=1 for every P. Thus tr(T)=1. On the other hand tr(lambda*I)=2*lambda, so lambda=1/2 and T=I/2. This follows from conjugation invariance, irreducibility and trace normalization, without computing the entries of rho. Positivity supplies the density-state interpretation but is not needed for the linear-operator identity T(A)=tr(A)*I/2. That extension is a mathematical consequence of the same proof, not a newly compiled local Lean theorem or a circuit-resource claim.

      Assessment rubric
      1. Expands Q*T*Q^dagger with right factor (QP)^dagger=PQ, then uses a bijection of Pauli classes modulo unit phases and adjoint phase cancellation. Does not treat every product QP as Hermitian. (1 weight)
      2. Derives commutation with the whole representation and applies the scalar commutant corollary on finite-dimensional C^2 with the given irreducibility. (1 weight)
      3. Uses trace cyclicity and P^dagger*P=I to get tr(T)=1=2*lambda and lambda=1/2. (1 weight)
      4. Concludes T=I/2 for every input density matrix by the Schur/averaging argument, not brute-force coordinates or a new formal/circuit claim. (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: 11c31361c66f8f024eece34bda8ca89fd2754069adea474f939160f43b4dbdaf

      Item digest: 27dbc029f5e7856c2ef078f782564d1e1b35c8c9a283a9394c8617aba39196c0

      Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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

      Answer revision lineage

      { "predecessor_item_digest": "78bd0325d3ec88da16fbd93359b46049553ad3e088445cbb3f077baccc1e530a", "predecessor_key": "qcb-core-plan-107-pauli-twirl-maximally-mixed", "repair_record": "shared/repairs/plan-107-pauli-adjoint-repair.json", "repair_record_digest": "c6c7b731c68107c1b125b7d98580ee09d3c9db16660e823deb4d5275bc67c8e7", "review_record": "reports/textbook-v1/repairs/plan-107-pauli-adjoint-repair-migration-revalidation-review.json", "review_digest": "c12fbdecd508c640ab02ca021efa49d5ac82294b14e717e481cdb3c40e0a5725" }