LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Faithful State Dominates Positive Operator

Statement

Let $H$ be finite-dimensional, let $σ$ be a density operator that is positive definite on $H$ , and let $X$ be a non-negative endomorphism of $H$ . Then there is a finite real $c \geq 0$ such that $X \leq c σ$ .

Facts & Assumptions

Given: A finite-dimensional complex inner-product space $H$ , a faithful density operator $σ$ , and $X \geq 0$ .

[F1]

A density operator is non-negative; faithfulness on $H$ means its restriction to $H$ is positive definite (Density operator). This current draft definition is present, but its declared existence supplier remains unresolved.

[F2]

A non-negative operator has an orthonormal eigenbasis with nonnegative eigenvalues; positive definiteness makes every eigenvalue strictly positive (A non-negative operator is equivalently self-adjoint with nonnegative eigenvalues, a positive semidefinite matrix in an orthonormal basis, or an operator of the form S^*S, Non-negative and positive operators).

[F3]

Non-negativity is characterized by nonnegative quadratic forms, so $Y \geq 0$ means $⟨ Y v, v ⟩ \geq 0$ for every $v$ (Non-negative and positive operators).

Proof

1.1givenF1F2choose

Diagonalize $X$ and let $M \geq 0$ be its largest eigenvalue; if $X = 0$ , take $M = 0$ . Diagonalize $σ$ and let $m > 0$ be its smallest eigenvalue, which is positive by faithfulness and [F2]. For every $v \in H$ , these spectral bounds give $⟨ X v, v ⟩ \leq M ∥ v ∥^{2}$ and $⟨ σ v, v ⟩ \geq m ∥ v ∥^{2}$ .

2.1step 1.1F3algebra∎

Set $c = M / m$ . Then $c$ is finite and nonnegative, and for every $v$ step 1.1 gives $⟨ (c σ - X) v, v ⟩ \geq (c m - M) ∥ v ∥^{2} = 0$ . By [F3], $c σ - X \geq 0$ , which is exactly $X \leq c σ$ . This also covers $X = 0$ with $c = 0$ .

Depends on

Used by

Singular Pair No Broadcasting Theorem

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 (standard reference, not scraped)