Fu-Luo decoherence convexity is refuted

Abstract

An explicit four-dimensional system with four qubit sub-environments violates the conjectured convexity of the Fu-Luo decoherence quantifier.

S. Fu and S. Luo, Quantifying Decoherence via Increases in Classicality, Entropy 23(12) (2021), 1594, Section 3. The source states verbatim: “We conjecture that D(ρ_S|Π, U) is convex in ρ. It seems that a proof may require some deep mathematics.” Equation (17) states “J(ρ,Π) = 1 + tr(√ρ Π†(√ρ)) = 1 + Σ_i 〈i|√ρ|i〉².” Equations (21)–(22) state “ρ′S = tr_E ρ′SE = Σ{i,j=1}^d tr(U{Ei} ρ_E U_{Ej}†) · Π_i ρ_S Π_j”, with “ρ_S ∘ Ω”, and Equation (27) states “D(ρ_S|Π, U) = J(ρ′_S, Π) − J(ρ_S, Π)”.

Definition 1.1 (The classicality functional J).

$$\forall d\in \mathbb{N},\forall rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),J\left(rho\right)=1+\sum _{i:\mathrm{Fin}\left(d\right)}\mathrm{Complex}.\mathrm{re}\left((\mathrm{CFC}.\mathrm{sqrt}\left(rho\right)\left(i,i\right){)}^2\right)$$

Formalization. D5/S3/Quantum/Decoherence/FuLuoDecoherenceConvexityRefutation.J (✓ std3).

Citation. S. Fu and S. Luo (2021). Quantifying Decoherence via Increases in Classicality. DOI: 10.3390/e23121594. URL: https://www.mdpi.com/1099-4300/23/12/1594.

Commentary.

Equation (17) states verbatim: “J(ρ,Π) = 1 + tr(√ρ Π†(√ρ)) = 1 + Σ_i 〈i|√ρ|i〉².” The encoding uses the standard basis of Fin d and takes the real part of each diagonal square.

Definition 1.2 (Environment basis labels).

$$\forall d\in \mathbb{N},\forall k\in \mathrm{Fin}\left(d\right)\to \mathbb{N},\mathrm{EnvIdx}\left(k\right)=((l:\mathrm{Fin}\left(d\right))\to \mathrm{Fin}\left(k\left(l\right)\right))$$

Formalization. D5/S3/Quantum/Decoherence/FuLuoDecoherenceConvexityRefutation.EnvIdx (✓ std3).

Citation. S. Fu and S. Luo (2021). Quantifying Decoherence via Increases in Classicality. DOI: 10.3390/e23121594. URL: https://www.mdpi.com/1099-4300/23/12/1594.

Commentary.

An environment basis label assigns to each part l a basis element of Fin (k l).

Definition 1.3 (A local environment operator).

$$\forall d\in \mathbb{N},\forall k\in \mathrm{Fin}\left(d\right)\to \mathbb{N},\forall i\in \mathrm{Fin}\left(d\right),\forall Ui\in \mathrm{Matrix}\left(\mathrm{Fin}\left(k\left(i\right)\right),\mathrm{Fin}\left(k\left(i\right)\right),\mathbb{C}\right),\mathrm{liftE}\left(i,Ui\right)=\lambda x:\mathrm{EnvIdx}\left(k\right),\lambda y:\mathrm{EnvIdx}\left(k\right),\mathrm{ite}\left((\forall l\in \mathrm{Fin}\left(d\right),(l\ne i)\Rightarrow (x\left(l\right)=y\left(l\right))),Ui\left(x\left(i\right)\right)\left(y\left(i\right)\right),0\right)$$

Formalization. D5/S3/Quantum/Decoherence/FuLuoDecoherenceConvexityRefutation.liftE (✓ std3).

Citation. S. Fu and S. Luo (2021). Quantifying Decoherence via Increases in Classicality. DOI: 10.3390/e23121594. URL: https://www.mdpi.com/1099-4300/23/12/1594.

Commentary.

The source describes U_{Ei} acting only on H_{Ei}. The encoding applies Ui at coordinate i and enforces equality at every other environment coordinate.

Definition 1.4 (The product environment state).

