slug: fullwood-parzygnat-2025-states-over-time-subadditivity bibkey: fullwood2025dynamical doi: 10.3390/e27040331 url: https://doi.org/10.3390/e27040331 triage: theorem motivation_gids:
- D5/S3/Quantum/Information/FullwoodParzygnatSubadditivityRefutation.result
Subadditivity of the entropy of quantum states over time
Problem
J. Fullwood and A. J. Parzygnat, On Dynamical Measures of Quantum Information, Entropy 27(4), 331 (2025), Remark 1:
At present, we do not know of any examples of quantum states over time that violate subadditivity, which leads us to conjecture that the entropy functional S restricted to quantum states over time does in fact satisfy subadditivity.
A quantum state over time is for a density matrix and a CPTP map , with the Jamiołkowski matrix , and . The verbatim texts, including the restatement in J. Fullwood and B. Yang, arXiv:2608.28946 §6, are in the literature note. Issue #14994 preregisters the reading over finite Kraus channels and the refutation.
Motivation
The conjecture is equivalent to non-negativity of the dynamical mutual information , the quantity the authors propose as the mutual information between the input and output of a process. Subadditivity fails for general unit-trace Hermitian matrices with positive marginals; the conjecture asserts that the matrices arising from processes are an exception.
Gap
Fullwood and Yang prove subadditivity when the input is a single qubit (any output dimension,
Theorem 4.1) and report that numerical examples suggest failure in higher dimensions, without an example.
The literature check in #14994 found no settlement; not-found-in-searched-scope.
Route
Take , and the Werner–Holevo channel , with the ten Kraus operators , .
- and with , so .
- With the Hermitian idempotent of trace one, : eigenvalues once and with multiplicity 24.
- and , so .
Falsifier
A convention different from the sources (the Choi instead of the Jamiołkowski matrix, another ordering of the factors, or another extension of the entropy), or an error in the spectrum. Positive control in #14994: 300 random qubit-input channels satisfy the inequality, consistently with Theorem 4.1.
Evidence
D5/S3/Quantum/Information/FullwoodParzygnatSubadditivityRefutation.lean defines jamio, pdm and claim over
finite Kraus channels (FiniteKrausChannel.PhyslibLeaf.MatrixMap.of_kraus) with the repository’s signed spectral
entropy ChenKatoBrandaoCMIRefutation.entropy (a sum of Real.negMulLog over the eigenvalues, which equals
because Real.log is even), and proves result : ¬ claim. The axiom closure of
result is exactly propext, Classical.choice and Quot.sound; there is no sorry or
native_decide.
Triage
Tier 1: a named conjecture of a 2025 journal paper, restated open in an August 2026 preprint, preregistered
in #14994 before any Lean. theorem; resolution refuted. result is bind-only (the fixed
counterexample combines the frozen Kraus interface with pinned spectral, functional-calculus and logarithm
facts); admission basis open-problem-resolution; utility kind=certified-instance; basis=refutes. There
is no digestion atom.
What the refutation shows
- Proved by
result: the dynamical mutual information of a quantum process can be negative: the Werner–Holevo channel on the maximally mixed state of gives . - Mechanism: the Jamiołkowski matrix of the Werner–Holevo channel is the partial transpose of its Choi matrix , namely , so the state over time has one negative eigenvalue and the flat positive spectrum of multiplicity . The positive part carries total weight spread over levels and contributes ; the negative eigenvalue contributes . At the excess of the positive part over the of the two maximally mixed marginals outweighs that loss; at it does not.
- Computed, not formalized (#14994): for the same family in dimension the gap is , with NumPy values , , , at (and , at ). Analytically , so and ; positivity for every is not established here.
- Open: the smallest input dimension with a violation (qubit inputs never violate, by Theorem 4.1; qutrit and four-level inputs are not decided by this family), and whether the multi-time generalization of the entropy admits a modified mutual information that is non-negative.
ASSUMED-UNVERIFIED
The literature check in #14994 is bounded and does not establish worldwide novelty or priority.