The kernel and trace criteria are not equivalent

Abstract

The kernel criterion for optimality of entanglement witnesses does not imply the trace criterion.

The dimensions m and n are arbitrary natural numbers. Fin m and Fin n index the two factors, and all matrices and vectors have complex entries. A product vector has coordinate x(p.1)y(p.2). star denotes complex conjugation, dotProduct is the bilinear coordinate sum, mulVec is matrix action, and kronecker is the Kronecker product of matrices. Complex nonnegativity requires a nonnegative real part and zero imaginary part. toLp places a coordinate vector in EuclideanSpace with its standard inner product. The Lean names trTwo and trOne have notation tr₂ and tr₁, respectively. ofReal and natCastComplex display the scalar embeddings used in Lean.

Definition 1.1 (Block positivity).

$$\forall m\in Nat,\forall n\in Nat,\forall W\in \mathrm{Matrix}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\right),\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\right),Complex\right),(\mathrm{blockPositive}\left(W\right))\iff (\forall x\in \mathrm{Fin}\left(m\right)\to Complex,\forall y\in \mathrm{Fin}\left(n\right)\to Complex,0\le \mathrm{dotProduct}\left(\mathrm{star}\left((\lambda p:\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\right),x\left(\mathrm{fst}\left(p\right)\right)\cdot y\left(\mathrm{snd}\left(p\right)\right))\right),\mathrm{mulVec}\left(W,(\lambda p:\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\right),x\left(\mathrm{fst}\left(p\right)\right)\cdot y\left(\mathrm{snd}\left(p\right)\right))\right)\right))$$

Formalization. D5/S3/Quantum/Entanglement/WitnessKernelTraceCriteriaRefutation.blockPositive (✓ std3).

Citation. Frederik vom Ende and Simon Cichy (2025). Simple Sufficient Criteria for Optimality of Entanglement Witnesses. URL: https://arxiv.org/abs/2505.15615v2.

Commentary.

Section II B requires a nonnegative complex expectation on every product vector, without normalization assumptions on either factor.

Definition 1.2 (Entanglement witnesses).

$$\forall m\in Nat,\forall n\in Nat,\forall W\in \mathrm{Matrix}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\right),\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\right),Complex\right),(\mathrm{IsWitness}\left(W\right))\iff ((\mathrm{blockPositive}\left(W\right))\wedge (\exists sigma\in \mathrm{Matrix}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\right),\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\right),Complex\right),(\mathrm{PosSemidef}\left(sigma\right))\wedge (\mathrm{trace}\left(W\cdot sigma\right)<0)))$$

Formalization. D5/S3/Quantum/Entanglement/WitnessKernelTraceCriteriaRefutation.IsWitness (✓ std3).

Citation. Frederik vom Ende and Simon Cichy (2025). Simple Sufficient Criteria for Optimality of Entanglement Witnesses. URL: https://arxiv.org/abs/2505.15615v2.

Commentary.

A block-positive matrix is a witness when some positive semidefinite matrix sigma satisfies the strict negative trace inequality tr(W sigma) < 0.

Definition 1.3 (Trace over the second factor).

$$\forall m\in Nat,\forall n\in Nat,\forall W\in \mathrm{Matrix}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\right),\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\right),Complex\right),\forall i\in \mathrm{Fin}\left(m\right),\forall k\in \mathrm{Fin}\left(m\right),\mathrm{trTwo}\left(W\right)\left(i,k\right)=\sum _{j:\mathrm{Fin}\left(n\right)}(W\left(\mathrm{pair}\left(i,j\right),\mathrm{pair}\left(k,j\right)\right))$$

Formalization. D5/S3/Quantum/Entanglement/WitnessKernelTraceCriteriaRefutation.trTwo (✓ std3).

Citation. Frederik vom Ende and Simon Cichy (2025). Simple Sufficient Criteria for Optimality of Entanglement Witnesses. URL: https://arxiv.org/abs/2505.15615v2.

Commentary.

trTwo is the existing partialTraceRight: sum over the repeated second index while retaining the first factor.

Definition 1.4 (Trace over the first factor).

$$\forall m\in Nat,\forall n\in Nat,\forall W\in \mathrm{Matrix}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\right),\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\right),Complex\right),\forall j\in \mathrm{Fin}\left(n\right),\forall l\in \mathrm{Fin}\left(n\right),\mathrm{trOne}\left(W\right)\left(j,l\right)=\sum _{i:\mathrm{Fin}\left(m\right)}(W\left(\mathrm{pair}\left(i,j\right),\mathrm{pair}\left(i,l\right)\right))$$

Formalization. D5/S3/Quantum/Entanglement/WitnessKernelTraceCriteriaRefutation.trOne (✓ std3).

