slug: slbd2026
bibkey: sprietlangrenez2026kdreal
doi: 10.48550/arXiv.2511.01996
url: https://arxiv.org/abs/2511.01996v2
triage: theorem
motivation_gids:
  - D5/S3/Quantum/Information/KirkwoodDiracSLDRefutation.result

A faithful mixed-state counterexample to KD-real SLD exclusion

Problem

Matéo Spriet, Christopher Langrenez, Raymond Brummelhuis and Stephan De Bièvre, What Is Special About the Kirkwood–Dirac Distributions? Only They Produce Natural Conditional Expectations, arXiv:2511.01996v2, §6.3, immediately after (6.23), state:

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 ${\mathrm{I}}_{\mathrm{QF}}$ does not vanish.

The conjecture is unnumbered; Proposition 6.5 is the published pure-state theorem. The journal article, DOI 10.3390/sym18061008, retains the conjecture after (168), with the pure-state result numbered Proposition 7. The claim is bound to arXiv v2. Source and literature evidence are in #22488; the source note is sprietlangrenez2026kdreal.

Statement echo

All module-local names below belong to D5.S3.Quantum.Information.KirkwoodDiracSLDRefutation; the four public definitions and result are in its SprietKirkwoodDiracSLD namespace.

The public definitions retain the literal source expressions. Density, SLD and Fisher information use their existing owners. Each binder or conjunct above either represents the quoted mathematical setting or makes an implicit existence assertion explicit; none narrows the source class. Faithfulness is a property of the counterexample, not a hypothesis restricting claim.

Motivation

The frozen settling declaration is D5/S3/Quantum/Information/KirkwoodDiracSLDRefutation.result. It refutes the universal mixed-state extension using a faithful nine-dimensional state, a noncommuting KD-real generator, and a KD-real SLD with source QFI $1/6$.

Gap

The pure-state exclusion does not imply mixed-state exclusion. A KD-real Hermitian sector can contain noncommuting matrices; Hermitian does not mean entrywise real in either original basis. The explicit counterexample supplies the missing mixed-state test.

Route

The module verifies literal rational and $\sqrt{3}$ matrix entries. Its private Fourier matrix supplies a unitary second basis with no zero overlaps. A projection certificate proves positivity of $\rho =(I+E)/12$, and the trace is one. Entrywise coefficient calculations establish KD reality of $\rho$, $X$ and $L$. The SLD equation and $\mathrm{Tr}(\rho L^2)=1/6$ contradict the universal conclusion.

The public result is the designated refutation result (basis=refutes) and is exempt from four-slot escape registration (CLAUDE.md §3.9).

Falsifier

A source restriction excluding faithful dimension-nine inputs, a change in the KD-symbol convention, or a failure of the literal SLD/QFI identities would invalidate this translation. The source formulation and the unchanged public definitions fix those conventions. The conjecture’s negation does not claim failure of the published pure-state theorem or the restricted mixed-state examples.

Evidence

Kernel-checked scope

SprietKirkwoodDiracSLD.result proves the exact negation of claim. The private consumed declarations Probe.rho_positive, Probe.rho_trace, Probe.rho_coefficient, Probe.obs_coefficient, Probe.sld_coefficient, Probe.sld_equation and Probe.qfi_value verify the concrete witness. The family and the abstract algebra mechanism below are not Lean theorems in this module. All these names use the module namespace stated above.

Exact experiment

Experiments directory at b9a1174abe58ac137c7a7e49bb845ac52832fbf0.

The verified script is docs/reports/kd-real-sld/check.py, SHA-256 c42699ad074e01429ad4d7357c5bb4499247ab9794c763bb85e31ea49e9c086f. The command python3 /Users/auric/.sshx/815985d0136943d51269228f/attempt-1/check-experiment.py runs the exact bytes extracted from that commit; exit 0, with ALL_CHECKS_OK, using Python 3.14.8 and SymPy 1.14.0. It checks the symbolic $p=3$ rational identities with a real parameter, positivity certificates for $0<t<1$, and the member $t=1/2$. The finite graph identities are checked only at $p=3,5,7$, over respectively $729$, $15625$, and $117649$ monomial products. The pure-qubit fidelity example has QFI $4$ and non-real SLD symbol. These are exact symbolic computations, not floating-point samples or Lean proofs.

Triage

What the settlement shows

1. Proved, kernel-checked: the literal universal mixed-state claim is false (SprietKirkwoodDiracSLD.result). The faithful $d=9$ witness and its QFI $1/6$ are checked by the consumed Probe.rho_positive and Probe.qfi_value calculations, together with the KD-reality and SLD helpers listed in Evidence.

