ChannelTimeReversalNoGo

Abstract

Randomisation and complete positivity obstruct reversal of every unitary channel.

Definition 1.1 (Symmetries of the channel set).

$$\forall d\in \mathbb{N},\forall S\in \mathrm{MatrixMap}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)\to \mathrm{MatrixMap}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\mathrm{IsChannelSymmetry}\left(S\right)=\left((\mathrm{Set}.\mathrm{BijOn}\left(S,\{Phi:\mathrm{MatrixMap}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)\mid \mathrm{IsCPTP}\left(Phi\right)\},\{Phi:\mathrm{MatrixMap}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)\mid \mathrm{IsCPTP}\left(Phi\right)\}\right))\wedge (\forall Phi\in \mathrm{MatrixMap}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall Psi\in \mathrm{MatrixMap}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),(\mathrm{IsCPTP}\left(Phi\right))\Rightarrow ((\mathrm{IsCPTP}\left(Psi\right))\Rightarrow (\forall p\in \mathbb{R},(0\le p)\Rightarrow ((p\le 1)\Rightarrow (S\left(((p:\mathbb{C}))\cdot (Phi)+(((1-p:\mathbb{R}):\mathbb{C}))\cdot (Psi)\right)=((p:\mathbb{C}))\cdot (S\left(Phi\right))+(((1-p:\mathbb{R}):\mathbb{C}))\cdot (S\left(Psi\right)))))))\right)$$

Formalization. D5/S3/QuantumChannels/ChannelTimeReversalNoGo.IsChannelSymmetry (✓ std3).

Citation. Giulio Chiribella and Erik Aurell and Karol Życzkowski (2021). Symmetries of quantum evolutions. DOI: 10.1103/PhysRevResearch.3.033028. URL: https://arxiv.org/abs/2101.04962.

Commentary.

Definition 3, PDF page 5: “A symmetry transformation from the operation space Op(Hin , Hout ) to the operation space Op(Kin , Kout ) (an operation space symmetry, for short) is a bijective transformation S : Op(Hin , Hout ) → Op(Kin , Kout )” that “is consistent with randomisations, namely S(p Q + (1−p) R) = p S(Q)+(1−p) S(R), for every pair of quantum operations Q and R, and for every probability p ∈ [0, 1]”. On channels the null-operation requirement has no instance. Here Set.BijOn states bijectivity on the set defined by IsCPTP, and the second conjunct states the complete binary randomisation identity for every real probability in [0,1].

Definition 1.2 (Conjugation by a matrix).

$$\forall d\in \mathbb{N},\forall U\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\mathrm{unitaryChannel}\left(U\right)=(\mathrm{LinearMap}.\mathrm{mulRight}\left(\mathbb{C},\mathrm{star}\left(U\right)\right)){\circ }_l(\mathrm{LinearMap}.\mathrm{mulLeft}\left(\mathbb{C},U\right))$$

Formalization. D5/S3/QuantumChannels/ChannelTimeReversalNoGo.unitaryChannel (✓ std3).

Citation. Giulio Chiribella and Erik Aurell and Karol Życzkowski (2021). Symmetries of quantum evolutions. DOI: 10.1103/PhysRevResearch.3.033028. URL: https://arxiv.org/abs/2101.04962.

Commentary.

For every natural dimension d and every complex d by d matrix U, unitaryChannel U is LinearMap.mulRight ℂ (star U) after LinearMap.mulLeft ℂ U. It sends X to U X (star U). For unitary U this is a completely positive trace-preserving map.

Definition 1.3 (No time reversal on all channels).

$$claim=\left(\forall d\in \mathbb{N},(2\le d)\Rightarrow (\forall S\in \mathrm{MatrixMap}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)\to \mathrm{MatrixMap}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),(\mathrm{IsChannelSymmetry}\left(S\right))\Rightarrow ((\neg (\forall U\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),(U\in \mathrm{Matrix}.\mathrm{unitaryGroup}\left(\mathrm{Fin}\left(d\right),\mathbb{C}\right))\Rightarrow (S\left(\mathrm{unitaryChannel}\left(U\right)\right)=\mathrm{unitaryChannel}\left(\mathrm{star}\left(U\right)\right))))\wedge (\neg (\forall U\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),(U\in \mathrm{Matrix}.\mathrm{unitaryGroup}\left(\mathrm{Fin}\left(d\right),\mathbb{C}\right))\Rightarrow (S\left(\mathrm{unitaryChannel}\left(U\right)\right)=\mathrm{unitaryChannel}\left(\mathrm{Matrix}.\mathrm{transpose}\left(U\right)\right))))))\right)$$

Formalization. D5/S3/QuantumChannels/ChannelTimeReversalNoGo.claim (✓ std3).

Citation. Giulio Chiribella and Erik Aurell and Karol Życzkowski (2021). Symmetries of quantum evolutions. DOI: 10.1103/PhysRevResearch.3.033028. URL: https://arxiv.org/abs/2101.04962.

