Pipeline-generated

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.

Pure and Mixed States, Ensembles, and Schmidt Decomposition — Examples

1 · Prerequisites

2 · Summary

The Bell vector is already a two-term Schmidt form: its positive coefficients are both $1 / \sqrt{2}$ and each factor family is an ordered orthonormal basis. Expanding its outer product and contracting either factor gives $I_{2} / 2$ , checking the tensor order and partial-trace index convention directly. The example also shows that this density operator has two distinct equal-weight ensemble decompositions, in the computational and ${∣ + ⟩, ∣ - ⟩}$ bases; see Bell-state Schmidt decomposition and reduced density.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedjudge pass (gpt-6-luna)Open item page →

Bell-state Schmidt decomposition and reduced density

Statement

For $H = K = C^{2}$ with ordered standard bases $e_{0}, e_{1}$ , the Bell vector $Ψ = (e_{0} \otimes e_{0} + e_{1} \otimes e_{1}) / \sqrt{2}$ is already in Schmidt form: it is a finite sum $\sum_{j} s_{j} u_{j} \otimes v_{j}$ with positive coefficients and orthonormal families in both factors, here $s_{0} = s_{1} = 1 / \sqrt{2}$ and $u_{j} = v_{j} = e_{j}$ . Its reduced state on either factor is $I_{2} / 2$ .

Example

The product-basis coordinates make the two product terms orthogonal, and the partial trace removes the two off-diagonal cross terms. Both reductions are therefore maximally mixed on the two-dimensional factor. The same state $I_{2} / 2$ is also the barycenter of either the equal-weight computational-basis projectors or the equal-weight ${∣ + ⟩, ∣ - ⟩}$ projectors, giving two distinct ensemble descriptions of one density operator.

Facts & Assumptions

Given: $H = K = C^{2}$ , their ordered standard bases, and tensor order $H$ then $K$ .

[F1]

The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ : the two standard coordinate vectors $e_{0}, e_{1}$ form the ordered standard basis of $C^{2}$ .

[F2]

The standard formulas $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ and $\sum_{k < n} x_{k} \overline{y_{k}}$ on $C^{n}$ are inner products: $⟨ z, w ⟩ = \sum_{r < 2} z_{r} \overline{w_{r}}$ on $C^{2}$ , so $e_{0}, e_{1}$ are orthonormal.

[F3]

Ordered tensor registers, their inner product, and wire permutations: the ordered product basis has product pairings, and a factor permutation maps each basis tensor to the tensor with reordered factors.

[F4]

Partial trace over a finite tensor factor: the partial trace over the second factor sums matrix entries with equal auxiliary indices.

[F5]

Dirac Notation Conversion: $∣ x ⟩ ⟨ y ∣$ acts by $z \mapsto ⟨ z, y ⟩ x$ .

[F6]

Ray-to-projector is well-defined and bijective and Density operator: for each unit vector $v$ , $P_{v} = ∣ v ⟩ ⟨ v ∣$ is a density operator.

[F7]

Ensemble and purification: a finite list of density operators with nonnegative weights summing to one is an ensemble, and its barycenter is the weighted operator sum.

[F8]

The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ and Every nonzero finite-dimensional complex inner-product space admits a density operator: the standard basis gives $\dim C^{2} = 2$ , so $I_{2} / 2$ is a density operator on $C^{2}$ .

Verification

1.1givenF1F2F3algebra

By [F1]–[F2], $e_{0}, e_{1}$ are an ordered orthonormal basis. Taking $u_{j} = e_{j}$ and $v_{j} = e_{j}$ for $j = 0, 1$ , the displayed expression for $Ψ$ is a finite sum with positive coefficients $s_{0} = s_{1} = 1 / \sqrt{2}$ and orthonormal families in both factors. The product basis from [F3] is orthonormal, so $∥ Ψ ∥^{2} = \frac{1}{2} (1 + 1) = 1$ . Hence this expression is a Schmidt form by the finite-sum definition in the statement.

1.2givenF1F2F3F4F5algebra

Expanding the outer product using [F5] gives $∣ Ψ ⟩ ⟨ Ψ ∣ = \frac{1}{2} (∣ e_{0} e_{0} ⟩ ⟨ e_{0} e_{0} ∣ + ∣ e_{0} e_{0} ⟩ ⟨ e_{1} e_{1} ∣ + ∣ e_{1} e_{1} ⟩ ⟨ e_{0} e_{0} ∣ + ∣ e_{1} e_{1} ⟩ ⟨ e_{1} e_{1} ∣)$ . Contracting the second factor by [F4] kills the cross terms and leaves $\frac{1}{2} (∣ e_{0} ⟩ ⟨ e_{0} ∣ + ∣ e_{1} ⟩ ⟨ e_{1} ∣) = I_{2} / 2$ .

2.1F1F2F3F4F5step 1.2algebra

The factor permutation in [F3] sends $e_{0} \otimes e_{0}$ and $e_{1} \otimes e_{1}$ to themselves, so the reordered vector has the same expression as $Ψ$ . Apply [F4] to trace its second factor, now the original $H$ factor; the same contraction as in step 1.2 gives $\frac{1}{2} (∣ e_{0} ⟩ ⟨ e_{0} ∣ + ∣ e_{1} ⟩ ⟨ e_{1} ∣) = I_{2} / 2$ on the original $K$ .

3.1givenF1F2F5F6F7F8algebra∎

Set $∣ + ⟩ = (e_{0} + e_{1}) / \sqrt{2}$ and $∣ - ⟩ = (e_{0} - e_{1}) / \sqrt{2}$ , and write $P_{v} = ∣ v ⟩ ⟨ v ∣$ for $v = e_{0}, e_{1}, +, -$ . These vectors are unit by [F1]–[F2], so [F6] makes their projectors density operators. By [F7], the pairs $(\frac{1}{2}, P_{e_{0}}), (\frac{1}{2}, P_{e_{1}})$ and $(\frac{1}{2}, P_{+}), (\frac{1}{2}, P_{-})$ are finite ensembles. Expanding the outer products with [F5] gives $P_{+} + P_{-} = P_{e_{0}} + P_{e_{1}}$ . Since $(e_{0}, e_{1})$ is an orthonormal basis by [F1]–[F2], each $z \in C^{2}$ satisfies $z = ⟨ z, e_{0} ⟩ e_{0} + ⟨ z, e_{1} ⟩ e_{1}$ , so $P_{e_{0}} + P_{e_{1}} = I_{2}$ . Both ensemble barycenters are therefore $I_{2} / 2$ , which is a density operator by [F8]. The ensembles are distinct because $P_{e_{0}}$ and $P_{+}$ have different one-dimensional ranges. Thus the same density operator has two ensemble descriptions.