$$\forall d\in \mathbb{N},\forall k\in \mathrm{Fin}\left(d\right)\to \mathbb{N},\forall tau\in ((l:\mathrm{Fin}\left(d\right))\to \mathrm{DensityState}\left(\mathrm{Fin}\left(k\left(l\right)\right)\right)),\mathrm{rhoE}\left(tau\right)=\lambda x:\mathrm{EnvIdx}\left(k\right),\lambda y:\mathrm{EnvIdx}\left(k\right),\prod _{l:\mathrm{Fin}\left(d\right)}\mathrm{Subtype}.\mathrm{val}\left(tau\left(l\right)\right)\left(x\left(l\right)\right)\left(y\left(l\right)\right)$$

Formalization. D5/S3/Quantum/Decoherence/FuLuoDecoherenceConvexityRefutation.rhoE (✓ std3).

Citation. S. Fu and S. Luo (2021). Quantifying Decoherence via Increases in Classicality. DOI: 10.3390/e23121594. URL: https://www.mdpi.com/1099-4300/23/12/1594.

Commentary.

The source describes the initial state as ρ_SE = ρ_S ⊗ ρ_E with ρ_E = ρ_{E1} ⊗ ρ_{E2} ⊗ ⋯ ⊗ ρ_{Ed}. The encoding multiplies the corresponding entries of the component density states.

Definition 1.5 (The environment overlap matrix).

$$\forall d\in \mathbb{N},\forall k\in \mathrm{Fin}\left(d\right)\to \mathbb{N},\forall tau\in ((l:\mathrm{Fin}\left(d\right))\to \mathrm{DensityState}\left(\mathrm{Fin}\left(k\left(l\right)\right)\right)),\forall U\in ((l:\mathrm{Fin}\left(d\right))\to \mathrm{Matrix}.\mathrm{unitaryGroup}\left(\mathrm{Fin}\left(k\left(l\right)\right),\mathbb{C}\right)),\forall i\in \mathrm{Fin}\left(d\right),\forall j\in \mathrm{Fin}\left(d\right),\mathrm{omega}\left(tau,U,i,j\right)=\mathrm{Matrix}.\mathrm{trace}\left(((\mathrm{liftE}\left(i,\mathrm{val}\left(U\left(i\right)\right)\right))\cdot (\mathrm{rhoE}\left(tau\right)))\cdot (\mathrm{Matrix}.\mathrm{conjTranspose}\left(\mathrm{liftE}\left(j,\mathrm{val}\left(U\left(j\right)\right)\right)\right))\right)$$

Formalization. D5/S3/Quantum/Decoherence/FuLuoDecoherenceConvexityRefutation.omega (✓ std3).

Citation. S. Fu and S. Luo (2021). Quantifying Decoherence via Increases in Classicality. DOI: 10.3390/e23121594. URL: https://www.mdpi.com/1099-4300/23/12/1594.

Commentary.

Equation (21) states verbatim: “ρ′S = tr_E ρ′SE = Σ{i,j=1}^d tr(U{Ei} ρ_E U_{Ej}†) · Π_i ρ_S Π_j”. The overlap is the displayed trace factor.

Definition 1.6 (The final system state).

$$\forall d\in \mathbb{N},\forall k\in \mathrm{Fin}\left(d\right)\to \mathbb{N},\forall tau\in ((l:\mathrm{Fin}\left(d\right))\to \mathrm{DensityState}\left(\mathrm{Fin}\left(k\left(l\right)\right)\right)),\forall U\in ((l:\mathrm{Fin}\left(d\right))\to \mathrm{Matrix}.\mathrm{unitaryGroup}\left(\mathrm{Fin}\left(k\left(l\right)\right),\mathbb{C}\right)),\forall rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\mathrm{finalState}\left(tau,U,rho\right)=\lambda a:\mathrm{Fin}\left(d\right),\lambda b:\mathrm{Fin}\left(d\right),(rho\left(a,b\right))\cdot (\mathrm{omega}\left(tau,U,a,b\right))$$

Formalization. D5/S3/Quantum/Decoherence/FuLuoDecoherenceConvexityRefutation.finalState (✓ std3).

Citation. S. Fu and S. Luo (2021). Quantifying Decoherence via Increases in Classicality. DOI: 10.3390/e23121594. URL: https://www.mdpi.com/1099-4300/23/12/1594.

Commentary.

Equation (22) states verbatim that the reduced state is “ρ_S ∘ Ω”, where ∘ is the Hadamard product and Ω = (ω_ij). The encoding multiplies each entry by omega.

Definition 1.7 (The decoherence quantifier D).

