Trace-norm CMI contraction conjecture

Abstract

A flagged measurement in two qubit bases strictly contracts local trace distance while preserving the trace-norm conditional mutual information of a tripartite state.

Definition 1.1 (Local trace-norm contraction ratio).

$$\forall n\in \mathbb{N},\forall nPrime\in \mathbb{N},\forall iota\in \mathrm{Type},[\mathrm{Fintype}\left(iota\right)]\forall K\in iota\to \mathrm{Matrix}\left(\mathrm{Fin}\left(nPrime\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),\mathrm{localContraction}\left(K\right)=\mathrm{sSup}\left(\{r:\mathbb{R}\mid \exists rho\in \mathrm{DensityState}\left(\mathrm{Fin}\left(n\right)\right),\exists rhoPrime\in \mathrm{DensityState}\left(\mathrm{Fin}\left(n\right)\right),(\neg rho=rhoPrime)\wedge (r=\frac{\mathrm{traceNorm}\left(\mathrm{ofKraus}\left(K,K,CStarMatrix.ofMatrix.symm\left(\mathrm{val}\left(rho\right)\right)\right)-\mathrm{ofKraus}\left(K,K,CStarMatrix.ofMatrix.symm\left(\mathrm{val}\left(rhoPrime\right)\right)\right)\right)}{\mathrm{traceNorm}\left(CStarMatrix.ofMatrix.symm\left(\mathrm{val}\left(rho\right)\right)-CStarMatrix.ofMatrix.symm\left(\mathrm{val}\left(rhoPrime\right)\right)\right)})\}\right)$$

Formalization. D5/S3/Quantum/Information/ChenKatoBrandaoTraceNormCMIRefutation.localContraction (✓ std3).

Citation. Chi-Fang Chen, Kohtaro Kato and Fernando G. S. L. Brandão (2020). Matrix Product Density Operators: when do they have a local parent Hamiltonian?. URL: https://arxiv.org/abs/2010.14682v3.

Commentary.

Conjecture III.2, PDF p. 17: the local contraction ratio is the supremum of the trace-norm output difference divided by the trace-norm input difference. The two input DensityState values are distinct. Their underlying matrices are exposed by CStarMatrix.ofMatrix.symm. ofKraus(K,K,X) denotes FiniteKrausChannel.PhyslibLeaf.MatrixMap.of_kraus applied to K, K and X, namely the sum of K_i X K_i adjoint. The definition uses the repository traceNorm and the real supremum sSup.

Definition 1.2 (Trace-norm conditional mutual information).

$$\forall dA\in \mathbb{N},\forall dB\in \mathbb{N},\forall n\in \mathbb{N},\forall M\in \mathrm{Matrix}\left(((\mathrm{Fin}\left(dA\right)\times \mathrm{Fin}\left(dB\right))\times \mathrm{Fin}\left(n\right)),((\mathrm{Fin}\left(dA\right)\times \mathrm{Fin}\left(dB\right))\times \mathrm{Fin}\left(n\right)),\mathbb{C}\right),\mathrm{let}R:(\mathrm{Fin}\left(dA\right)\times (\mathrm{Fin}\left(dB\right)\times \mathrm{Fin}\left(n\right)))\to ((\mathrm{Fin}\left(dA\right)\times \mathrm{Fin}\left(dB\right))\times \mathrm{Fin}\left(n\right)):=\mathrm{fun}(p:(\mathrm{Fin}\left(dA\right)\times (\mathrm{Fin}\left(dB\right)\times \mathrm{Fin}\left(n\right))))\mapsto ((Prod.fst\left(p\right),Prod.fst\left(Prod.snd\left(p\right)\right)),Prod.snd\left(Prod.snd\left(p\right)\right)),\mathrm{let}S:((\mathrm{Fin}\left(dA\right)\times \mathrm{Fin}\left(dB\right))\times \mathrm{Fin}\left(n\right))\to (\mathrm{Fin}\left(dA\right)\times (\mathrm{Fin}\left(dB\right)\times \mathrm{Fin}\left(n\right))):=\mathrm{fun}(p:((\mathrm{Fin}\left(dA\right)\times \mathrm{Fin}\left(dB\right))\times \mathrm{Fin}\left(n\right)))\mapsto (Prod.fst\left(Prod.fst\left(p\right)\right),(Prod.snd\left(Prod.fst\left(p\right)\right),Prod.snd\left(p\right))),\mathrm{let}AB:\mathrm{Matrix}\left((\mathrm{Fin}\left(dA\right)\times \mathrm{Fin}\left(dB\right)),(\mathrm{Fin}\left(dA\right)\times \mathrm{Fin}\left(dB\right)),\mathbb{C}\right):=\mathrm{partialTraceRight}\left(M\right),\mathrm{let}A:\mathrm{Matrix}\left(\mathrm{Fin}\left(dA\right),\mathrm{Fin}\left(dA\right),\mathbb{C}\right):=\mathrm{partialTraceRight}\left(AB\right),\mathrm{let}B:\mathrm{Matrix}\left(\mathrm{Fin}\left(dB\right),\mathrm{Fin}\left(dB\right),\mathbb{C}\right):=\mathrm{partialTraceLeft}\left(AB\right),\mathrm{let}BC:\mathrm{Matrix}\left((\mathrm{Fin}\left(dB\right)\times \mathrm{Fin}\left(n\right)),(\mathrm{Fin}\left(dB\right)\times \mathrm{Fin}\left(n\right)),\mathbb{C}\right):=\mathrm{partialTraceLeft}\left(Matrix.submatrix\left(M,R,R\right)\right),I1\left(M\right)=\mathrm{traceNorm}\left(M-Matrix.submatrix\left(Matrix.kronecker\left(A,BC\right),S,S\right)\right)-\mathrm{traceNorm}\left(AB-Matrix.kronecker\left(A,B\right)\right)$$

Formalization. D5/S3/Quantum/Information/ChenKatoBrandaoTraceNormCMIRefutation.I1 (✓ std3).

Citation. Chi-Fang Chen, Kohtaro Kato and Fernando G. S. L. Brandão (2020). Matrix Product Density Operators: when do they have a local parent Hamiltonian?. URL: https://arxiv.org/abs/2010.14682v3.

Commentary.

Definition 2, PDF p. 14, verbatim: I_1(A:C|B) := ||rho_ABC - rho_A tensor rho_BC||_1 - ||rho_AB - rho_A tensor rho_B||_1. The input coordinates are (A times B) times C. partialTraceRight traces the right factor; partialTraceLeft traces the left factor. The maps R and S reassociate the product indices in opposite directions. AB, A, B and BC are the literal reduced matrices. The tensor product A tensor BC is reassociated back to the input coordinates before subtraction. No rank condition is imposed.

Theorem 1.3 (Trace norm of a real diagonal matrix).

$$\forall n\in \mathrm{Type},[\mathrm{Fintype}\left(n\right)][\mathrm{DecidableEq}\left(n\right)]\forall d\in n\to \mathbb{R},Complex.re\left(Matrix.trace\left(CFC.sqrt\left(Matrix.conjTranspose\left(Matrix.diagonal\left(\mathrm{fun}(i:n)\mapsto Complex.ofReal\left(d\left(i\right)\right)\right)\right)\cdot Matrix.diagonal\left(\mathrm{fun}(i:n)\mapsto Complex.ofReal\left(d\left(i\right)\right)\right)\right)\right)\right)=\sum _{i:n}(|d\left(i\right)|)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Information/ChenKatoBrandaoTraceNormCMIRefutation.diagonal_norm (✓ std3). ∎

Source. Repository-derived.

Commentary.

The trace norm of a complex diagonal matrix with real entries is the sum of their absolute values. The positive square root of its adjoint product is diagonal with entries equal to those absolute values. The index type is any finite type with decidable equality, including the empty type.

Definition 1.4 (Chen–Kato–Brandão Conjecture III.2).

$$claim\iff (\forall n\in \mathbb{N},\forall nPrime\in \mathbb{N},\forall iota\in \mathrm{Type},[\mathrm{Fintype}\left(iota\right)]\forall K\in iota\to \mathrm{Matrix}\left(\mathrm{Fin}\left(nPrime\right),\mathrm{Fin}\left(n\right),\mathbb{C}\right),(\sum _{i:iota}(\mathrm{conjTranspose}\left(K\left(i\right)\right)\cdot K\left(i\right))=1)\Rightarrow ((\mathrm{localContraction}\left(K\right)<1)\Rightarrow (\exists eta\in \mathbb{R},(eta<1)\wedge (\forall dA\in \mathbb{N},\forall dB\in \mathbb{N},\forall rho\in \mathrm{DensityState}\left(((\mathrm{Fin}\left(dA\right)\times \mathrm{Fin}\left(dB\right))\times \mathrm{Fin}\left(n\right))\right),\mathrm{let}L:iota\to \mathrm{Matrix}\left(((\mathrm{Fin}\left(dA\right)\times \mathrm{Fin}\left(dB\right))\times \mathrm{Fin}\left(nPrime\right)),((\mathrm{Fin}\left(dA\right)\times \mathrm{Fin}\left(dB\right))\times \mathrm{Fin}\left(n\right)),\mathbb{C}\right):=\mathrm{fun}(i:iota)\mapsto Matrix.kronecker\left((1:\mathrm{Matrix}\left((\mathrm{Fin}\left(dA\right)\times \mathrm{Fin}\left(dB\right)),(\mathrm{Fin}\left(dA\right)\times \mathrm{Fin}\left(dB\right)),\mathbb{C}\right)),K\left(i\right)\right),I1\left(\mathrm{ofKraus}\left(L,L,CStarMatrix.ofMatrix.symm\left(\mathrm{val}\left(rho\right)\right)\right)\right)\le eta\cdot I1\left(CStarMatrix.ofMatrix.symm\left(\mathrm{val}\left(rho\right)\right)\right)))))$$

Formalization. D5/S3/Quantum/Information/ChenKatoBrandaoTraceNormCMIRefutation.claim (✓ std3).

Citation. Chi-Fang Chen, Kohtaro Kato and Fernando G. S. L. Brandão (2020). Matrix Product Density Operators: when do they have a local parent Hamiltonian?. URL: https://arxiv.org/abs/2010.14682v3.

Commentary.

Conjecture III.2, PDF p. 17, verbatim: For any channel E: C to CPrime with local contraction ratio eta_1,C < 1, there exists a global constant eta < 1 such that for any tripartite system ABC and any state rho_ABC, I_1(A:CPrime|B)_E(rho) <= eta I_1(A:C|B)_rho. All dimensions range over natural numbers. The finite Kraus family is arbitrary and its completeness equation is the channel hypothesis. L_i is the literal identity on AB kronecker K_i, and the bound applies uniformly to every DensityState on the input product carrier, including singular states.

Theorem 1.5 (A flagged qubit measurement refutes the conjecture).

$$\neg claim$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Information/ChenKatoBrandaoTraceNormCMIRefutation.result (✓ std3). ∎

Resolves. Problems/chen-kato-brandao-2020-trace-norm-cmi-contraction (refuted) by D5/S3/Quantum/Information/ChenKatoBrandaoTraceNormCMIRefutation.result.

Source. Repository-derived.

Acknowledgement. Chi-Fang Chen, Kohtaro Kato and Fernando G. S. L. Brandão (2020). Matrix Product Density Operators: when do they have a local parent Hamiltonian?. URL: https://arxiv.org/abs/2010.14682v3.

Commentary.

Take the channel from a qubit to four classical outcomes that measures the computational basis with probability 1/2 and the plus-minus basis with probability 1/2, recording both the basis and the outcome. Its local trace-norm contraction ratio is at most 1/sqrt(2), strictly less than one. Let A and B be qubits and let the input state be the equal mixture of the Bell state phi-plus on BC flagged by A = 0 and the Bell state psi-minus on BC flagged by A = 1. The AB marginal is the identity divided by four, so the second trace-norm term vanishes both before and after the channel. The input trace-norm conditional mutual information equals one. The centered output is Hermitian and its square is the identity divided by 256; multiplying it by 16 gives a unitary whose real trace pairing with the centered output is one. Thus the output trace-norm conditional mutual information is at least one. The asserted uniform bound would force 1 <= eta for eta < 1, a contradiction.

References

• Truth anchor: D5/S3/Quantum/Information/ChenKatoBrandaoTraceNormCMIRefutation.I1
• Truth anchor: D5/S3/Quantum/Information/ChenKatoBrandaoTraceNormCMIRefutation.claim
• Truth anchor: D5/S3/Quantum/Information/ChenKatoBrandaoTraceNormCMIRefutation.diagonal_norm
• Truth anchor: D5/S3/Quantum/Information/ChenKatoBrandaoTraceNormCMIRefutation.localContraction
• Truth anchor: D5/S3/Quantum/Information/ChenKatoBrandaoTraceNormCMIRefutation.result
• Dependency: D5/S3/Quantum/Foundation/FiniteKrausChannel
• Dependency: D5/S3/Quantum/Foundation/FiniteTraceDistance
• Dependency: D5/S3/Quantum/Information/PartialTraceMutualInformation