Commentary.

Section V.B, PDF page 7: “We conjecture that this assumption can be lifted, and that the no-go theorem to time reversal applies also to symmetries of the set of quantum channels.” The dimension d ranges over every natural number at least two. IsCPTP is the existing completely positive trace-preserving predicate on complex-linear maps of d by d matrices. For every natural dimension d and every d by d complex matrix U, conjugation by U is LinearMap.mulRight ℂ (star U) after LinearMap.mulLeft ℂ U, equal to LinearMap.mulLeftRight ℂ (U, star U). The displayed claim uses unitaryChannel in both targets. The two targets are conjugation by star U and by Matrix.transpose U. The quantifier ranges over every randomisation-consistent bijection of this channel set.

Theorem 1.4 (Pauli spectral projectors are positive semidefinite).

$$\forall a\in \mathrm{Fin}\left(3\right),\forall e\in Bool,\mathrm{Matrix}.\mathrm{PosSemidef}\left(D5.S3.\mathrm{Quantum}.\mathrm{Magic}.\mathrm{WignerDistanceMinimum}.\mathrm{spectral}\left([D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{StabilizerPairLocalUnitaryInequivalence}.\mathrm{Pauli}.X,D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{StabilizerPairLocalUnitaryInequivalence}.\mathrm{Pauli}.Y,D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{StabilizerPairLocalUnitaryInequivalence}.\mathrm{Pauli}.Z]\left(a\right),\mathrm{ite}\left(e=true,1,0\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/QuantumChannels/ChannelTimeReversalNoGo.density_psd (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every axis index a in Fin 3 and Boolean sign e, the spectral projector of the Pauli axis a with sign e is positive semidefinite.

Theorem 1.5 (Pauli spectral projectors have trace one).

$$\forall a\in \mathrm{Fin}\left(3\right),\forall e\in Bool,\mathrm{Matrix}.\mathrm{trace}\left(D5.S3.\mathrm{Quantum}.\mathrm{Magic}.\mathrm{WignerDistanceMinimum}.\mathrm{spectral}\left([D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{StabilizerPairLocalUnitaryInequivalence}.\mathrm{Pauli}.X,D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{StabilizerPairLocalUnitaryInequivalence}.\mathrm{Pauli}.Y,D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{StabilizerPairLocalUnitaryInequivalence}.\mathrm{Pauli}.Z]\left(a\right),\mathrm{ite}\left(e=true,1,0\right)\right)\right)=1$$

Proof. Machine-checked in Lean as D5/S3/QuantumChannels/ChannelTimeReversalNoGo.density_trace (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every axis index a in Fin 3 and Boolean sign e, the spectral projector of the Pauli axis a with sign e has trace one.

Theorem 1.6 (Expansion in the qubit Pauli basis).

$$\forall X\in \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right),X=(\frac{\mathrm{Matrix}.\mathrm{trace}\left(X\right)}{2})\cdot ((1:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right)))+\sum _{b:\mathrm{Fin}\left(3\right)}((\frac{\mathrm{Matrix}.\mathrm{trace}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{pauli}\left(b\right)\cdot X\right)}{2})\cdot (D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{pauli}\left(b\right)))$$

Proof. Machine-checked in Lean as D5/S3/QuantumChannels/ChannelTimeReversalNoGo.pauli_expansion (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every complex two-by-two matrix is the sum of its trace component and its three Pauli components.

Theorem 1.7 (Pauli axes have zero trace).

$$\forall a\in \mathrm{Fin}\left(3\right),\mathrm{Matrix}.\mathrm{trace}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{pauli}\left(a\right)\right)=0$$

Proof. Machine-checked in Lean as D5/S3/QuantumChannels/ChannelTimeReversalNoGo.sigma_trace (✓ std3). ∎

Source. Repository-derived.

Commentary.

Each of the three qubit Pauli axes has trace zero.

Definition 1.8 (Qubit spin flip).

$$D5.S3.\mathrm{QuantumChannels}.\mathrm{ChannelTimeReversalNoGo}.\mathrm{QubitUnital}.J=(\mathrm{unitaryChannel}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{pauli}\left(1\right)\right)){\circ }_l(\mathrm{LinearEquiv}.\mathrm{toLinearMap}\left(\mathrm{Matrix}.\mathrm{transposeLinearEquiv}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C},\mathbb{C}\right)\right))$$

Formalization. D5/S3/QuantumChannels/ChannelTimeReversalNoGo.J (✓ std3).

Source. Repository-derived.

Commentary.

The complex-linear qubit spin flip transposes a matrix and conjugates it by the second Pauli axis.

Theorem 1.9 (Trace formula for the qubit spin flip).