$$\forall d\in \mathbb{N},\forall k\in \mathrm{Fin}\left(d\right)\to \mathbb{N},\forall tau\in ((l:\mathrm{Fin}\left(d\right))\to \mathrm{DensityState}\left(\mathrm{Fin}\left(k\left(l\right)\right)\right)),\forall U\in ((l:\mathrm{Fin}\left(d\right))\to \mathrm{Matrix}.\mathrm{unitaryGroup}\left(\mathrm{Fin}\left(k\left(l\right)\right),\mathbb{C}\right)),\forall rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),D\left(tau,U,rho\right)=J\left(\mathrm{finalState}\left(tau,U,rho\right)\right)-J\left(rho\right)$$

Formalization. D5/S3/Quantum/Decoherence/FuLuoDecoherenceConvexityRefutation.D (✓ std3).

Citation. S. Fu and S. Luo (2021). Quantifying Decoherence via Increases in Classicality. DOI: 10.3390/e23121594. URL: https://www.mdpi.com/1099-4300/23/12/1594.

Commentary.

Equation (27) states verbatim: “D(ρ_S|Π, U) = J(ρ′_S, Π) − J(ρ_S, Π)”. The encoding subtracts the initial classicality from the final classicality.

Definition 1.8 (The conjectured convexity statement).

$$(\mathrm{claim})\iff (\forall d\in \mathbb{N},\forall k\in \mathrm{Fin}\left(d\right)\to \mathbb{N},\forall tau\in ((l:\mathrm{Fin}\left(d\right))\to \mathrm{DensityState}\left(\mathrm{Fin}\left(k\left(l\right)\right)\right)),\forall U\in ((l:\mathrm{Fin}\left(d\right))\to \mathrm{Matrix}.\mathrm{unitaryGroup}\left(\mathrm{Fin}\left(k\left(l\right)\right),\mathbb{C}\right)),\forall rho\in \mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right),\forall sigma\in \mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right),\forall t\in \mathbb{R},(0\le t)\Rightarrow ((t\le 1)\Rightarrow (D\left(tau,U,\mathrm{Equiv}.\mathrm{symm}\left(\mathrm{CStarMatrix}.\mathrm{ofMatrix}\right)\left((t)\cdot (\mathrm{Subtype}.\mathrm{val}\left(rho\right))+(1-t)\cdot (\mathrm{Subtype}.\mathrm{val}\left(sigma\right))\right)\right)\le (t)\cdot (D\left(tau,U,\mathrm{Equiv}.\mathrm{symm}\left(\mathrm{CStarMatrix}.\mathrm{ofMatrix}\right)\left(\mathrm{Subtype}.\mathrm{val}\left(rho\right)\right)\right))+(1-t)\cdot (D\left(tau,U,\mathrm{Equiv}.\mathrm{symm}\left(\mathrm{CStarMatrix}.\mathrm{ofMatrix}\right)\left(\mathrm{Subtype}.\mathrm{val}\left(sigma\right)\right)\right)))))$$

Formalization. D5/S3/Quantum/Decoherence/FuLuoDecoherenceConvexityRefutation.claim (✓ std3).

Citation. S. Fu and S. Luo (2021). Quantifying Decoherence via Increases in Classicality. DOI: 10.3390/e23121594. URL: https://www.mdpi.com/1099-4300/23/12/1594.

Commentary.

The source states verbatim after Proposition 3: “We conjecture that D(rho_S|Pi, U) is convex in rho. It seems that a proof may require some deep mathematics.” The formal statement expands convexity as the Jensen inequality for every dimension, product environment, family of local unitaries, pair of density states, and t in [0,1].

Theorem 1.9 (An explicit violation in dimension four).

