Relative quantumness can increase under a commutativity-preserving channel

Abstract

A completely positive, trace-preserving qubit channel that preserves commuting density matrices increases relative quantumness at alpha zero. The exact trace arguments of the logarithms are 50401283/7340144 before the channel and 1879639/266240 afterwards.

Definition 1.1 (Density matrices).

$$\forall d:\mathbb{N},\forall A:{\mathbb{C}}^{d\times d},\mathrm{IsDensity}\left(A\right)\iff ((\mathrm{PSD}\left(A\right))\wedge (\mathrm{Tr}\left(A\right)=1))$$

Formalization. D5/S3/QuantumChannels/CoPRelativeQuantumnessRefutation.IsDensity (✓ std3).

Citation. A. Meunson; T. Deesuwan (2026). Cumulant-based quantum relative Rényi functional. DOI: 10.48550/arXiv.2606.31205. URL: https://arxiv.org/abs/2606.31205v1.

Commentary.

A density matrix on C^d is a positive semidefinite complex d by d matrix with trace one. PSD denotes Matrix.PosSemidef and Tr is the complex matrix trace.

Definition 1.2 (Regularization).

$$\forall d:\mathbb{N},\forall \epsilon :\mathbb{R},\forall A:{\mathbb{C}}^{d\times d},\mathrm{reg}\left(\epsilon ,A\right)=(1-\epsilon )\cdot A+\frac{\epsilon }{\mathrm{real}\left(d\right)}\cdot I$$

Formalization. D5/S3/QuantumChannels/CoPRelativeQuantumnessRefutation.reg (✓ std3).

Citation. A. Meunson; T. Deesuwan (2026). Cumulant-based quantum relative Rényi functional. DOI: 10.48550/arXiv.2606.31205. URL: https://arxiv.org/abs/2606.31205v1.

Commentary.

Given $\rho ,\sigma \in \mathcal{D}\left(\mathcal{H}\right)$ and a parameter $\epsilon \in (0,1)$, define ${\rho }_{\epsilon }:=(1-\epsilon )\rho +\epsilon \frac{\mathbb{I}}{d},{\sigma }_{\epsilon }:=(1-\epsilon )\sigma +\epsilon \frac{\mathbb{I}}{d}$, where $d=\dim \left(\mathcal{H}\right)$. Here d is a natural number, A is a complex d by d matrix, and epsilon is real. The division epsilon/d is real division after casting d to the reals; I is the identity matrix and scalar multiplication is by a real scalar. The conjecture uses 0 < epsilon < 1.

Definition 1.3 (Relative quantumness at alpha zero).

$$\forall d:\mathbb{N},\forall A:{\mathbb{C}}^{d\times d},\forall B:{\mathbb{C}}^{d\times d},Q\left(A,B\right)=-(\frac{1}{(0-1)}\cdot \ln \left(\mathrm{Re}\left(\mathrm{Tr}\left(A\cdot \exp \left((0-1)\cdot (\log \left(A\right)-\log \left(B\right))\right)\right)\right)\right))$$

Formalization. D5/S3/QuantumChannels/CoPRelativeQuantumnessRefutation.Q (✓ std3).

Citation. A. Meunson; T. Deesuwan (2026). Cumulant-based quantum relative Rényi functional. DOI: 10.48550/arXiv.2606.31205. URL: https://arxiv.org/abs/2606.31205v1.

Commentary.

Define $Q\left({\rho }_{\epsilon }\Vert {\sigma }_{\epsilon }\right):=-S_0^Q\left({\rho }_{\epsilon }\Vert {\sigma }_{\epsilon }\right)$. The expression displayed here is literally minus S_0^Q, with the source factor 1/(0-1) and exponent (0-1)(log A-log B). Log of a matrix means continuous functional calculus for the real logarithm in the L2 operator norm; exp is the matrix exponential. The scalar logarithm is applied to the real part of the complex trace. On the positive definite matrices used below that trace is the positive real number calculated explicitly.

Definition 1.4 (Completely positive trace-preserving maps).

$$\forall d:\mathbb{N},\forall N:\mathrm{MatrixMap}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\mathrm{IsCPTP}\left(N\right)\iff ((\mathrm{IsCompletelyPositive}\left(N\right))\wedge (\forall A:{\mathbb{C}}^{d\times d},\mathrm{Tr}\left(N\left(A\right)\right)=\mathrm{Tr}\left(A\right)))$$

Formalization. D5/S3/QuantumChannels/CoPRelativeQuantumnessRefutation.IsCPTP (✓ std3).

Citation. A. Meunson; T. Deesuwan (2026). Cumulant-based quantum relative Rényi functional. DOI: 10.48550/arXiv.2606.31205. URL: https://arxiv.org/abs/2606.31205v1.

Commentary.

