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

A finite instrument has an isometric coherent record

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$ . Fix an order on its finite nonempty outcome set $Ω$ , with $m = ∣ Ω ∣$ . There are a common integer $r \geq 1$ and Kraus families $(M_{a, j})_{0 \leq j < r}$ , padding shorter families by zero operators, such that $\sum_{a \in Ω} \sum_{j < r} M_{a, j}^{†} M_{a, j} = I_{H} .$ Let $E = Q_{m} \otimes Q_{r}$ with its ordered product basis $(e_{a} \otimes f_{j})_{a, j}$ , and define $V x : = \sum_{a \in Ω} \sum_{j < r} M_{a, j} x \otimes e_{a} \otimes f_{j} \in K \otimes E .$ Then $V$ is a linear isometry. Let $Π_{a}$ be the projection on $E$ which keeps exactly the basis vectors $e_{a} \otimes f_{j}$ . For every $X \in L (H)$ , ${Tr}_{E} ⁣ ((I_{K} \otimes Π_{a}) V X V^{†} (I_{K} \otimes Π_{a})) = I_{a} (X) .$ The first record register stores the observed outcome $a$ ; the second index $j$ is hidden environment data.

Facts & Assumptions

Given: A finite instrument, its nonempty finite outcome set $Ω$ , a fixed ordering of $Ω$ , and its input and output spaces $H, K$ .

[F1]

Finite instruments and conditional states: every outcome map is completely positive, and the sum of its output traces equals the input trace for every input operator.

[F2]

Kraus and Choi characterizations of complete positivity: every finite-dimensional completely positive map $L (H) \to L (K)$ 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]

Finite registers and their ordered computational bases: for positive integers $m, r$ , $Q_{m}$ and $Q_{r}$ have ordered orthonormal bases indexed by their levels.

[F6]

Ordered tensor registers, their inner product, and wire permutations: the ordered tensor product has the product inner product, so the basis $(e_{a} \otimes f_{j})$ is orthonormal.

[F7]

Finite projective measurements: a finite family of pairwise orthogonal self-adjoint projections summing to identity is a projective measurement.

[F8]

Tensor products of finitely many linear maps: tensor maps act on elementary tensors by applying each factor map in its factor.

[F9]

Partial trace over a finite tensor factor: the partial trace over a finite basis of the second factor sums the diagonal second-factor matrix entries.

[F10]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ : $⟨ M x, y ⟩ = ⟨ x, M^{†} y ⟩$ , using the repository first-linear convention.

[F11]

Every linear map between finite-dimensional inner product spaces has a unique adjoint: every map between finite-dimensional inner-product spaces has a unique adjoint, so $V^{†}$ is defined.

[F12]

A finite instrument with nonzero input has nonzero output space: existence of a finite instrument from nonzero $H$ forces its finite-dimensional output space $K$ to be nonzero.

[F13]

Dirac Notation Conversion: the rank-one map $∣ u ⟩ ⟨ v ∣$ sends $z$ to $⟨ z, v ⟩ u$ in the repository's first-linear convention.

Proof

1.1givenF1F2F3F12choose

By [F12], $K$ is nonzero. For each $a \in Ω$ , complete positivity in [F1] and [F2] supplies a finite Kraus family for $I_{a}$ as in [F3]. Let $r$ be the maximum of their finitely many lengths and $1$ ; append zero operators to shorter lists until every list has length $r$ . These finitely many choices are made successively over $Ω$ , so no choice axiom is used.

1.2givenF5F6F7F8construct

Define $P_{a} e_{b} = e_{b}$ if $b = a$ and $0$ otherwise on $Q_{m}$ , and put $Π_{a} = P_{a} \otimes I_{Q_{r}}$ . The basis definitions show $P_{a}$ is self-adjoint and idempotent, the $P_{a}$ are pairwise orthogonal and sum to $I_{Q_{m}}$ , so [F7] makes them a projective measurement. By [F8], $Π_{a} (e_{b} \otimes f_{j})$ equals $e_{b} \otimes f_{j}$ if $b = a$ and $0$ otherwise; since these basis vectors are orthonormal and span $E$ , $Π_{a}$ is the orthogonal projection onto the subspace with observed label $a$ .

2.1givenstep 1.1F4F5algebra

The branch families in step 1.1 are the instrument's finite branch Kraus families, so [F4] gives $\sum_{a, j < r} M_{a, j}^{†} M_{a, j} = I_{H}$ . Since $m, r \geq 1$ , the registers in [F5] exist.

3.1givenstep 2.1F6F10construct

For $x, y \in H$ , orthogonality of the product record basis [F6] and the adjoint identity [F10] give $⟨ V x, V y ⟩ = \sum_{a, j} ⟨ M_{a, j} x, M_{a, j} y ⟩ = \sum_{a, j} ⟨ x, M_{a, j}^{†} M_{a, j} y ⟩ = ⟨ x, y ⟩$ by step 2.1. Thus the finite sum defines a linear isometry.

4.1givenstep 1.1step 1.2F3F8F9F11F13algebra∎

The adjoint $V^{†}$ in the claimed operator identity exists by [F11]. Expanding the isometry gives $V X V^{†} = \sum_{b, c \in Ω} \sum_{j, k < r} M_{b, j} X M_{c, k}^{†} \otimes ∣ e_{b} \otimes f_{j} ⟩ ⟨ e_{c} \otimes f_{k} ∣ .$ Applying $I_{K} \otimes Π_{a}$ on both sides kills terms unless $b = c = a$ . The partial-trace formula [F9] then keeps only the diagonal hidden entries $j = k$ , leaving $\sum_{j < r} M_{a, j} X M_{a, j}^{†} = I_{a} (X)$ by [F3]. The rank-one record operators have the action specified by [F13]. Thus only $a$ is recorded as the outcome; $j$ is traced out.

Depends on

Used by

Finite instruments can be coherently deferred Theorem

Dependency tree · two levels

47 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)