2. Computed: for $p=3$ and every real $0<t<1$, the experiment’s family is faithful and KD-positive. With its rank-three projection $E$ and Hermitian generator $X$, it has $L_t=-6it[X,E]/(4+t)$, a KD-real SLD, and QFI $3t^2/(4+t)$. Evidence: the exact experiment above; this uniform family is not a Lean theorem here.

3. Computed identities, with range justified by algebra: the same rational matrix identities are checked with $t$ real. They apply on $-1\le t\le 2$, with nonzero QFI when $t\ne 0$; the states are faithful on $-1<t<2$. For $t=3u-1$, substitution in the checked scalar expressions gives eigenvalues $(1+t)/9=u/3$ and $(1-t/2)/9=(1-u)/6$, KD entries $(1+t)/81=u/27$ and $(2-t)/162=(1-u)/54$, and QFI $3t^2/(4+t)=(3u-1{)}^2/(u+1)$. On $0\le u\le 1$ all eigenvalues and KD entries are nonnegative, and on the interior they are positive; $4+t=3(u+1)>0$. This substitution and sign argument are proved in prose from the experiment’s identities; no additional computational range or Lean family theorem is claimed.

4. Computed: at $t=1/2$, the density eigenvalues are $1/6$ with multiplicity three and $1/12$ with multiplicity six, and KD entries are $1/54$ and $1/108$. Evidence: the exact experiment’s projection decomposition and member certificate.

5. Computed: the $p=3$ family has a nonzero commutator while its Jordan equation has the KD-real solution above. Evidence: the exact symbolic matrix checker. The concrete Lean realization verifies the single instance; abstract closure of a KD-real star-algebra under Jordan inversion is not formally proved here.

6. Computed: both original-basis marginals are $1/9$ and both tangent diagonals vanish in the $p=3$ family. Hence their classical Fisher information is zero. Evidence: the exact experiment’s marginal and derivative identities; the final consequence follows because every summand is a zero squared derivative divided by $1/9$. This agrees with the source Proposition 6.3.

7. Proved in prose by hypothesis separation: the published pure-state Proposition 6.5 and the two restricted mixed-state examples are not negated. This witness is faithful and has two distinct positive eigenvalues, so it is not pure. Both mixed-state examples first require the $A$ basis to diagonalize $\rho$. The first additionally assumes real transition coefficients; the second assumes $X=f(A)+{\Pi }_{b_0}^B$. In this counterexample $A$ is the computational basis and ${\rho }_{0,3}=1/36$, as follows by substitution in the displayed witness matrix, so its state is not diagonal in that basis. Its Fourier transition matrix also has non-real entries. Thus neither source example asserts the unrestricted conclusion refuted here. No Lean proof of these neighbouring theorems is claimed. The exact experiment additionally checks one pure-qubit fidelity instance, without proving the general source theorem. The source’s established results keep their stated hypotheses; no proved result is inferred false merely because this conjectured extension fails.

8. Open: the arbitrary odd-prime family and the general KD-real star-algebra/Jordan-map mechanism as Lean theorems. The preregistration supplies an ordinary proof outline, while the experiment checks the finite graph laws only for $p=3,5,7$.

9. Open: minimal counterexample dimension and classification of bases or extra hypotheses for which mixed-state exclusion survives. A witness in dimension nine proves an upper bound on the least possible counterexample dimension, without a minimality claim.

Literature status

The source and literature screen recorded in #22488 found no settlement in its checked scope. The accessible source arXiv v2 and journal §6.3 retain the question; the current source-citing papers and the relevant accessible KD/Fourier papers did not supply the settlement. Standard Weyl identities and spectral SLD facts are ingredients, not a claim of originality for those facts. The exact finite refutation is an application settling the named assertion; the arbitrary-prime mechanism remains outside this module’s formal scope.

ASSUMED-UNVERIFIED

Literature completeness is ASSUMED-UNVERIFIED. The full Brummelhuis journal texts behind DOIs 10.1088/1751-8121/ae1271 and 10.1088/1751-8121/ae1337 were inaccessible; their accessible precursor was screened. Full theses 2607.26761 and 2605.29717 were not exhaustively read, and author/citation searches had access or rate limits. No exhaustive novelty or minimal-dimension claim is made. The parameter family, scalar range explanation and abstract algebra discussion have the evidence kinds stated in Triage, rather than being promoted to new Lean theorems.