Citation. Frederik vom Ende and Simon Cichy (2025). Simple Sufficient Criteria for Optimality of Entanglement Witnesses. URL: https://arxiv.org/abs/2505.15615v2.

Commentary.

trOne is the existing partialTraceLeft: sum over the repeated first index while retaining the second factor.

Definition 1.5 (Schmidt rank).

$$\forall m\in Nat,\forall n\in Nat,\forall v\in \mathrm{Prod}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\right)\to Complex,\mathrm{schmidtRank}\left(v\right)=\mathrm{rank}\left(\mathrm{of}\left((\lambda i:\mathrm{Fin}\left(m\right),\lambda j:\mathrm{Fin}\left(n\right),v\left(\mathrm{pair}\left(i,j\right)\right))\right)\right)$$

Formalization. D5/S3/Quantum/Entanglement/WitnessKernelTraceCriteriaRefutation.schmidtRank (✓ std3).

Citation. Frederik vom Ende and Simon Cichy (2025). Simple Sufficient Criteria for Optimality of Entanglement Witnesses. URL: https://arxiv.org/abs/2505.15615v2.

Commentary.

Remark 3(i) defines Schmidt rank as the rank of the vector’s coefficient matrix.

Definition 1.6 (The kernel criterion).

$$\forall m\in Nat,\forall n\in Nat,\forall W\in \mathrm{Matrix}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\right),\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\right),Complex\right),(\mathrm{kernelCriterion}\left(W\right))\iff (((m\le n)\wedge (\exists v\in \mathrm{Prod}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\right)\to Complex,(\mathrm{mulVec}\left((W+\mathrm{kronecker}\left(\mathrm{trTwo}\left(W\right),1\right)),v\right)=0)\wedge (\mathrm{schmidtRank}\left(v\right)=m)))\vee ((n\le m)\wedge (\exists v\in \mathrm{Prod}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\right)\to Complex,(\mathrm{mulVec}\left((W+\mathrm{kronecker}\left(1,\mathrm{trOne}\left(W\right)\right)),v\right)=0)\wedge (\mathrm{schmidtRank}\left(v\right)=n))))$$

Formalization. D5/S3/Quantum/Entanglement/WitnessKernelTraceCriteriaRefutation.kernelCriterion (✓ std3).

Citation. Frederik vom Ende and Simon Cichy (2025). Simple Sufficient Criteria for Optimality of Entanglement Witnesses. URL: https://arxiv.org/abs/2505.15615v2.

Commentary.

Theorem 2 uses a full Schmidt-rank vector in one of the two partial-trace-shifted kernels. Both alternatives, with their dimension inequalities, are retained.

Definition 1.7 (Maximally entangled states).

$$\forall m\in Nat,\forall n\in Nat,\forall Omega\in \mathrm{Prod}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\right)\to Complex,(\mathrm{maximallyEntangled}\left(Omega\right))\iff (\exists u\in \mathrm{Fin}\left(\min \left(m,n\right)\right)\to \left(\mathrm{Fin}\left(m\right)\to Complex\right),\exists w\in \mathrm{Fin}\left(\min \left(m,n\right)\right)\to \left(\mathrm{Fin}\left(n\right)\to Complex\right),(\mathrm{Orthonormal}\left(Complex,(\lambda j:\mathrm{Fin}\left(\min \left(m,n\right)\right),\mathrm{toLp}\left(2,u\left(j\right)\right))\right))\wedge ((\mathrm{Orthonormal}\left(Complex,(\lambda j:\mathrm{Fin}\left(\min \left(m,n\right)\right),\mathrm{toLp}\left(2,w\left(j\right)\right))\right))\wedge (Omega=\sum _{j:\mathrm{Fin}\left(\min \left(m,n\right)\right)}(\mathrm{smul}\left(\mathrm{ofReal}\left(\mathrm{natCastReal}{\left(\min \left(m,n\right)\right)}^{-\frac{1}{2}}\right),(\lambda p:\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\right),u\left(j\right)\left(\mathrm{fst}\left(p\right)\right)\cdot w\left(j\right)\left(\mathrm{snd}\left(p\right)\right))\right)))))$$

Formalization. D5/S3/Quantum/Entanglement/WitnessKernelTraceCriteriaRefutation.maximallyEntangled (✓ std3).

Citation. Frederik vom Ende and Simon Cichy (2025). Simple Sufficient Criteria for Optimality of Entanglement Witnesses. URL: https://arxiv.org/abs/2505.15615v2.

Commentary.

Corollary 2 uses min(m,n) orthonormal vectors in each factor with every Schmidt coefficient equal to min(m,n) raised to negative one half. The orthonormality predicates use the standard complex Euclidean inner product.