MatrixMap(Fin(d), Fin(d), C) is the type of complex-linear maps between d by d complex matrices. IsCompletelyPositive is the existing matrix-map predicate: every amplification by an identity map preserves positive semidefiniteness. Trace preservation is quantified over all complex matrices A, without a density-matrix restriction.

Definition 1.5 (Preservation of commuting density matrices).

$$\forall d:\mathbb{N},\forall N:\mathrm{MatrixMap}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\mathrm{IsCoP}\left(N\right)\iff (\forall A:{\mathbb{C}}^{d\times d},\forall B:{\mathbb{C}}^{d\times d},(\mathrm{IsDensity}\left(A\right))\Rightarrow ((\mathrm{IsDensity}\left(B\right))\Rightarrow ((A\cdot B=B\cdot A)\Rightarrow (N\left(A\right)\cdot N\left(B\right)=N\left(B\right)\cdot N\left(A\right)))))$$

Formalization. D5/S3/QuantumChannels/CoPRelativeQuantumnessRefutation.IsCoP (✓ std3).

Citation. A. Meunson; T. Deesuwan (2026). Cumulant-based quantum relative Rényi functional. DOI: 10.48550/arXiv.2606.31205. URL: https://arxiv.org/abs/2606.31205v1.

Commentary.

Let $\mathcal{H}$ be a finite-dimensional Hilbert space. A CPTP map $\mathcal{N}:\mathcal{B}\left(\mathcal{H}\right)\to \mathcal{B}\left(\mathcal{H}\right)$ is called a CoP channel if, for every pair $(\rho ,\sigma )\in \mathcal{D}\left(\mathcal{H}\right)\times \mathcal{D}\left(\mathcal{H}\right)$ satisfying $[\rho ,\sigma ]=0$, one has $[\mathcal{N}\left(\rho \right),\mathcal{N}\left(\sigma \right)]=0$. (Section VIII.A, PDF p. 18.) The predicate IsCoP encodes the commuting-pair condition; the separate IsCPTP premise supplies the CPTP requirement in the quoted definition. Equality AB = BA encodes the vanishing commutator. Both A and B range over all complex d by d matrices and are required to be density matrices.

Definition 1.6 (Matrix support).

$$\forall d:\mathbb{N},\forall A:{\mathbb{C}}^{d\times d},\mathrm{supp}\left(A\right)=\mathrm{range}\left({\mathrm{toLin}}^{\prime }\left(A\right)\right)$$

Formalization. D5/S3/QuantumChannels/CoPRelativeQuantumnessRefutation.supp (✓ std3).

Citation. A. Meunson; T. Deesuwan (2026). Cumulant-based quantum relative Rényi functional. DOI: 10.48550/arXiv.2606.31205. URL: https://arxiv.org/abs/2606.31205v1.

Commentary.

The support of A is the range of the linear map Matrix.toLin’ A on C^d, with the standard coordinate basis. For Hermitian positive semidefinite matrices this is the usual operator support. Inclusion of supports is the submodule order, written as subset inclusion.

Definition 1.7 (Conjecture 15).

$$claim\iff (\forall d:\mathbb{N},\forall \rho :{\mathbb{C}}^{d\times d},\forall \sigma :{\mathbb{C}}^{d\times d},\forall \epsilon :\mathbb{R},\forall N:\mathrm{MatrixMap}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),(\mathrm{IsDensity}\left(\rho \right))\Rightarrow ((\mathrm{IsDensity}\left(\sigma \right))\Rightarrow ((\rho \cdot \sigma \ne \sigma \cdot \rho )\Rightarrow ((0<\epsilon )\Rightarrow ((\epsilon <1)\Rightarrow ((\mathrm{IsCPTP}\left(N\right))\Rightarrow ((\mathrm{IsCoP}\left(N\right))\Rightarrow ((\mathrm{supp}\left(N\left(\mathrm{reg}\left(\epsilon ,\rho \right)\right)\right)\subseteq \mathrm{supp}\left(N\left(\mathrm{reg}\left(\epsilon ,\sigma \right)\right)\right))\Rightarrow ((Q\left(N\left(\mathrm{reg}\left(\epsilon ,\rho \right)\right),N\left(\mathrm{reg}\left(\epsilon ,\sigma \right)\right)\right)\le Q\left(\mathrm{reg}\left(\epsilon ,\rho \right),\mathrm{reg}\left(\epsilon ,\sigma \right)\right))\wedge (0\le Q\left(N\left(\mathrm{reg}\left(\epsilon ,\rho \right)\right),N\left(\mathrm{reg}\left(\epsilon ,\sigma \right)\right)\right)))))))))))$$

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

Citation. A. Meunson; T. Deesuwan (2026). Cumulant-based quantum relative Rényi functional. DOI: 10.48550/arXiv.2606.31205. URL: https://arxiv.org/abs/2606.31205v1.

Commentary.

\begin{conjecture}[QDPI at $\alpha =0$ for non-commuting inputs under CoP channels] Let $(\rho ,\sigma )\in \mathcal{D}\left(\mathcal{H}\right)\times \mathcal{D}\left(\mathcal{H}\right)$ satisfy $[\rho ,\sigma ]\ne 0,$ where ${\rho }_{\epsilon },{\sigma }_{\epsilon }$ are the regularized states defined in Eq.\eqref{state_regularized}. Suppose that $\mathcal{N}$ is a CoP channel satisfying $\mathrm{supp}\left(\mathcal{N}\left({\rho }_{\epsilon }\right)\right)\subseteq \mathrm{supp}\left(\mathcal{N}\left({\sigma }_{\epsilon }\right)\right).$ Then, \begin{equation} $Q\left({\rho }_{\epsilon }\Vert {\sigma }_{\epsilon }\right)\ge Q\left(\mathcal{N}\left({\rho }_{\epsilon }\right)\Vert \mathcal{N}\left({\sigma }_{\epsilon }\right)\right)\ge 0.$ \end{equation} \end{conjecture} (Conjecture 15, Section VIII.A, PDF p. 18.) Here H is C^d for arbitrary natural d; rho and sigma are density matrices; epsilon is real with 0 < epsilon < 1; and N is a complex-linear map satisfying IsCPTP and IsCoP. The source nonzero commutator is rho sigma and sigma rho differ. Rho_epsilon and sigma_epsilon are reg(epsilon,rho) and reg(epsilon,sigma). Support inclusion is inclusion of their output ranges. The two conclusion inequalities are encoded as Q(output rho,output sigma) <= Q(input rho,input sigma) and 0 <= Q(output rho,output sigma). The displayed pair normalizes the source typo. Verbatim malformed source fragment: \rho,\sigma)\in \mathcal D(\mathcal H)\times\mathcal D(\mathcal H).

Theorem 1.8 (A qubit refutation).

$$\neg claim$$

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

Resolves. Problems/meunson-deesuwan-2026-cop-relative-quantumness-refutation (refuted) by D5/S3/QuantumChannels/CoPRelativeQuantumnessRefutation.result.

Source. Repository-derived.

Acknowledgement. A. Meunson; T. Deesuwan (2026). Cumulant-based quantum relative Rényi functional. DOI: 10.48550/arXiv.2606.31205. URL: https://arxiv.org/abs/2606.31205v1.

Commentary.

Put t_n = (4^n-1)/(4^n+1), R = (I+t_7 Z)/2, S = (I+t_8 H)/2, R’ = (I+t_6 Z)/2 and S’ = (I+t_3 J)/2, where X and Z are Pauli matrices, H = (11 Z+5 sqrt(3) X)/14 and J = (29 Z+sqrt(455) X)/36. Set epsilon = 1/65537 and recover rho and sigma from R and S by undoing regularization. The unital channel has N(X) = u X+v Z, N(Y) = u w Y and N(Z) = w Z, with u = (3211313/127793250) sqrt(1365), v = -(727356123473/168188824118250) sqrt(3), w = 22365525/22373717. Four explicit Kraus operators realize the channel: reshape the vectors bp(v/a), ep, bm(v/b), em in output-input index order and scale them by sqrt(a/4), sqrt(delta/(4a)), sqrt(b/4), sqrt(delta/(4b)), where a=(1+u)(1+w), b=(1-u)(1+w) and delta=(1-u^2)(1-w^2)-v^2. Entrywise equality to the Kraus sum proves complete positivity using the frozen Kraus-channel theorem; its trace is preserved on every input. Entrywise commutator identities show preservation of every commuting pair. The inputs are noncommuting density matrices, and both outputs are positive definite, so the support inclusion holds. Two-point functional calculus for self-adjoint involutions gives Tr[R exp(log S-log R)] = 50401283/7340144 < 1879639/266240 = Tr[R’ exp(log S’-log R’)]. Strict monotonicity of the real logarithm contradicts the first inequality of Conjecture 15.

References

• Truth anchor: D5/S3/QuantumChannels/CoPRelativeQuantumnessRefutation.IsCPTP
• Truth anchor: D5/S3/QuantumChannels/CoPRelativeQuantumnessRefutation.IsCoP
• Truth anchor: D5/S3/QuantumChannels/CoPRelativeQuantumnessRefutation.IsDensity
• Truth anchor: D5/S3/QuantumChannels/CoPRelativeQuantumnessRefutation.Q
• Truth anchor: D5/S3/QuantumChannels/CoPRelativeQuantumnessRefutation.claim
• Truth anchor: D5/S3/QuantumChannels/CoPRelativeQuantumnessRefutation.reg
• Truth anchor: D5/S3/QuantumChannels/CoPRelativeQuantumnessRefutation.result
• Truth anchor: D5/S3/QuantumChannels/CoPRelativeQuantumnessRefutation.supp
• Dependency: D5/S3/Quantum/Foundation/FiniteKrausChannel