Refutation of completely contractive CMI data processing

Abstract

A dephasing-plus-shift channel has only scalar correctable observables on the whole input space, yet preserves positive conditional mutual information for a singular input state.

Definition 1.1 (The whole-space correctable algebra).

$$\forall a\in \mathrm{Type},\forall b\in \mathrm{Type},[\mathrm{Fintype}\left(a\right)][\mathrm{DecidableEq}\left(a\right)][\mathrm{Fintype}\left(b\right)]\forall iota\in \mathrm{Type},\forall K\in iota\to \mathrm{Matrix}\left(b,a,\mathbb{C}\right),\mathrm{correctable}\left(K\right)=Algebra.adjoin\left(\mathbb{C},\{O:\mathrm{Matrix}\left(a,a,\mathbb{C}\right)\mid \forall i\in iota,\forall j\in iota,\mathrm{Commute}\left(O,\mathrm{conjTranspose}\left(K\left(i\right)\right)\cdot K\left(j\right)\right)\}\right)$$

Formalization. D5/S3/Quantum/Information/ChenKatoBrandaoCMIRefutation.correctable (✓ 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.

Section II.D, PDF p. 11, equation (22), verbatim: “For a given channel ℰ: A → A′, we define the correctable algebra 𝒜(ℰ) ⊂ ℬ(ℋ_A) as 𝒜(ℰ) := Alg{O_A | [O_A, E_a† E_b] = 0, ∀a,b}.” The Kraus family K has output rows b and input columns a. Algebra.adjoin takes the complex algebra generated by the entire commutant on the input space; the bottom Subalgebra consists of scalar multiples of the identity. Commute is the equality of the two multiplication orders, hence the zero-commutator condition. The index type iota need not itself be finite in this definition.

Definition 1.2 (Eigenvalue entropy, including zero eigenvalues).

$$\forall a\in \mathrm{Type},[\mathrm{Fintype}\left(a\right)][\mathrm{DecidableEq}\left(a\right)]\forall M\in \mathrm{Matrix}\left(a,a,\mathbb{C}\right),\mathrm{entropy}\left(M\right)=\mathrm{if}h:Matrix.IsHermitian\left(M\right)\mathrm{then}\sum _{i:a}(Real.negMulLog\left(Matrix.IsHermitian.eigenvalues\left(h,i\right)\right))\mathrm{else}0$$

Formalization. D5/S3/Quantum/Information/ChenKatoBrandaoCMIRefutation.entropy (✓ 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.

Section I, PDF p. 3, equation (1): “where S(A)_ρ = -tr ρ_A log₂ ρ_A is the von Neumann entropy of the reduced state on A.” The eigenvalue expression is the finite spectral form of this definition. Real.negMulLog(t) is -t log(t), including value zero at t = 0. The definition extends by zero off Hermitian matrices; density matrices and their marginals use only its Hermitian branch. All logarithms in the encoding are natural. Changing from the source’s base two divides all four entropy terms by the same positive log(2), so preserves the equality and every proposed contraction inequality.

Definition 1.3 (Literal conditional mutual information).

$$\forall A\in \mathrm{Type},\forall B\in \mathrm{Type},\forall C\in \mathrm{Type},[\mathrm{Fintype}\left(A\right)][\mathrm{DecidableEq}\left(A\right)][\mathrm{Fintype}\left(B\right)][\mathrm{DecidableEq}\left(B\right)][\mathrm{Fintype}\left(C\right)][\mathrm{DecidableEq}\left(C\right)]\forall M\in \mathrm{Matrix}\left(((A\times B)\times C),((A\times B)\times C),\mathbb{C}\right),\mathrm{let}R:(A\times (B\times C))\to ((A\times B)\times C):=\mathrm{fun}(x:(A\times (B\times C)))\mapsto ((Prod.fst\left(x\right),Prod.fst\left(Prod.snd\left(x\right)\right)),Prod.snd\left(Prod.snd\left(x\right)\right)),\mathrm{let}N:\mathrm{Matrix}\left((A\times (B\times C)),(A\times (B\times C)),\mathbb{C}\right):=Matrix.submatrix\left(M,R,R\right),\mathrm{cmi}\left(M\right)=\mathrm{entropy}\left(\mathrm{partialTraceRight}\left(M\right)\right)+\mathrm{entropy}\left(\mathrm{partialTraceLeft}\left(N\right)\right)-\mathrm{entropy}\left(\mathrm{partialTraceRight}\left(\mathrm{partialTraceLeft}\left(N\right)\right)\right)-\mathrm{entropy}\left(M\right)$$

Formalization. D5/S3/Quantum/Information/ChenKatoBrandaoCMIRefutation.cmi (✓ 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.

Section I, PDF p. 3, equation (1), verbatim: “The CMI I(A:C|B)_ρ is a function defined for a tripartite state ρ_ABC as I(A:C|B)_ρ = S(AB)_ρ + S(BC)_ρ - S(B)_ρ - S(ABC)_ρ.” The input order is (A times B) times C. The local let-bound map R only reassociates indices; N is the literal submatrix with R in both positions. partialTraceRight traces the right factor and partialTraceLeft the left factor. Thus the displayed four terms are precisely the AB, BC, B and ABC entropies, with no rank assumption.

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

$$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{correctable}\left(K\right)=\perp )\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),\mathrm{cmi}\left(\mathrm{ofKraus}\left(L,L,CStarMatrix.ofMatrix.symm\left(\mathrm{val}\left(rho\right)\right)\right)\right)\le eta\cdot \mathrm{cmi}\left(CStarMatrix.ofMatrix.symm\left(\mathrm{val}\left(rho\right)\right)\right)))))$$

