ExampleConstruction: AI-generatedVerification: 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.

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.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

53 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.3, Example 2.8 (standard reference, not scraped)
John Preskill, Quantum Computation, Chapter 2: Foundations I: States and Ensembles, §2.4 (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, §18.3 (standard reference, not scraped)