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.

Every finite state ensemble is obtainable from a purification

Statement

Let $(p_{a}, σ_{a})_{a = 1}^{n}$ be a finite ensemble of density operators on a nonzero finite-dimensional complex-inner-product space $H$ , with barycenter $ρ = \sum_{a} p_{a} σ_{a}$ . For every finite-dimensional auxiliary space $K$ and every purification $Ψ \in H \otimes K$ of $ρ$ , there is a finite complete effect family $(E_{a})_{a = 1}^{n}$ on $K$ such that

${Tr}_{K} ⁣ [(I_{H} \otimes \sqrt{E_{a}}) ∣ Ψ ⟩ ⟨ Ψ ∣ (I_{H} \otimes \sqrt{E_{a}})] = p_{a} σ_{a}$

for each $a$ . In particular, for a pure-state ensemble $σ_{a} = ∣ u_{a} ⟩ ⟨ u_{a} ∣$ , the corresponding output is $p_{a} ∣ u_{a} ⟩ ⟨ u_{a} ∣$ . A zero weight has $E_{a} = 0$ . The statement is a finite-dimensional operator identity and assumes no measurement postulate or outcome law.

Facts & Assumptions

Given: A finite ensemble $(p_{a}, σ_{a})$ with barycenter $ρ$ and a unit purification $Ψ \in H \otimes K$ of $ρ$ .

[F1]

Ensemble and purification: $p_{a} \geq 0$ , $\sum_{a} p_{a} = 1$ , each $σ_{a}$ is a density operator, $ρ = \sum_{a} p_{a} σ_{a}$ , and a purification has partial trace $ρ$ .

[F2]

Finite ensemble barycenters are density operators: the barycenter $ρ$ is a density operator.

[F3]

Schmidt decomposition: $Ψ = \sum_{j = 1}^{r} \sqrt{λ_{j}} e_{j} \otimes f_{j}$ for positive $λ_{j}$ and orthonormal families in $H$ and $K$ .

[F4]

Ordered tensor registers, their inner product, and wire permutations: tensor factors have a specified order and product-basis pairings are products of factor pairings.

[F5]

Partial trace over a finite tensor factor: in ordered orthonormal product bases, the partial trace over $K$ sums entries with equal auxiliary indices.

[F6]

The partial trace is characterized by the trace pairing and is basis-independent: the auxiliary basis in the partial-trace coordinate formula may be any ordered orthonormal basis of $K$ .

[F7]

Dirac Notation Conversion: the root inner product is linear in its first argument and $∣ x ⟩ ⟨ y ∣$ acts by $z \mapsto ⟨ z, y ⟩ x$ .

[F8]

Tensor products of finitely many linear maps: $I_{H} \otimes T$ sends $x \otimes y$ to $x \otimes T y$ and extends linearly.

[F9]

Density operator: every density operator is non-negative, and its support is the orthogonal complement of its kernel.

[F10]

A non-negative operator has a unique non-negative square root: a non-negative operator $T$ has a unique non-negative square root $R$ with $R^{2} = T$ .

[F11]

Finite positive effect family: a finite complete positive family consists of non-negative operators summing to identity.

[F12]

A complete positive family consists of effects: each member of such a family is an effect.

[F13]

Linear combination of a finite list, and the span $span (S)$ as the smallest linear subspace containing $S$ , The orthogonal complement $W^{⊥} = {v : ⟨ v, w ⟩ = 0 for all w \in W}$ and For a subspace $W$ of a finite-dimensional inner product space, $V = W \oplus W^{⊥}$ : the spans $S$ and $L$ are subspaces, their orthogonal complements are subspaces, and $H = S \oplus S^{⊥}$ and $K = L \oplus L^{⊥}$ .

[F14]

If $\dim_{F} V = n$ and $U$ is a linear subspace of $V$ , then $U$ is finite-dimensional, $\dim_{F} U \leq n$ , and $\dim_{F} U = n$ if and only if $U = V$ and Every finite-dimensional real or complex inner product space has an orthonormal basis: a subspace of a finite-dimensional space, including $W^{⊥}$ , is finite-dimensional and has an orthonormal basis; adjoining such a basis of $W^{⊥}$ to an orthonormal basis of $W$ gives an orthonormal basis of $V$ .

[F15]

Dirac Notation Coordinate Identity: in ordered orthonormal bases, the coordinate matrix of $∣ x ⟩ ⟨ y ∣$ is $[x] [y]^{†}$ .

