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

Nonunique mixed ensemble

Example

On $H = C^{2}$ with the standard inner product and orthonormal basis $e_{1} = (\binom{1}{0})$ , $e_{2} = (\binom{0}{1})$ , put $e_{\pm} : = \frac{1}{\sqrt{2}} (e_{1} \pm e_{2})$ (Density operators and scalar spectral probability). Then the maximally mixed density operator $\frac{1}{2} I$ admits the two orthonormal convex decompositions

$\frac{1}{2} I = \frac{1}{2} T_{e_{1}, e_{1}} + \frac{1}{2} T_{e_{2}, e_{2}} = \frac{1}{2} T_{e_{+}, e_{+}} + \frac{1}{2} T_{e_{-}, e_{-}},$

where $(e_{1}, e_{2})$ and $(e_{+}, e_{-})$ are distinct orthonormal bases of $H$ . Thus the same density operator has two distinct orthonormal convex decompositions into rank-one density operators.

Facts & Assumptions

Given: $H = C^{2}$ with the standard inner product; the orthonormal basis $(e_{1}, e_{2})$ ; the unit vectors $e_{\pm}$ ; the operators $T_{u, v} x = ⟨ x, v ⟩ u$ .

[A1]

A density operator is a self-adjoint positive trace-class operator with trace $1$ (Density operators and scalar spectral probability(a), definition only). For a finite family of unit vectors $u_{j} i n m a t h b b C^{2}$ and weights $w_{j} g e 0$ with $s u m_{j} w_{j} = 1$ , set $h o : = s u m_{j} w_{j} u_{j} u_{j}^{*}$ . This is a finite matrix and hence trace class; it is self-adjoint, $x^{*} h o x = s u m_{j} w_{j} ∣ u_{j}^{*} x ∣^{2} g e 0$ , and its finite trace is $s u m_{j} w_{j} s u m_{k = 1}^{2} ∣ (u_{j})_{k} ∣^{2} = s u m_{j} w_{j} = 1$ . Thus it is a density operator even without orthogonality. This is a local finite-matrix calculation, not an invocation of the supplier's Countable Choice expansion.

[A2]

$T_{u, v}$ is trace class with $tr (T_{u, v}) = ⟨ u, v ⟩$ and $∥ T_{u, v} ∥_{1} = ∥ u ∥ ∥ v ∥$ ; the trace is linear on trace-class operators (Rank-one operator calculus). In the present $H = C^{2}$ these facts follow directly from $T_{u, v} = u v^{*}$ : the diagonal sum is $\sum_{k} u_{k} \overline{v_{k}} = ⟨ u, v ⟩$ , and $(u v^{*})^{*} (u v^{*}) = ∥ u ∥^{2} v v^{*}$ has at most one nonzero eigenvalue, $∥ u ∥^{2} ∥ v ∥^{2}$ , so its singular-value sum is $∥ u ∥ ∥ v ∥$ . Finite diagonal sums are linear. No choice principle is used in these finite computations.

[A3]

In an orthonormal basis of $C^{2}$ the matrix of $T_{u, v}$ is the column-times-row matrix $u v^{*}$ ; $T_{e_{1}, e_{1}}$ and $T_{e_{2}, e_{2}}$ therefore have matrices $(\begin{array}{cc} 1 & 0 \\ 0 & 0 \end{array})$ and $(\begin{array}{cc} 0 & 0 \\ 0 & 1 \end{array})$ .

Verification

1.1A1A2A3algebra

[Computational basis decomposition] By [A3], $\frac{1}{2} T_{e_{1}, e_{1}} + \frac{1}{2} T_{e_{2}, e_{2}}$ has matrix $\frac{1}{2} (\begin{array}{cc} 1 & 0 \\ 0 & 0 \end{array}) + \frac{1}{2} (\begin{array}{cc} 0 & 0 \\ 0 & 1 \end{array}) = \frac{1}{2} I$ , and by [A2] it is a trace-class operator of trace $\frac{1}{2} + \frac{1}{2} = 1$ ; by [A1] it is a density operator coming from the orthonormal family $(e_{1}, e_{2})$ with weights $\frac{1}{2}, \frac{1}{2}$ .

2.1step 1.1A1A3algebra

[Fixed $\pm$ basis decomposition] The vectors $e_{\pm} = \frac{1}{\sqrt{2}} (e_{1} \pm e_{2})$ are unit and orthogonal since $⟨ e_{+}, e_{-} ⟩ = \frac{1}{2} (⟨ e_{1}, e_{1} ⟩ - ⟨ e_{1}, e_{2} ⟩ + ⟨ e_{2}, e_{1} ⟩ - ⟨ e_{2}, e_{2} ⟩) = 0$ ; their matrices are $T_{e_{+}, e_{+}} = \frac{1}{2} (\begin{array}{cc} 1 & 1 \\ 1 & 1 \end{array})$ and $T_{e_{-}, e_{-}} = \frac{1}{2} (\begin{array}{cc} 1 & - 1 \\ - 1 & 1 \end{array})$ , so $\frac{1}{2} T_{e_{+}, e_{+}} + \frac{1}{2} T_{e_{-}, e_{-}} = \frac{1}{2} I$ again, with weights $\frac{1}{2}, \frac{1}{2}$ on an orthonormal family; thus the same operator $\frac{1}{2} I$ has a second decomposition.

3.1step 1.1step 2.1A1algebra∎

[The decompositions are different] The two orthonormal families are distinct: $∣ ⟨ e_{1}, e_{+} ⟩ ∣ = \frac{1}{\sqrt{2}} \notin {0, 1}$ , so $e_{1}$ is not a scalar multiple of $e_{\pm}$ and $T_{e_{1}, e_{1}}$ is not one of $T_{e_{\pm}, e_{\pm}}$ (their matrices of step 2.1 differ from $(\begin{array}{cc} 1 & 0 \\ 0 & 0 \end{array})$ ); hence the two lists of rank-one density operators are not the same up to reordering, while both convex combinations equal the single operator $\frac{1}{2} I$ by steps 1.1 and 2.1. Therefore this density operator has a nonunique orthonormal convex decomposition into rank-one density operators, consistent with the expansion in [A1].

Remarks

The operator identity is basis-independent. Both decompositions define the same matrix $ρ = \frac{1}{2} I$ , so $tr (ρ A) = \frac{1}{2} tr A$ for every endomorphism $A$ of $H$ .
Nonuniqueness needs no optimization. The two decompositions here are already orthonormal and vary only in the choice of basis; no operational preparation procedure is specified.

Nonunique mixed ensemble

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources