The Fuchs–Caves fidelity ROC question is refuted

Abstract

A three-dimensional fidelity measurement point lies below the optimal quantum ROC curve.

Definition 1.1 (The optimal ROC boundary at a fixed false-positive coordinate).

$$\forall (d:\mathbb{N}),(\forall (\rho :\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)),(\forall (\Sigma :\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)),(\forall (x:\mathbb{R}),(\forall (y:\mathbb{R}),((D5.S3.Quantum.Measurement.FidelityMeasurementROCRefutation.onOptimalROC\left(\rho ,\Sigma ,x,y\right))\iff (\forall (f:\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)),((f\in Set.Icc\left((0:\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)),(1:\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right))\right))\Rightarrow ((Complex.re\left(Matrix.trace\left((f)\cdot (\rho )\right)\right)=x)\Rightarrow (Complex.re\left(Matrix.trace\left((f)\cdot (\Sigma )\right)\right)\le y)))))))))$$

Formalization. D5/S3/Quantum/Measurement/FidelityMeasurementROCRefutation.onOptimalROC (✓ std3).

Citation. András Bodor and Mátyás Koniorczyk (2017). Receiver Operation Characteristics of Quantum State Discrimination. DOI: 10.1007/s10946-017-9629-5. URL: https://arxiv.org/abs/1603.06801v1.

Commentary.

The source describes the feasible ROC domain as convex and calls its upper boundary the optimal ROC curve (TeX lines 289–300). For a matrix test f, onOptimalROC requires every effect between zero and the identity whose false-positive coordinate is x to have true-positive coordinate at most y.

Definition 1.2 (The Fuchs–Caves fidelity observable).

$$\forall (d:\mathbb{N}),(\forall (\rho :\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)),(\forall (\Sigma :\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)),(D5.S3.Quantum.Measurement.FidelityMeasurementROCRefutation.fidelityObservable\left(\rho ,\Sigma \right)=((Inv.inv\left(CFC.sqrt\left(\rho \right)\right))\cdot (CFC.sqrt\left(((CFC.sqrt\left(\rho \right))\cdot (\Sigma ))\cdot (CFC.sqrt\left(\rho \right))\right)))\cdot (Inv.inv\left(CFC.sqrt\left(\rho \right)\right)))))$$

Formalization. D5/S3/Quantum/Measurement/FidelityMeasurementROCRefutation.fidelityObservable (✓ std3).

Citation. András Bodor and Mátyás Koniorczyk (2017). Receiver Operation Characteristics of Quantum State Discrimination. DOI: 10.1007/s10946-017-9629-5. URL: https://arxiv.org/abs/1603.06801v1.

Commentary.

The observable is the matrix in equation (44), TeX lines 932–940: the inverse of the positive square root of the first state, followed by the positive square root of the sandwich with the second state, followed by the same inverse.

Definition 1.3 (Cumulative measurement probability).

$$\forall (d:\mathbb{N}),(\forall (a:\mathrm{Fin}\left(d\right)\to \left(\mathrm{Fin}\left(d\right)\to \mathbb{C}\right)),(\forall (m:\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)),(\forall (k:\mathrm{Fin}\left((d)+(1)\right)),(D5.S3.Quantum.Measurement.FidelityMeasurementROCRefutation.cumulative\left(a,m,k\right)=Finset.sum\left(Finset.filter\left(\lambda (i:\mathrm{Fin}\left(d\right))\mapsto (Fin.val\left(i\right)<Fin.val\left(k\right)),Finset.univ\left(\mathrm{Fin}\left(d\right)\right)\right),\lambda (i:\mathrm{Fin}\left(d\right))\mapsto (D5.S3.Quantum.Recovery.ProductPrefixRigidity.readout\left(m,a\left(i\right)\right))\right)))))$$

Formalization. D5/S3/Quantum/Measurement/FidelityMeasurementROCRefutation.cumulative (✓ std3).

Citation. András Bodor and Mátyás Koniorczyk (2017). Receiver Operation Characteristics of Quantum State Discrimination. DOI: 10.1007/s10946-017-9629-5. URL: https://arxiv.org/abs/1603.06801v1.

Commentary.