Formalization. D5/S3/Quantum/Information/ChenKatoBrandaoCMIRefutation.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.

Section III.C, PDF p. 16, Conjecture III.1, verbatim: “For any channel ℰ: C → C′ with trivial correctable algebra 𝒜(ℰ) = ℂ I, there exists a constant η < 1 such that for any tripartite system ABC and any state ρ_ABC, it holds that I(A:C′|B)_ℰ(ρ) ≤ η I(A:C|B)_ρ.” The dimensions n, nPrime, dA and dB range over all natural numbers; Fin gives zero-based coordinates. The finite Kraus index type iota and family K are arbitrary. Normalization is the literal sum of K adjoint times K. DensityState is the existing carrier of positive semidefinite trace-one matrices and permits singular states. The let-bound L is I_AB kronecker K. ofKraus is the landed spelling for FiniteKrausChannel.PhyslibLeaf.MatrixMap.of_kraus: ofKraus(L,L,X) is literally the sum of L_i X L_i adjoint. CStarMatrix.ofMatrix.symm(val(rho)) exposes the same density matrix in Matrix coordinates. The strict upper bound eta < 1 is uniform over all ancillary dimensions and states for the fixed channel.

Theorem 1.5 (A four-dimensional channel refutes the conjecture).

$$\neg claim$$

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

Resolves. Problems/chen-kato-brandao-2020-completely-contractive-cmi (refuted) by D5/S3/Quantum/Information/ChenKatoBrandaoCMIRefutation.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.

For 0 < p < 1, take Kraus matrices K_(j,false) = sqrt(1-p) Matrix.single(j,j,1) and K_(j,true) = sqrt(p) Matrix.single(j+1,j,1), with cyclic Fin(n) addition. Their adjoint products include nonzero multiples of every diagonal matrix unit, forcing a commuting matrix to be diagonal. The adjacent cross-products force consecutive diagonal entries to agree; induction makes the whole matrix scalar. Specialize to n = 4 and p = 1/2. With dA = 2 and dB = 1, the input diagonal has weight 1/2 at ((0,0),0) and ((1,0),2), and zero elsewhere. The output has weight 1/4 at ((0,0),0), ((0,0),1), ((1,0),2) and ((1,0),3). The two conditional mutual informations are exactly log(2) > 0. Substitution into the asserted inequality gives log(2) <= eta log(2), contradicting eta < 1. The bit survives because the two selected inputs have disjoint output supports, although all globally correctable observables are scalar.

References

• Truth anchor: D5/S3/Quantum/Information/ChenKatoBrandaoCMIRefutation.claim
• Truth anchor: D5/S3/Quantum/Information/ChenKatoBrandaoCMIRefutation.cmi
• Truth anchor: D5/S3/Quantum/Information/ChenKatoBrandaoCMIRefutation.correctable
• Truth anchor: D5/S3/Quantum/Information/ChenKatoBrandaoCMIRefutation.entropy
• Truth anchor: D5/S3/Quantum/Information/ChenKatoBrandaoCMIRefutation.result
• Dependency: D5/S3/Quantum/Foundation/FiniteKrausChannel
• Dependency: D5/S3/Quantum/Information/PartialTraceMutualInformation