slug: fuchs-1996-thesis-logarithm-basis-question
bibkey: fuchs1996thesislogarithmbasis
doi: null
url: https://arxiv.org/abs/quant-ph/9601020v1
triage: theorem
motivation_gids:
  - D5/S3/Quantum/Foundation/FuchsLogarithmBasisRefutation.result

Fuchs’s physical-basis logarithm question

Problem

C. A. Fuchs, Distinguishability and Accessible Information in Quantum Theory, arXiv:quant-ph/9601020v1, §3.5.3, pp. 77–78, asks after equation (3.244):

An interesting open question is whether there exists a basis in which to represent the operators ρ̂₀, ρ̂₁, etc., so that the matrix appearing in the logarithm above is diagonal. If so, this would greatly simply the computation of L(t).

The source note identifies the version and equations. Preregistration #18588 fixes the literal Lean conventions. The universal physical-basis assertion is Refuted by D5.S3.Quantum.Foundation.FuchsLogarithmBasisRefutation.result.

Statement echo

The explicit dimension, faithfulness, trace, determinant and interval binders are the preregistered finite density-state interpretation. The construction and every binder are retained literally. The proof uses the frozen PathSpectralClassical.relativeCongruence sandwich and EntropyProductionCoherenceDeletionIdentity.cfc_diagonal for square roots of diagonal matrices.

Motivation

A physical change of basis acts on the original three-dimensional Hilbert space; its induced action on matrix space is constrained. The qutrit witness distinguishes that action from an unrestricted nine-dimensional unitary change of coordinates.

Gap

The source is an explicitly published open question. Issue #18588 records the orchestrator’s thesis reading and repository screen. Its literature screen reports no settlement in Fuchs–Caves (quant-ph/9604001), Jain–Nayak (quant-ph/0603278), or the surveyed later Fuchs papers; the reports concerning Petz–Sudár, Uhlmann and Bhatia–Rosenthal identify ingredients rather than this implication. Those literature reports are seat-reported. Search completeness is ASSUMED-UNVERIFIED.

Route

Let

$$R=\mathrm{diag}(1/2,1/3,1/6),{\rho }_1=\frac{1}{16}\left(\begin{array}{ccc}7& -1& 0\\ -1& 5& 0\\ 0& 0& 4\end{array}\right),D={\rho }_1-R.$$

The private rho0_posDef, rho1_posDef, rho0_trace, rho1_trace and delta_det verify the admissibility of this pair. Write $A=\mathrm{ksum}(R)$, $B=\mathrm{ksum}(D)$, $S=A^{1/2}$ and $K=S^{-1}B{S}^{-1}$. The private K_conj transports $K$ under a physical basis change.

Set $H=D+R/4$. The private kernel_H proves that $HX+XH=0$ forces $X$ to lie on the line through

$$P=\left(\begin{array}{ccc}1& 1& 0\\ 1& 1& 0\\ 0& 0& 0\end{array}\right).$$

The private K_M and K_simple identify the $-1/4$ eigenline of $K$ as the span of the vectorization of

$$M=\left(\begin{array}{ccc}1& \sqrt{5/6}& 0\\ \sqrt{5/6}& \sqrt{2/3}& 0\\ 0& 0& 0\end{array}\right).$$

The private M_minor proves its upper-left minor is nonzero, since $\sqrt{2/3}\ne 5/6$. In contrast, product_column_minor proves that every column of $\overline{U}\otimes U$ has zero such minor. The private diagonal_has_eigen_column supplies a column in the $-1/4$ eigenspace under a proposed diagonalization; unitary_column_ne_zero excludes a zero column. physical_obstruction combines these facts. The public result applies this obstruction at $d=3$, $t=1$.

Declaration judgement

The public result has proof_shape: bind-only, escape_witness: none, and admission_basis: open-problem-resolution (#18588; Refuted). The proof expands to existing matrix/CFC identities, finite entry calculations, algebraic normalization and their consumed logical consequences. Its private auxiliary theorems are consumed bind-only helpers. The helper-to-consumer relation and direct frozen declaration identities are generated from compiled proof terms in the PR judgement tables.

All short names below are in D5.S3.Quantum.Foundation.FuchsLogarithmBasisRefutation; private declaration names have the compiler-generated _private prefix. Consumers are extracted from elaborated constants, including generated intermediate declarations.

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

Falsifier

A physical unitary diagonalizing the stated logarithm argument for this pair at $t=1$, an incorrect source-to-operator correspondence, or an error in the eigenline/minor implication would defeat this refutation. Numerical optimization alone cannot establish the nonexistence of such a unitary; the Lean proof establishes it.

Evidence

The canonical source is FuchsLogarithmBasisRefutation.lean; its Blueprint displays all public definitions and the entire negated claim. The axiom closure of every public declaration is contained in {propext, Classical.choice, Quot.sound}.

Experiment

The experiment directory at commit a826c13d081fbfab273f201823dc367caa68749f contains check.py, SHA-256 96971449bd1f7f214a0d2c49c737c04c6eba2e05ca94070089ee51f84ec5148f. Command: /tmp/op-fuchs/probe/pyenv/bin/python /Users/auric/trureturing-experiments/docs/reports/fuchs-1996-physical-basis-logarithm-diagonal/check.py; exit 0, RESULT PASS. The script bytes match the pinned commit.

For the fixed qutrit pair, at $t=0.25,0.5,1$, respectively, the computed minimum eigenvalues are $0.9375,0.8750,0.7500$, and the best off-diagonal squared Frobenius masses found over 40 optimization starts are $9.480\times 10^{-5},3.792\times 10^{-4},1.517\times 10^{-3}$. These are optimization outputs, not certified global minima or analytic lower bounds. The computed commutator norm is $1.473\times 10^{-2}$. A commuting control at $t=0.7$ yields mass $2.016\times 10^{-16}$. Of 12 generated random qutrit candidates at $t=0.5$, 10 pass the positivity filter and are tested with 15 starts each; their printed commutator/mass pairs satisfy the script’s thresholds. These finite computations prove no all-pair classification.

Triage

What the settlement shows

For the displayed pair, the $(0,1)$ commutator entry is $(1/2-1/3)(-1/16)=-1/96\ne 0$; this is an exact prose calculation, not an additional kernel-checked theorem. The surviving sufficient repair follows directly from the displayed diagonal operations. Neither it nor the numerical examples assert the general converse.

ASSUMED-UNVERIFIED

Completeness of the prior-art screen and the seat-reported literature statements remain ASSUMED-UNVERIFIED. The all-dimension necessity theorem, the full parameter family and the integral/range route are outside the completed formal claim. Numerical search results are finite floating-point observations and do not certify nonexistence or a global minimum. The kernel-checked refutation is conditional on the explicit source interpretation recorded in the statement echo.