The source forms cumulative ROC coordinates by summing the ordered outcome probabilities (TeX lines 383–392). The definition sums the readout of m on the first k indices of the matrix-valued outcome family a.

Definition 1.4 (An ordered eigenbasis of the fidelity observable).

$$\forall (d:\mathbb{N}),(\forall (\rho :\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)),(\forall (\Sigma :\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)),(\forall (a:\mathrm{Fin}\left(d\right)\to \left(\mathrm{Fin}\left(d\right)\to \mathbb{C}\right)),((D5.S3.Quantum.Measurement.FidelityMeasurementROCRefutation.isOrderedFidelityEigenbasis\left(\rho ,\Sigma ,a\right))\iff ((\forall (i:\mathrm{Fin}\left(d\right)),(Finset.sum\left(Finset.univ\left(\mathrm{Fin}\left(d\right)\right),\lambda (j:\mathrm{Fin}\left(d\right))\mapsto ((\mathrm{star}\left(a\left(i\right)\left(j\right)\right))\cdot (a\left(i\right)\left(j\right)))\right)=(1:\mathbb{C})))\wedge ((\forall (i:\mathrm{Fin}\left(d\right)),(\forall (j:\mathrm{Fin}\left(d\right)),((i\ne j)\Rightarrow (Finset.sum\left(Finset.univ\left(\mathrm{Fin}\left(d\right)\right),\lambda (k:\mathrm{Fin}\left(d\right))\mapsto ((\mathrm{star}\left(a\left(i\right)\left(k\right)\right))\cdot (a\left(j\right)\left(k\right)))\right)=(0:\mathbb{C})))))\wedge ((\forall (i:\mathrm{Fin}\left(d\right)),(\exists (r:\mathbb{R}),(Matrix.mulVec\left(D5.S3.Quantum.Measurement.FidelityMeasurementROCRefutation.fidelityObservable\left(\rho ,\Sigma \right),a\left(i\right)\right)=((Complex.ofReal\left(r\right):\mathbb{C}))\cdot (a\left(i\right)))))\wedge (\forall (i:\mathrm{Fin}\left(d\right)),(\forall (j:\mathrm{Fin}\left(d\right)),((i\le j)\Rightarrow ((D5.S3.Quantum.Recovery.ProductPrefixRigidity.readout\left(\Sigma ,a\left(i\right)\right))\cdot (D5.S3.Quantum.Recovery.ProductPrefixRigidity.readout\left(\rho ,a\left(j\right)\right))\ge (D5.S3.Quantum.Recovery.ProductPrefixRigidity.readout\left(\Sigma ,a\left(j\right)\right))\cdot (D5.S3.Quantum.Recovery.ProductPrefixRigidity.readout\left(\rho ,a\left(i\right)\right)))))))))))))$$

Formalization. D5/S3/Quantum/Measurement/FidelityMeasurementROCRefutation.isOrderedFidelityEigenbasis (✓ std3).

Citation. András Bodor and Mátyás Koniorczyk (2017). Receiver Operation Characteristics of Quantum State Discrimination. DOI: 10.1007/s10946-017-9629-5. URL: https://arxiv.org/abs/1603.06801v1.

Commentary.

The source orders measurement outcomes by decreasing likelihood ratio p_i/q_i (TeX lines 329–335). This predicate requires normalized rows, pairwise orthogonality, eigenvector equations for the fidelity observable, and the corresponding likelihood-ratio ordering.

Definition 1.5 (Every cumulative fidelity point is optimal).

$$(D5.S3.Quantum.Measurement.FidelityMeasurementROCRefutation.claim\left(\right))\iff (\forall (d:\mathbb{N}),(\forall (\rho :\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)),(\forall (\Sigma :\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)),((Matrix.PosDef\left(\rho \right))\Rightarrow ((Matrix.trace\left(\rho \right)=(1:\mathbb{C}))\Rightarrow ((Matrix.PosDef\left(\Sigma \right))\Rightarrow ((Matrix.trace\left(\Sigma \right)=(1:\mathbb{C}))\Rightarrow (\forall (a:\mathrm{Fin}\left(d\right)\to \left(\mathrm{Fin}\left(d\right)\to \mathbb{C}\right)),((D5.S3.Quantum.Measurement.FidelityMeasurementROCRefutation.isOrderedFidelityEigenbasis\left(\rho ,\Sigma ,a\right))\Rightarrow (\forall (k:\mathrm{Fin}\left((d)+(1)\right)),(D5.S3.Quantum.Measurement.FidelityMeasurementROCRefutation.onOptimalROC\left(\rho ,\Sigma ,D5.S3.Quantum.Measurement.FidelityMeasurementROCRefutation.cumulative\left(a,\rho ,k\right),D5.S3.Quantum.Measurement.FidelityMeasurementROCRefutation.cumulative\left(a,\Sigma ,k\right)\right))))))))))))$$

