LemmaStatement: AI-adaptedProof: 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.

A finite POVM defines a classical-output quantum channel

Statement

Let $H$ be a nonzero finite-dimensional complex inner-product space and let $(E_{y})_{y \in Ω}$ be a finite POVM on $H$ , where $Ω = {y_{0}, \dots, y_{m - 1}}$ is a fixed enumeration of its nonempty outcome set. Let $K = C^{m}$ with standard orthonormal basis $(f_{0}, \dots, f_{m - 1})$ , and set $Π_{j} z : = ⟨ z, f_{j} ⟩ f_{j}$ , the rank-one projection onto $f_{j}$ under the root linear-first convention. The map $M_{E} (X) : = \sum_{j < m} tr (X E_{y_{j}}) Π_{j}$ is a quantum channel from $H$ to $K$ . For the indexed register $C^{Ω}$ with orthonormal basis $∣ y ⟩$ , the unitary identification $J f_{j} = ∣ y_{j} ⟩$ gives the equivalent channel $X \mapsto \sum_{y \in Ω} tr (E_{y} X) ∣ y ⟩ ⟨ y ∣ = J M_{E} (X) J^{*}$ . Thus either finite outcome-register convention is covered.

Facts & Assumptions

Given: The space $H$ , the finite POVM, its enumeration, and the output register $K$ in the Statement.

[F1]

Finite POVMs and their outcome law: each $E_{y}$ is non-negative and $\sum_{y} E_{y} = I_{H}$ ; the outcome weight on a state $ρ$ is $tr (ρ E_{y})$ .

[F2]

A non-negative operator has a unique non-negative square root: every non-negative operator $E_{y}$ has a non-negative square root $E_{y}^{1 / 2}$ .

[F3]

Real and complex inner-product spaces and their induced length: the inner product is linear in its first argument and conjugate-linear in its second.

[F4]

Finite Kraus representation: a finite Kraus family represents $Φ$ when $Φ (X) = \sum_{a} K_{a} X K_{a}^{*}$ for every input operator.

[F5]

Kraus and Choi characterizations of complete positivity: a finite Kraus representation implies complete positivity.

[F6]

Trace preservation is Kraus normalization: a finite Kraus representation is trace-preserving exactly when $\sum_{a} K_{a}^{*} K_{a} = I_{H}$ .

[F7]

For $A \in M_{m \times n} (F)$ and $B \in M_{n \times m} (F)$ , $tr (A B) = tr (B A)$ : the trace is cyclic for compatible finite-dimensional maps.

[F8]

Finite-dimensional quantum channel: a finite-dimensional quantum channel is a complex-linear completely positive trace-preserving map on the full operator space.

[F9]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ : the adjoint satisfies $⟨ K x, z ⟩ = ⟨ x, K^{*} z ⟩$ .

[F10]

Every finite-dimensional real or complex inner product space has an orthonormal basis: every finite-dimensional inner-product space has an orthonormal basis.

[F11]

Finite registers and their ordered computational bases: the specified output basis $(f_{j})$ is orthonormal.

[F12]

Every linear map between finite-dimensional inner product spaces has a unique adjoint: finite-dimensional linear maps have unique adjoints.

Proof

1.1givenF12F2F3F9F10F11constructchoose

The adjoints used below exist uniquely by [F12]. Choose an ordered orthonormal basis $(e_{k})_{k < d}$ of $H$ using [F10]. For each $j < m$ and $k < d$ , define $K_{j k} : H \to K$ by $K_{j k} x = f_{j} ⟨ E_{y_{j}}^{1 / 2} x, e_{k} ⟩$ . This is linear by the root convention in [F3]. Set $P_{k} x : = ⟨ x, e_{k} ⟩ e_{k}$ . The adjoint identity [F9] and the output-basis orthonormality [F11] give $K_{j k}^{*} z = ⟨ z, f_{j} ⟩ E_{y_{j}}^{1 / 2} e_{k}$ and therefore $K_{j k}^{*} K_{j k} = E_{y_{j}}^{1 / 2} P_{k} E_{y_{j}}^{1 / 2}$ .

2.1givenF1F2F6step 1.1algebra

Since $(e_{k})$ is a basis, $\sum_{k} P_{k} = I_{H}$ . Using step 1.1 and the completeness relation in [F1], $\sum_{j, k} K_{j k}^{*} K_{j k} = \sum_{j} E_{y_{j}}^{1 / 2} (\sum_{k} P_{k}) E_{y_{j}}^{1 / 2} = \sum_{j} E_{y_{j}} = I_{H}$ . Thus the finite family is trace-preserving by [F6].

3.1givenF4F6F5F7F8F11step 1.1step 2.1algebra∎

For each fixed $j$ , the $f_{j}$ output diagonal entry of $\sum_{k} K_{j k} X K_{j k}^{*}$ is $\sum_{k} ⟨ E_{y_{j}}^{1 / 2} X E_{y_{j}}^{1 / 2} e_{k}, e_{k} ⟩ = tr (E_{y_{j}}^{1 / 2} X E_{y_{j}}^{1 / 2})$ . By trace cyclicity [F7], this is $tr (X E_{y_{j}})$ , and all off-diagonal output entries vanish because each $K_{j k}$ has range in $C f_{j}$ and [F11] makes the output basis orthonormal. Summing over $j$ yields $M_{E}$ , so it has the finite Kraus representation [F4] and is completely positive by [F5]. Together with steps 1.1 and 2.1 it is a quantum channel by [F8]. The coordinate map $J f_{j} = ∣ y_{j} ⟩$ is unitary because it carries one orthonormal basis onto the other; replacing each Kraus map by $J K_{j k}$ preserves its normalization and complete positivity by [F5]–[F6]. The conjugated output is $\sum_{j} tr (X E_{y_{j}}) ∣ y_{j} ⟩ ⟨ y_{j} ∣ = \sum_{y} tr (E_{y} X) ∣ y ⟩ ⟨ y ∣$ by [F7], proving the indexed-register clause.

Depends on

Used by

Dependency tree · two levels

49 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, §2.3.1 (standard reference, not scraped)
Mark M. Wilde, From Classical to Quantum Shannon Theory, arXiv:1106.1445v8, §11.9.2 (standard reference, not scraped)