$$\neg (\forall d\in \mathbb{N},\forall k\in \mathrm{Fin}\left(d\right)\to \mathbb{N},\forall tau\in ((l:\mathrm{Fin}\left(d\right))\to \mathrm{DensityState}\left(\mathrm{Fin}\left(k\left(l\right)\right)\right)),\forall U\in ((l:\mathrm{Fin}\left(d\right))\to \mathrm{Matrix}.\mathrm{unitaryGroup}\left(\mathrm{Fin}\left(k\left(l\right)\right),\mathbb{C}\right)),\forall rho\in \mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right),\forall sigma\in \mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right),\forall t\in \mathbb{R},(0\le t)\Rightarrow ((t\le 1)\Rightarrow (D\left(tau,U,\mathrm{Equiv}.\mathrm{symm}\left(\mathrm{CStarMatrix}.\mathrm{ofMatrix}\right)\left((t)\cdot (\mathrm{Subtype}.\mathrm{val}\left(rho\right))+(1-t)\cdot (\mathrm{Subtype}.\mathrm{val}\left(sigma\right))\right)\right)\le (t)\cdot (D\left(tau,U,\mathrm{Equiv}.\mathrm{symm}\left(\mathrm{CStarMatrix}.\mathrm{ofMatrix}\right)\left(\mathrm{Subtype}.\mathrm{val}\left(rho\right)\right)\right))+(1-t)\cdot (D\left(tau,U,\mathrm{Equiv}.\mathrm{symm}\left(\mathrm{CStarMatrix}.\mathrm{ofMatrix}\right)\left(\mathrm{Subtype}.\mathrm{val}\left(sigma\right)\right)\right)))))$$

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

Resolves. Problems/fu-luo-decoherence-convexity (refuted) by D5/S3/Quantum/Decoherence/FuLuoDecoherenceConvexityRefutation.result.

Source. Repository-derived.

Acknowledgement. S. Fu and S. Luo (2021). Quantifying Decoherence via Increases in Classicality. DOI: 10.3390/e23121594. URL: https://www.mdpi.com/1099-4300/23/12/1594.

Commentary.

For four system coordinates, four qubit environments in the state |0><0|, and detector unitaries (X, X, Z, Z), the two explicit density states have D equal to 5/16 while their midpoint has D equal to 3/8. Thus the Jensen inequality in the expanded claim is false.

In the standard basis of Fin 4, the private definitions R false and R true are the two input matrices. The density states state false and state true use these matrices through CStarMatrix.ofMatrix. All entries below are real, regarded as complex numbers.

$$R\left(\mathrm{false}\right)=(\frac{1}{8})\cdot (\left(\begin{array}{cccc}1& 1& \sqrt{3}& \sqrt{3}\\ 1& 1& \sqrt{3}& \sqrt{3}\\ \sqrt{3}& \sqrt{3}& 3& 3\\ \sqrt{3}& \sqrt{3}& 3& 3\end{array}\right))$$

$$R\left(\mathrm{true}\right)=(\frac{1}{8})\cdot (\left(\begin{array}{cccc}1& -1& \sqrt{3}& -\sqrt{3}\\ -1& 1& -\sqrt{3}& \sqrt{3}\\ \sqrt{3}& -\sqrt{3}& 3& -3\\ -\sqrt{3}& \sqrt{3}& -3& 3\end{array}\right))$$

The private lemma mixture identifies their midpoint with M.

$$(\frac{1}{2})\cdot (R\left(\mathrm{false}\right))+(\frac{1}{2})\cdot (R\left(\mathrm{true}\right))=M$$

$$M=(\frac{1}{8})\cdot (\left(\begin{array}{cccc}1& 0& \sqrt{3}& 0\\ 0& 1& 0& \sqrt{3}\\ \sqrt{3}& 0& 3& 0\\ 0& \sqrt{3}& 0& 3\end{array}\right))$$

For the same tau and detectors, final_R and final_M give the output matrices B false, B true and BM.

$$\forall b\in \mathrm{Bool},\mathrm{finalState}\left(\mathrm{tau},\mathrm{detectors},R\left(b\right)\right)=B\left(b\right)$$

$$B\left(\mathrm{false}\right)=(\frac{1}{8})\cdot (\left(\begin{array}{cccc}1& 0& 0& 0\\ 0& 1& 0& 0\\ 0& 0& 3& 3\\ 0& 0& 3& 3\end{array}\right))$$

$$B\left(\mathrm{true}\right)=(\frac{1}{8})\cdot (\left(\begin{array}{cccc}1& 0& 0& 0\\ 0& 1& 0& 0\\ 0& 0& 3& -3\\ 0& 0& -3& 3\end{array}\right))$$

$$\mathrm{finalState}\left(\mathrm{tau},\mathrm{detectors},M\right)=\mathrm{BM}$$

$$\mathrm{BM}=(\frac{1}{8})\cdot (\left(\begin{array}{cccc}1& 0& 0& 0\\ 0& 1& 0& 0\\ 0& 0& 3& 0\\ 0& 0& 0& 3\end{array}\right))$$