Formalization. D5/S3/Quantum/Measurement/FidelityMeasurementROCRefutation.claim (✓ std3).

Source. Repository-derived.

Acknowledgement. András Bodor and Mátyás Koniorczyk (2017). Receiver Operation Characteristics of Quantum State Discrimination. DOI: 10.1007/s10946-017-9629-5. URL: https://arxiv.org/abs/1603.06801v1.

Commentary.

The formal question asserts that for every finite dimension, every pair of positive-definite trace-one complex matrices, every ordered orthonormal eigenbasis of the fidelity observable, and every k in Fin(d + 1), the cumulative point is on the optimal ROC boundary.

Theorem 1.6 (A qutrit counterexample).

$$\neg (D5.S3.Quantum.Measurement.FidelityMeasurementROCRefutation.claim\left(\right))$$

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

Resolves. Problems/bodor-koniorczyk-2017-fidelity-measurement-roc-refutation (refuted) by D5/S3/Quantum/Measurement/FidelityMeasurementROCRefutation.result.

Source. Repository-derived.

Acknowledgement. András Bodor and Mátyás Koniorczyk (2017). Receiver Operation Characteristics of Quantum State Discrimination. DOI: 10.1007/s10946-017-9629-5. URL: https://arxiv.org/abs/1603.06801v1.

Commentary.

Use the displayed three-dimensional states with entries 1/20 times [[2,1,1],[1,10,1],[1,1,8]] and 1/40 times [[16,4,2],[4,20,1],[2,1,4]], and use the diagonal observable diag(2,1,1/2). The first state is positive definite because its unscaled matrix is the sum of the all-ones rank-one matrix and a positive diagonal matrix; the second is a positive diagonal congruence of the first. Direct trace calculation gives trace one for both.

The positive square-root uniqueness argument identifies the Fuchs–Caves observable with the displayed diagonal matrix. Its coordinate basis is an ordered eigenbasis: the eigenvalues are 2, 1 and 1/2, while the readout probabilities are q = (1/10, 1/2, 2/5) and p = (2/5, 1/2, 1/10), so the likelihood ratios decrease as 4, 1, 1/4. At k = 1 the cumulative point is (1/10, 2/5).

Take the rank-one effect vvᵀ/1382 with v = (37,2,−3). Its positive-semidefinite and upper-bound certificates place it in the interval [0,1]. Exact multiplication gives false-positive coordinate 1/10 and true-positive coordinate 5539/13820, while 2/5 is 5528/13820. Applying the claimed optimality at k = 1 would therefore give 5539/13820 ≤ 2/5, which is false.

References

• Truth anchor: D5/S3/Quantum/Measurement/FidelityMeasurementROCRefutation.claim
• Truth anchor: D5/S3/Quantum/Measurement/FidelityMeasurementROCRefutation.cumulative
• Truth anchor: D5/S3/Quantum/Measurement/FidelityMeasurementROCRefutation.fidelityObservable
• Truth anchor: D5/S3/Quantum/Measurement/FidelityMeasurementROCRefutation.isOrderedFidelityEigenbasis
• Truth anchor: D5/S3/Quantum/Measurement/FidelityMeasurementROCRefutation.onOptimalROC
• Truth anchor: D5/S3/Quantum/Measurement/FidelityMeasurementROCRefutation.result
• Dependency: D5/S3/Quantum/Entanglement/AbsoluteSeparability/LowRankRays
• Dependency: D5/S3/Quantum/Matrix/AlternativeMeanLinearization