A mixed-state KD-real SLD counterexample

Abstract

A faithful nine-dimensional mixed state has a KD-real symmetric logarithmic derivative with nonzero quantum Fisher information, refuting the mixed-state exclusion conjecture.

Definition 1.1 (The left Kirkwood–Dirac distribution).

$$\forall d\in \mathbb{N},\forall a\in Matrix.unitaryGroup\left(\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall b\in Matrix.unitaryGroup\left(\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall C\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall x\in \mathrm{Fin}\left(d\right),\forall k\in \mathrm{Fin}\left(d\right),\mathrm{qLeft}\left(a,b,C\right)\left(x,k\right)=\mathrm{star}\left(\left(\mathrm{conjTranspose}\left(\mathrm{val}\left(a\right)\right)\cdot \mathrm{val}\left(b\right)\right)\left(x,k\right)\right)\cdot \left(\mathrm{conjTranspose}\left(\mathrm{val}\left(a\right)\right)\cdot C\cdot \mathrm{val}\left(b\right)\right)\left(x,k\right)$$

Formalization. D5/S3/Quantum/Information/KirkwoodDiracSLDRefutation.qLeft (✓ std3).

Citation. Matéo Spriet, Christopher Langrenez, Raymond Brummelhuis, Stephan De Bièvre (2026). What Is Special About the Kirkwood–Dirac Distributions? Only They Produce Natural Conditional Expectations. DOI: 10.48550/arXiv.2511.01996. URL: https://arxiv.org/abs/2511.01996v2.

Commentary.

The left KD distribution is the conjugate overlap multiplied by the matrix coefficient between the two orthonormal eigenbases.

Definition 1.2 (The left KD symbol).

$$\forall d\in \mathbb{N},\forall a\in Matrix.unitaryGroup\left(\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall b\in Matrix.unitaryGroup\left(\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall C\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall x\in \mathrm{Fin}\left(d\right),\forall k\in \mathrm{Fin}\left(d\right),\mathrm{symbolLeft}\left(a,b,C\right)\left(x,k\right)=Inv.inv\left(\left(\mathrm{conjTranspose}\left(\mathrm{val}\left(a\right)\right)\cdot \mathrm{val}\left(b\right)\right)\left(x,k\right)\right)\cdot \left(\mathrm{conjTranspose}\left(\mathrm{val}\left(a\right)\right)\cdot C\cdot \mathrm{val}\left(b\right)\right)\left(x,k\right)$$

Formalization. D5/S3/Quantum/Information/KirkwoodDiracSLDRefutation.symbolLeft (✓ std3).

Citation. Matéo Spriet, Christopher Langrenez, Raymond Brummelhuis, Stephan De Bièvre (2026). What Is Special About the Kirkwood–Dirac Distributions? Only They Produce Natural Conditional Expectations. DOI: 10.48550/arXiv.2511.01996. URL: https://arxiv.org/abs/2511.01996v2.

Commentary.

The left symbol is the inverse overlap multiplied by the same matrix coefficient.

Definition 1.3 (KD-real Hermitian matrices).

$$\forall d\in \mathbb{N},\forall a\in Matrix.unitaryGroup\left(\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall b\in Matrix.unitaryGroup\left(\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall C\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\mathrm{IsKDReal}\left(a,b,C\right)=\left((\mathrm{IsHermitian}\left(C\right))\wedge (\forall x\in \mathrm{Fin}\left(d\right),\forall k\in \mathrm{Fin}\left(d\right),Complex.im\left(Inv.inv\left(\left(\mathrm{conjTranspose}\left(\mathrm{val}\left(a\right)\right)\cdot \mathrm{val}\left(b\right)\right)\left(x,k\right)\right)\cdot \left(\mathrm{conjTranspose}\left(\mathrm{val}\left(a\right)\right)\cdot C\cdot \mathrm{val}\left(b\right)\right)\left(x,k\right)\right)=0)\right)$$

Formalization. D5/S3/Quantum/Information/KirkwoodDiracSLDRefutation.IsKDReal (✓ std3).

Citation. Matéo Spriet, Christopher Langrenez, Raymond Brummelhuis, Stephan De Bièvre (2026). What Is Special About the Kirkwood–Dirac Distributions? Only They Produce Natural Conditional Expectations. DOI: 10.48550/arXiv.2511.01996. URL: https://arxiv.org/abs/2511.01996v2.

Commentary.

A matrix is left KD-real when it is Hermitian and the imaginary part of its left KD symbol vanishes at every pair of basis labels.

Definition 1.4 (The mixed-state conjecture).

$$claim\iff (\forall d\in \mathbb{N},(0<d)\Rightarrow (\forall a\in Matrix.unitaryGroup\left(\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall b\in Matrix.unitaryGroup\left(\mathrm{Fin}\left(d\right),\mathbb{C}\right),(\forall x\in \mathrm{Fin}\left(d\right),\forall k\in \mathrm{Fin}\left(d\right),\left(\mathrm{conjTranspose}\left(\mathrm{val}\left(a\right)\right)\cdot \mathrm{val}\left(b\right)\right)\left(x,k\right)\ne 0)\Rightarrow (\forall rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall X\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),(D5.S3.Quantum.Information.SLDSpectralEnergy.IsDensity\left(rho\right))\Rightarrow ((\mathrm{IsKDReal}\left(a,b,rho\right))\Rightarrow ((\mathrm{IsKDReal}\left(a,b,X\right))\Rightarrow ((\exists L\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\mathrm{IsSLD}\left(rho,X,L\right))\wedge (\forall L\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),(D5.S3.Quantum.Information.FisherDiscord.Defs.IsSLD\left(rho,X,L\right))\Rightarrow ((4\cdot D5.S3.Quantum.Information.FisherDiscord.Defs.fisherSLD\left(rho,L\right)\ne 0)\Rightarrow (\neg (\mathrm{IsKDReal}\left(a,b,L\right)))))))))))$$

Formalization. D5/S3/Quantum/Information/KirkwoodDiracSLDRefutation.claim (✓ std3).

Citation. Matéo Spriet, Christopher Langrenez, Raymond Brummelhuis, Stephan De Bièvre (2026). What Is Special About the Kirkwood–Dirac Distributions? Only They Produce Natural Conditional Expectations. DOI: 10.48550/arXiv.2511.01996. URL: https://arxiv.org/abs/2511.01996v2.

Commentary.

Section 6.3, immediately after equation (6.23), states verbatim: “In view of what precedes, it is tempting to conjecture that, if \hat \rho and \hat X are both KD real, the optimal observable \hat L must not be KD-real itself, provided \rm I_{QF} does not vanish.” The encoding quantifies over every positive finite dimension, two unitary bases with nonzero overlaps, every density matrix and Hermitian observable in the KD-real sector, and every Hermitian SLD solution. The source QFI is 4 times fisherSLD.

Theorem 1.5 (The conjecture is false).

$$\neg (\forall d\in \mathbb{N},(0<d)\Rightarrow (\forall a\in Matrix.unitaryGroup\left(\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall b\in Matrix.unitaryGroup\left(\mathrm{Fin}\left(d\right),\mathbb{C}\right),(\forall x\in \mathrm{Fin}\left(d\right),\forall k\in \mathrm{Fin}\left(d\right),\left(\mathrm{conjTranspose}\left(\mathrm{val}\left(a\right)\right)\cdot \mathrm{val}\left(b\right)\right)\left(x,k\right)\ne 0)\Rightarrow (\forall rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\forall X\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),(D5.S3.Quantum.Information.SLDSpectralEnergy.IsDensity\left(rho\right))\Rightarrow ((\mathrm{IsKDReal}\left(a,b,rho\right))\Rightarrow ((\mathrm{IsKDReal}\left(a,b,X\right))\Rightarrow ((\exists L\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\mathrm{IsSLD}\left(rho,X,L\right))\wedge (\forall L\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),(D5.S3.Quantum.Information.FisherDiscord.Defs.IsSLD\left(rho,X,L\right))\Rightarrow ((4\cdot D5.S3.Quantum.Information.FisherDiscord.Defs.fisherSLD\left(rho,L\right)\ne 0)\Rightarrow (\neg (\mathrm{IsKDReal}\left(a,b,L\right)))))))))))$$

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

Resolves. Problems/slbd2026 (refuted) by D5/S3/Quantum/Information/KirkwoodDiracSLDRefutation.result.

Source. Repository-derived.

Acknowledgement. Matéo Spriet, Christopher Langrenez, Raymond Brummelhuis, Stephan De Bièvre (2026). What Is Special About the Kirkwood–Dirac Distributions? Only They Produce Natural Conditional Expectations. DOI: 10.48550/arXiv.2511.01996. URL: https://arxiv.org/abs/2511.01996v2.

Commentary.

The explicit p = 3, dimension-nine witness uses the identity basis and an explicit Fourier basis, a faithful density matrix rho, the Hermitian observable X and the Hermitian matrix L. The coefficient calculations make rho, X and L KD-real; L solves the SLD equation; and the source-normalized QFI is 1/6, so the universal conclusion that every nonzero-QFI SLD is not KD-real fails.

References

• Truth anchor: D5/S3/Quantum/Information/KirkwoodDiracSLDRefutation.IsKDReal
• Truth anchor: D5/S3/Quantum/Information/KirkwoodDiracSLDRefutation.claim
• Truth anchor: D5/S3/Quantum/Information/KirkwoodDiracSLDRefutation.qLeft
• Truth anchor: D5/S3/Quantum/Information/KirkwoodDiracSLDRefutation.result
• Truth anchor: D5/S3/Quantum/Information/KirkwoodDiracSLDRefutation.symbolLeft
• Dependency: D5/S3/Quantum/Information/FisherDiscord/Defs
• Dependency: D5/S3/Quantum/Information/SLDSpectralEnergy