Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help


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 , .

  1. and with , so .
  2. With the Hermitian idempotent of trace one, : eigenvalues once and with multiplicity 24.
  3. 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.