[F16]

The product basis is orthonormal and tensor dimensions multiply: elementary tensors from ordered factor bases form a basis of the tensor product, so they span it.

[F17]

Coordinate columns $[v]_{B}$ and matrices $[T]_{B}^{C}$ of linear maps relative to ordered bases, Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes, The transpose $A^{T}$ of a matrix and Real and imaginary parts, complex conjugation, and modulus: operator matrices use ordered-basis coordinates, products are row-by-column sums, transpose interchanges indices, and $M^{*} = {\overline{M}}^{T}$ .

[F18]

Kernel and image of a linear map: $\ker ρ = {x \in H : ρ x = 0}$ , and $im ρ$ is the set of outputs $ρ x$ .

Proof

1.1F1F2F3F4F5F6F7F9F13F14F18algebra

By [F1]–[F2], the barycenter $ρ$ is a density operator, as required for the purification hypothesis. By [F3], write $Ψ = \sum_{j = 1}^{r} \sqrt{λ_{j}} e_{j} \otimes f_{j}$ with $λ_{j} > 0$ and orthonormal families; $r \geq 1$ because $Ψ$ is a unit vector. Set $S = span {e_{1}, \dots, e_{r}}$ and $L = span {f_{1}, \dots, f_{r}}$ . By [F13]–[F14], the complements $S^{⊥}$ and $L^{⊥}$ are finite-dimensional and have orthonormal bases; adjoining those bases completes the Schmidt families to orthonormal bases of $H$ and $K$ . The basis-independent partial-trace formula [F5]–[F6], together with [F7], gives $ρ = {Tr}_{K} (∣ Ψ ⟩ ⟨ Ψ ∣) = \sum_{j} λ_{j} ∣ e_{j} ⟩ ⟨ e_{j} ∣$ . This operator is positive with eigenvalue $λ_{j}$ on $e_{j}$ and zero on $S^{⊥}$ ; the orthogonal decomposition shows $\ker ρ = S^{⊥}$ , so the support definition [F9] and kernel definition [F18] give $S = supp (ρ)$ . The expansion of $Ψ$ shows that its auxiliary support is $L$ .

1.2F1F9F10F18algebra

If $p_{a} > 0$ and $x \in \ker ρ$ as defined in [F18], then $0 = ⟨ ρ x, x ⟩ = \sum_{b} p_{b} ⟨ σ_{b} x, x ⟩$ . Every summand is nonnegative by [F9], so $⟨ σ_{a} x, x ⟩ = 0$ . Writing $R_{a} = \sqrt{σ_{a}}$ by [F10], self-adjointness gives $⟨ σ_{a} x, x ⟩ = ⟨ R_{a} x, R_{a} x ⟩ = 0$ , hence $σ_{a} x = 0$ . Self-adjointness then gives $⟨ σ_{a} y, x ⟩ = 0$ for every $y$ , so $σ_{a} y \in S$ .

2.1F1F9step 1.1step 1.2algebra

On $S$ , define $R e_{j} = λ_{j}^{- 1 / 2} e_{j}$ and $A_{a} = p_{a} R (σ_{a} ∣_{S}) R$ when $p_{a} > 0$ ; put $A_{a} = 0$ when $p_{a} = 0$ . Each $A_{a}$ is self-adjoint because $R$ and $σ_{a} ∣_{S}$ are self-adjoint, and it is non-negative because its quadratic form is $p_{a} ⟨ σ_{a} R x, R x ⟩ \geq 0$ . Since $\sum_{a} p_{a} σ_{a} = ρ$ , one has $\sum_{a} A_{a} = R (ρ ∣_{S}) R = I_{S}$ .

3.1F1F11F12F13F14F17step 2.1constructchoosealgebra

By [F13], $K = L \oplus L^{⊥}$ ; choose an orthonormal basis of $L^{⊥}$ by [F14], so $(f_{j})$ together with that basis is an orthonormal basis of $K$ . On $L$ , define $E_{a}$ by the matrix $A_{a}^{T}$ in $(f_{j})$ and extend it by zero on $L^{⊥}$ . Since each $A_{a}$ is self-adjoint, $A_{a}^{T}$ is self-adjoint; for every coordinate vector $z$ , [F17] gives $z^{*} A_{a}^{T} z = \overline{(\overset{ˉ}{z})^{*} A_{a} \overset{ˉ}{z}} \geq 0$ , so this block is non-negative. Their sum is identity on $L$ and zero on $L^{⊥}$ . Choose $a_{0}$ with $p_{a_{0}} > 0$ , which exists since $\sum_{a} p_{a} = 1$ , and add the projection $0 \oplus I_{L^{⊥}}$ to $E_{a_{0}}$ . The resulting operators are non-negative and sum to $I_{K}$ , so [F11]–[F12] make them a complete effect family. In particular, $E_{a} = 0$ when $p_{a} = 0$ .

