TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Channel data processing for finite quantum relative entropy

Statement

Let $H, K$ be nonzero finite-dimensional complex inner-product spaces, let $Φ : L (H) \to L (K)$ be a quantum channel (Finite-dimensional quantum channel), and let $A, B$ be non-negative operators on $H$ . Then

$D (Φ (A) ∥ Φ (B)) \leq D (A ∥ B) .$

Facts & Assumptions

Given: The spaces, channel and non-negative operators in the Statement.

[F1]

Kraus and Choi characterizations of complete positivity: a finite-dimensional completely positive map has a finite Kraus representation.

[F2]

Finite Kraus representation: a Kraus representation has the form $Φ (X) = \sum_{j} K_{j} X K_{j}^{*}$ on the full operator space.

[F3]

Trace preservation is Kraus normalization: trace preservation is equivalent to $\sum_{j} K_{j}^{*} K_{j} = I_{H}$ .

[F4]

Partial-trace data processing for finite quantum relative entropy: partial trace over a nonzero finite factor does not increase QRE.

[F5]

Isometric invariance of finite quantum relative entropy: simultaneous isometric conjugation preserves QRE.

[F6]

Partial trace over a finite tensor factor: partial trace over the environment removes the matching diagonal Kraus blocks and retains the output operator.

[F7]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ : $⟨ K x, K y ⟩ = ⟨ x, K^{*} K y ⟩$ under the repository's inner-product convention.

[F8]

Finite registers and their ordered computational bases: the standard register $E = C^{r}$ has the specified ordered orthonormal basis $(f_{j})$ .

Proof

1.1givenF1F2F3F7F8construct

By [F1]–[F2], choose a finite Kraus family $(K_{j})_{j < r}$ for $Φ$ . Since $H \neq {0}$ and [F3] gives $\sum_{j} K_{j}^{*} K_{j} = I_{H}$ , the family is nonempty. Let $E = C^{r}$ with the ordered orthonormal basis $(f_{j})$ from [F8], and define $V : H \to K \otimes E$ by $V x : = \sum_{j < r} K_{j} x \otimes f_{j}$ . For $x, y \in H$ , orthonormality and [F3], [F7] give $⟨ V x, V y ⟩ = \sum_{j} ⟨ K_{j} x, K_{j} y ⟩ = ⟨ x, (\sum_{j} K_{j}^{*} K_{j}) y ⟩ = ⟨ x, y ⟩$ ; hence $V^{*} V = I_{H}$ .

2.1givenF2F6F8step 1.1algebra

Expanding in the environment basis [F8] gives $V X V^{*} = \sum_{j, k} K_{j} X K_{k}^{*} \otimes M_{j k}$ , where $M_{j k} z = ⟨ z, f_{k} ⟩ f_{j}$ . The partial-trace formula [F6] keeps exactly the terms $j = k$ , so ${Tr}_{E} (V X V^{*}) = \sum_{j} K_{j} X K_{j}^{*} = Φ (X)$ for every $X$ .

3.1givenF4F5step 2.1algebra∎

Apply isometric invariance [F5] and then partial-trace data processing [F4] to the pair $(V A V^{*}, V B V^{*})$ on $K \otimes E$ . By step 2.1, $D (Φ (A) ∥ Φ (B)) = D ({Tr}_{E} (V A V^{*}) ∥ {Tr}_{E} (V B V^{*})) \leq D (V A V^{*} ∥ V B V^{*}) = D (A ∥ B)$ .

Remarks

The finite Stinespring dilation used in the proof is summarized by the following map diagram. It records the factor that is discarded by the partial trace; the proof relies on the Kraus and trace calculations above, not on the diagram.

Depends on

Used by

Qubit dephasing decreases quantum relative entropy Example
Nonnegativity and equality for finite quantum relative entropy Theorem
The finite Holevo measurement bound Theorem

Dependency tree · two levels

43 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

John Watrous, The Theory of Quantum Information, Theorem 5.35 (standard reference, not scraped)
Mark M. Wilde, From Classical to Quantum Shannon Theory, arXiv:1106.1445v8, Theorem 11.8.1 and §12.5 (standard reference, not scraped)