$$\forall X\in \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right),D5.S3.\mathrm{QuantumChannels}.\mathrm{ChannelTimeReversalNoGo}.\mathrm{QubitUnital}.J\left(X\right)=(\mathrm{Matrix}.\mathrm{trace}\left(X\right))\cdot ((1:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right)))-X$$

Proof. Machine-checked in Lean as D5/S3/QuantumChannels/ChannelTimeReversalNoGo.J_apply (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every complex two-by-two matrix X, the spin flip sends X to its trace times the identity minus X.

Theorem 1.10 (Time-reversal symmetries do not exist).

$$\forall d\in \mathbb{N},(2\le d)\Rightarrow (\forall S\in \mathrm{MatrixMap}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)\to \mathrm{MatrixMap}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),(\mathrm{IsChannelSymmetry}\left(S\right))\Rightarrow ((\neg (\forall U\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),(U\in \mathrm{Matrix}.\mathrm{unitaryGroup}\left(\mathrm{Fin}\left(d\right),\mathbb{C}\right))\Rightarrow (S\left(\mathrm{unitaryChannel}\left(U\right)\right)=\mathrm{unitaryChannel}\left(\mathrm{star}\left(U\right)\right))))\wedge (\neg (\forall U\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),(U\in \mathrm{Matrix}.\mathrm{unitaryGroup}\left(\mathrm{Fin}\left(d\right),\mathbb{C}\right))\Rightarrow (S\left(\mathrm{unitaryChannel}\left(U\right)\right)=\mathrm{unitaryChannel}\left(\mathrm{Matrix}.\mathrm{transpose}\left(U\right)\right))))))$$

Proof. Machine-checked in Lean as D5/S3/QuantumChannels/ChannelTimeReversalNoGo.result (✓ std3). ∎

Resolves. Problems/chiribella-aurell-zyczkowski-2021-channel-time-reversal (proved) by D5/S3/QuantumChannels/ChannelTimeReversalNoGo.result.

Source. Repository-derived.

Acknowledgement. Giulio Chiribella and Erik Aurell and Karol Życzkowski (2021). Symmetries of quantum evolutions. DOI: 10.1103/PhysRevResearch.3.033028. URL: https://arxiv.org/abs/2101.04962.

Commentary.

For dimensions at least three, Bi_basic forces three finite-block identities; diagonal_contradiction makes the positive block have trace zero, contradicting its trace one. For qubits, finite_pauli_identity and unital_reversed identify the action on unital channels. The pure_preimage and pure_density_rotation lemmas supply a unitary rotation of a pure replacement preimage. The forced_witness_output identity then gives diag(9/8, -1/8), whose negative diagonal entry proves inverse_unitary_no_go. Double transposition preserves complete positivity, trace preservation and convex mixtures, is involutive, and sends conjugation by the transpose of U to conjugation by star U. Composing with this transformation reduces the transpose target to the adjoint target.

References

• Truth anchor: D5/S3/QuantumChannels/ChannelTimeReversalNoGo.IsChannelSymmetry
• Truth anchor: D5/S3/QuantumChannels/ChannelTimeReversalNoGo.J
• Truth anchor: D5/S3/QuantumChannels/ChannelTimeReversalNoGo.J_apply
• Truth anchor: D5/S3/QuantumChannels/ChannelTimeReversalNoGo.claim
• Truth anchor: D5/S3/QuantumChannels/ChannelTimeReversalNoGo.density_psd
• Truth anchor: D5/S3/QuantumChannels/ChannelTimeReversalNoGo.density_trace
• Truth anchor: D5/S3/QuantumChannels/ChannelTimeReversalNoGo.pauli_expansion
• Truth anchor: D5/S3/QuantumChannels/ChannelTimeReversalNoGo.result
• Truth anchor: D5/S3/QuantumChannels/ChannelTimeReversalNoGo.sigma_trace
• Truth anchor: D5/S3/QuantumChannels/ChannelTimeReversalNoGo.unitaryChannel
• Dependency: D5/S3/Quantum/Entanglement/ElegantJointMeasurementSourceNoise
• Dependency: D5/S3/Quantum/Entanglement/GraphDensity/FormationBounds
• Dependency: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction
• Dependency: D5/S3/Quantum/Fibers/RankOneFeedbackProtocol
• Dependency: D5/S3/Quantum/Information/RenyiInformationCombiningOrderThree
• Dependency: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation
• Dependency: D5/S3/Quantum/QuantumChannels/IptPptSquaredEquivalence
• Dependency: D5/S3/Quantum/QuantumChannels/PositiveFilterTransposeRefutation
• Dependency: D5/S3/Quantum/QuantumChannels/ProductUnitaryChoiSpectrum
• Dependency: D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation
• Dependency: D5/S3/Quantum/RandomCircuits/HaarTwoCopyTwirl
• Dependency: D5/S3/QuantumChannels/PauliThreeWeightBayesianInverseUniqueness