4.1F10F13step 3.1algebra

Let $Λ e_{j} = \sqrt{λ_{j}} e_{j}$ and $S_{a} = \sqrt{E_{a}}$ . Each $E_{a}$ is block diagonal on $L \oplus L^{⊥}$ . The direct sum of the non-negative square roots of its two blocks is a non-negative square root of $E_{a}$ , so uniqueness in [F10] shows that $S_{a}$ is block diagonal. If $B_{a}$ is the matrix of $S_{a} ∣_{L}$ in $(f_{j})$ , then $B_{a}$ is self-adjoint and $B_{a}^{2} = A_{a}^{T}$ .

5.1F3F4F7F8F16F17step 4.1algebra

Put $T_{a} = I_{H} \otimes S_{a}$ and $Φ_{a} = T_{a} Ψ$ . On elementary tensors, [F4], [F8] and self-adjointness of $S_{a}$ give $⟨ T_{a} (x \otimes y), x^{'} \otimes y^{'} ⟩ = ⟨ x \otimes y, T_{a} (x^{'} \otimes y^{'}) ⟩$ ; since elementary tensors span by [F16], $T_{a}$ is self-adjoint. By [F7], for every $z$ , $T_{a} ∣ Ψ ⟩ ⟨ Ψ ∣ T_{a} z = ⟨ T_{a} z, Ψ ⟩ T_{a} Ψ = ⟨ z, T_{a} Ψ ⟩ Φ_{a} = ∣ Φ_{a} ⟩ ⟨ Φ_{a} ∣ z$ . Thus the displayed filtered operator is the outer product of $Φ_{a}$ . In the ordered Schmidt product basis, $Ψ$ has coefficient matrix $Λ$ , and [F8] sends $e_{i} \otimes f_{j}$ to $e_{i} \otimes S_{a} f_{j}$ ; row-by-column multiplication [F17] gives coefficient matrix $C_{a} = Λ B_{a}^{T}$ on $H \otimes L$ .

6.1F1F5F7F15F16F17step 2.1step 4.1step 5.1algebra

By [F5], [F7], [F15]–[F17], the partial trace of the filtered vector's outer product has matrix $C_{a} C_{a}^{*} = Λ B_{a}^{T} \overline{B_{a}} Λ$ . Since $B_{a}$ is self-adjoint, $B_{a}^{T} = \overline{B_{a}}$ ; hence $B_{a}^{T} \overline{B_{a}} = \overline{B_{a}^{2}} = \overline{A_{a}^{T}} = A_{a}$ , the last equality using self-adjointness of $A_{a}$ . Therefore the reduced operator on $S$ is $Λ A_{a} Λ = p_{a} σ_{a} ∣_{S}$ , by the definition of $A_{a}$ and $Λ R = I_{S}$ .

7.1step 1.2step 3.1step 6.1algebra∎

If $p_{a} > 0$ , step 1.2 shows that $σ_{a}$ vanishes on $S^{⊥}$ , so the operator identity from step 6.1 extends to all of $H$ . If $p_{a} = 0$ , step 3.1 gives $E_{a} = 0$ , so the filtered vector and $p_{a} σ_{a}$ are both zero. This proves the required identity for every outcome.

Remarks

The finite mixed-ensemble statement is proved directly by the positive-matrix construction $A_{a} = p_{a} ρ_{S}^{- 1 / 2} σ_{a} ρ_{S}^{- 1 / 2}$ (written in the Schmidt basis above). Spectrally refining each $σ_{a}$ rewrites this grouped operator as a sum of rank-one terms, but summing fine-grained square-root-filter outputs alone would not prove the displayed formula for the square root of the grouped effect. The proof forms the grouped effects first and verifies their square-root filters directly. All spectral and basis selections in the proof are finite-dimensional; no arbitrary-index choice is used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

76 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.1.2–2.1.3 (standard reference, not scraped)
John Preskill, Quantum Computation, Chapter 2: Foundations I: States and Ensembles, §2.5 (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, §§15.1 and 18.3 (standard reference, not scraped)