The positive square-root certificates use R itself for each endpoint, SM for M, S for B, and SBM for BM. The private lemmas R_pos, SM_pos, S_pos and SBM_pos certify positive semidefiniteness; R_square, SM_square, S_square and SBM_square certify the squares. The lemmas sqrt_R, sqrt_M, sqrt_B and sqrt_BM identify these with CFC.sqrt.

$$\mathrm{SM}=(\frac{\sqrt{2}}{8})\cdot (\left(\begin{array}{cccc}1& 0& \sqrt{3}& 0\\ 0& 1& 0& \sqrt{3}\\ \sqrt{3}& 0& 3& 0\\ 0& \sqrt{3}& 0& 3\end{array}\right))$$

$$S\left(\mathrm{false}\right)=(\frac{1}{4})\cdot (\left(\begin{array}{cccc}\sqrt{2}& 0& 0& 0\\ 0& \sqrt{2}& 0& 0\\ 0& 0& \sqrt{3}& \sqrt{3}\\ 0& 0& \sqrt{3}& \sqrt{3}\end{array}\right))$$

$$S\left(\mathrm{true}\right)=(\frac{1}{4})\cdot (\left(\begin{array}{cccc}\sqrt{2}& 0& 0& 0\\ 0& \sqrt{2}& 0& 0\\ 0& 0& \sqrt{3}& -\sqrt{3}\\ 0& 0& -\sqrt{3}& \sqrt{3}\end{array}\right))$$

$$\mathrm{SBM}=(\frac{1}{4})\cdot (\left(\begin{array}{cccc}\sqrt{2}& 0& 0& 0\\ 0& \sqrt{2}& 0& 0\\ 0& 0& (\sqrt{2})\cdot (\sqrt{3})& 0\\ 0& 0& 0& (\sqrt{2})\cdot (\sqrt{3})\end{array}\right))$$

$$\forall b\in \mathrm{Bool},(\mathrm{CFC}.\mathrm{sqrt}\left(R\left(b\right)\right)=R\left(b\right))\wedge (\mathrm{Matrix}.\mathrm{PosSemidef}\left(R\left(b\right)\right)\wedge ((R\left(b\right))\cdot (R\left(b\right))=R\left(b\right)))$$

$$(\mathrm{CFC}.\mathrm{sqrt}\left(M\right)=\mathrm{SM})\wedge (\mathrm{Matrix}.\mathrm{PosSemidef}\left(\mathrm{SM}\right)\wedge ((\mathrm{SM})\cdot (\mathrm{SM})=M))$$

$$\forall b\in \mathrm{Bool},(\mathrm{CFC}.\mathrm{sqrt}\left(B\left(b\right)\right)=S\left(b\right))\wedge (\mathrm{Matrix}.\mathrm{PosSemidef}\left(S\left(b\right)\right)\wedge ((S\left(b\right))\cdot (S\left(b\right))=B\left(b\right)))$$

$$(\mathrm{CFC}.\mathrm{sqrt}\left(\mathrm{BM}\right)=\mathrm{SBM})\wedge (\mathrm{Matrix}.\mathrm{PosSemidef}\left(\mathrm{SBM}\right)\wedge ((\mathrm{SBM})\cdot (\mathrm{SBM})=\mathrm{BM}))$$

References

• Truth anchor: D5/S3/Quantum/Decoherence/FuLuoDecoherenceConvexityRefutation.D
• Truth anchor: D5/S3/Quantum/Decoherence/FuLuoDecoherenceConvexityRefutation.EnvIdx
• Truth anchor: D5/S3/Quantum/Decoherence/FuLuoDecoherenceConvexityRefutation.J
• Truth anchor: D5/S3/Quantum/Decoherence/FuLuoDecoherenceConvexityRefutation.claim
• Truth anchor: D5/S3/Quantum/Decoherence/FuLuoDecoherenceConvexityRefutation.finalState
• Truth anchor: D5/S3/Quantum/Decoherence/FuLuoDecoherenceConvexityRefutation.liftE
• Truth anchor: D5/S3/Quantum/Decoherence/FuLuoDecoherenceConvexityRefutation.omega
• Truth anchor: D5/S3/Quantum/Decoherence/FuLuoDecoherenceConvexityRefutation.result
• Truth anchor: D5/S3/Quantum/Decoherence/FuLuoDecoherenceConvexityRefutation.rhoE
• Dependency: D5/S3/Quantum/Reduction/ProbeComponentRigidity