TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Every finite instrument induces a unique POVM

Statement

Let $(I_{a})_{a \in Ω}$ be a finite instrument from a nonzero finite-dimensional complex inner-product space $H$ to a finite-dimensional complex inner-product space $K$ . There is a unique finite POVM $(E_{a})_{a \in Ω}$ on $H$ such that ${tr}_{K} (I_{a} (X)) = {tr}_{H} (X E_{a}) (X \in L (H), a \in Ω) .$ Consequently, for every density operator $ρ$ on $H$ , the instrument probability ${tr}_{K} (I_{a} (ρ))$ equals the POVM weight ${tr}_{H} (ρ E_{a})$ .

Facts & Assumptions

Given: The finite instrument and its finite nonempty outcome set $Ω$ .

[F1]

Finite instruments and conditional states: every $I_{a} : L (H) \to L (K)$ is completely positive and $\sum_{a} {tr}_{K} (I_{a} (X)) = {tr}_{H} (X)$ for every $X$ .

[F2]

Kraus and Choi characterizations of complete positivity: every completely positive finite-dimensional map between full operator spaces has a finite Kraus representation.

[F3]

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

[F4]

Instrument branch Kraus families satisfy total normalization: for finite branch Kraus families of an instrument, $\sum_{a, j} M_{a, j}^{†} M_{a, j} = I_{H}$ .

[F5]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ and Adjoints satisfy $(S + T)^{*} = S^{*} + T^{*}$ , $(λ T)^{*} = \overline{λ} T^{*}$ , $(S T)^{*} = T^{*} S^{*}$ , and $T^{* *} = T$ : $⟨ T v, w ⟩ = ⟨ v, T^{†} w ⟩$ , $(S T)^{†} = T^{†} S^{†}$ , and $(T^{†})^{†} = T$ .

[F6]

Non-negative and positive operators: non-negativity means self-adjointness and a non-negative quadratic form.

[F7]

Finite positive effect family and Finite POVMs and their outcome law: a finite POVM is a nonempty finite family of non-negative operators summing to identity, and its outcome weights are $tr (ρ E_{a})$ .

[F8]

Trace is a linear functional on $M_{n} (F)$ and For $A \in M_{m \times n} (F)$ and $B \in M_{n \times m} (F)$ , $tr (A B) = tr (B A)$ : trace is linear and ${tr}_{K} (A B) = {tr}_{H} (B A)$ for compatible rectangular maps $A : H \to K$ , $B : K \to H$ .

[F9]

The trace pairing on a finite endomorphism space is nondegenerate: if ${tr}_{H} (A X) = 0$ for every $X \in L (H)$ , then $A = 0$ .

Proof

1.1givenF1F2F3choose

For each $a \in Ω$ , [F1] makes $I_{a}$ completely positive, so [F2] supplies a finite family $(M_{a, j})_{j}$ representing it as in [F3]. If the supplied family is empty, append one zero operator; this preserves the formula and makes each index list nonempty. Since $Ω$ is finite, the lists can be selected one at a time by finite induction; no arbitrary-index choice is used.

2.1givenstep 1.1F1F3F4algebra

Define $Φ = \sum_{a \in Ω} I_{a}$ . Concatenating the finite lists in step 1.1 gives a Kraus representation of $Φ$ . These are exactly the finite branch Kraus families of the instrument in [F1], so [F4] gives $\sum_{a, j} M_{a, j}^{†} M_{a, j} = I_{H}$ .

3.1givenstep 2.1F5F6F7algebra

For each outcome define $E_{a} = \sum_{j} M_{a, j}^{†} M_{a, j}$ . By [F5], each summand is self-adjoint and $⟨ M_{a, j}^{†} M_{a, j} x, x ⟩ = ⟨ M_{a, j} x, M_{a, j} x ⟩ \geq 0$ . Thus each $E_{a}$ is non-negative by [F6]. Step 2.1 gives $\sum_{a} E_{a} = I_{H}$ , so $(E_{a})$ is a finite POVM by [F7].

4.1givenstep 1.1step 3.1F3F8algebra

For every $X \in L (H)$ , the Kraus formula [F3], trace linearity, and rectangular cyclicity [F8] give ${tr}_{K} (I_{a} (X)) = \sum_{j} {tr}_{K} (M_{a, j} X M_{a, j}^{†}) = \sum_{j} {tr}_{H} (X M_{a, j}^{†} M_{a, j}) = {tr}_{H} (X E_{a})$ . This proves the displayed outcome-law identity for every density operator as well.

5.1givenstep 4.1F8F9algebra∎

If another family $E_{a}^{'}$ has the same identity for every $X$ , then ${tr}_{H} (X (E_{a} - E_{a}^{'})) = 0$ for all $X$ . By [F8], this equals ${tr}_{H} ((E_{a} - E_{a}^{'}) X)$ ; [F9] implies $E_{a} - E_{a}^{'} = 0$ . This holds for each $a$ , so the induced POVM is unique.

Depends on

Used by

Finite measurement branches and classical control Definition
The outcome law and outputs of a measured circuit Definition

Dependency tree · two levels

40 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 (2018 author-hosted draft), §§2.2.2 and 2.3.2 (standard reference, not scraped)
John Preskill, Quantum Computation, Chapter 3: Foundations II: Measurement and Evolution (standard reference, not scraped)