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.

The set of density operators is convex

Statement

For a nonzero finite-dimensional complex-inner-product space $H$ , the set of density operators on $H$ is convex: if $ρ, σ$ are density operators and $t \in [0, 1]$ , then $t ρ + (1 - t) σ$ is a density operator.

Facts & Assumptions

Given: Density operators $ρ, σ$ on $H$ and a real number $t$ with $0 \leq t \leq 1$ .

[F1]

Density operator: a density operator is a non-negative endomorphism with trace one.

[F2]

Ensemble and purification: a finite ensemble has finite nonnegative weights summing to one and density-operator components, and its barycenter is their weighted sum.

[F3]

Finite ensemble barycenters are density operators: the barycenter of a finite ensemble of density operators is a density operator, including zero-weight components.

Proof

1.1givenF1F2algebra

The pair of weights $(t, 1 - t)$ is nonnegative and sums to one for every $t \in [0, 1]$ , including $t = 0$ and $t = 1$ . Since $ρ, σ$ are density operators by [F1], $(t, ρ), (1 - t, σ)$ is a finite ensemble by [F2].

2.1givenF2F3step 1.1algebra∎

Its barycenter is $t ρ + (1 - t) σ$ by [F2], and is a density operator by [F3]. Thus every segment between two density operators lies in the set, so the set is convex.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

14 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 (standard reference, not scraped)
John Preskill, Quantum Computation, Chapter 2: Foundations I: States and Ensembles, §2.5.1 (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, §15.1 (standard reference, not scraped)