Definition 1.8 (The trace criterion).

$$\forall m\in Nat,\forall n\in Nat,\forall W\in \mathrm{Matrix}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\right),\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\right),Complex\right),(\mathrm{traceCriterion}\left(W\right))\iff (\exists Omega\in \mathrm{Prod}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\right)\to Complex,(\mathrm{maximallyEntangled}\left(Omega\right))\wedge (\mathrm{dotProduct}\left(\mathrm{star}\left(Omega\right),\mathrm{mulVec}\left(W,Omega\right)\right)=-\frac{\mathrm{trace}\left(W\right)}{\mathrm{natCastComplex}\left(\min \left(m,n\right)\right)}))$$

Formalization. D5/S3/Quantum/Entanglement/WitnessKernelTraceCriteriaRefutation.traceCriterion (✓ std3).

Citation. Frederik vom Ende and Simon Cichy (2025). Simple Sufficient Criteria for Optimality of Entanglement Witnesses. URL: https://arxiv.org/abs/2505.15615v2.

Commentary.

The trace criterion is equality in equation (11) for at least one maximally entangled state. The equality is an equality of complex numbers.

Definition 1.9 (The equivalence question).

$$(claim)\iff (\forall m\in Nat,\forall n\in Nat,\forall W\in \mathrm{Matrix}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\right),\mathrm{Prod}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(n\right)\right),Complex\right),(\mathrm{IsWitness}\left(W\right))\Rightarrow ((\mathrm{kernelCriterion}\left(W\right))\iff (\mathrm{traceCriterion}\left(W\right))))$$

Formalization. D5/S3/Quantum/Entanglement/WitnessKernelTraceCriteriaRefutation.claim (✓ std3).

Citation. Frederik vom Ende and Simon Cichy (2025). Simple Sufficient Criteria for Optimality of Entanglement Witnesses. URL: https://arxiv.org/abs/2505.15615v2.

Commentary.

Section IV asks whether the trace-based criterion of Corollary 2 is equivalent to the kernel criterion of Theorem 2. The statement quantifies over all finite dimensions and every witness.

Theorem 1.10 (The equivalence is false).

$$\neg claim$$

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

Resolves. Problems/vom-ende-cichy-2025-kernel-trace-criteria-refutation (refuted) by D5/S3/Quantum/Entanglement/WitnessKernelTraceCriteriaRefutation.result.

Source. Repository-derived.

Commentary.

In the ordered basis (00,01,10,11), take W with rows (0,0,0,-2), (0,1,0,0), (0,0,4,0), (-2,0,0,0). Its product expectation is the squared modulus of conjugate(x(0))y(1)-2conjugate(x(1))y(0), so it is block positive. The Bell vector (1,0,0,1)/sqrt(2) gives a positive semidefinite outer product with trace pairing -2. The second partial trace is diag(1,4); the shifted matrix annihilates (2,0,0,1), whose coefficient matrix diag(2,1) has rank two. Every maximally entangled state has squared norm one. For any z, the quadratic form of W+2I is 2|z(00)-z(11)| squared plus 3|z(01)| squared plus 6|z(10)| squared. Consequently every such state’s expectation is at least -2, whereas the trace criterion requires -5/2. Thus this witness satisfies the kernel criterion and fails the trace criterion. This conclusion does not alter either criterion’s sufficient implication to optimality.

References

• Truth anchor: D5/S3/Quantum/Entanglement/WitnessKernelTraceCriteriaRefutation.IsWitness
• Truth anchor: D5/S3/Quantum/Entanglement/WitnessKernelTraceCriteriaRefutation.blockPositive
• Truth anchor: D5/S3/Quantum/Entanglement/WitnessKernelTraceCriteriaRefutation.claim
• Truth anchor: D5/S3/Quantum/Entanglement/WitnessKernelTraceCriteriaRefutation.kernelCriterion
• Truth anchor: D5/S3/Quantum/Entanglement/WitnessKernelTraceCriteriaRefutation.maximallyEntangled
• Truth anchor: D5/S3/Quantum/Entanglement/WitnessKernelTraceCriteriaRefutation.result
• Truth anchor: D5/S3/Quantum/Entanglement/WitnessKernelTraceCriteriaRefutation.schmidtRank
• Truth anchor: D5/S3/Quantum/Entanglement/WitnessKernelTraceCriteriaRefutation.trOne
• Truth anchor: D5/S3/Quantum/Entanglement/WitnessKernelTraceCriteriaRefutation.trTwo
• Truth anchor: D5/S3/Quantum/Entanglement/WitnessKernelTraceCriteriaRefutation.traceCriterion
• Dependency: D5/S3/Quantum/Information/PartialTraceMutualInformation