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

Trace of a product of positive semidefinite matrices is nonnegative

Statement

If $P, Q \in C^{n \times n}$ are positive semidefinite, then $tr (P Q) \geq 0$ for every $n \geq 0$ .

Facts & Assumptions

Given: $P, Q$ are self-adjoint and have nonnegative quadratic forms on a finite-dimensional complex inner-product space.

[F1]

Non-negative and positive operators: nonnegative means self-adjoint and $⟨ T x, x ⟩ \geq 0$ for every vector $x$ .

[F2]

A non-negative operator has a unique non-negative square root: a nonnegative finite-dimensional operator has a nonnegative square root $R$ satisfying $R^{2} = P$ .

[F3]

For $A \in M_{m \times n} (F)$ and $B \in M_{n \times m} (F)$ , $tr (A B) = tr (B A)$ : $tr (U V) = tr (V U)$ for compatible finite matrices.

[F4]

The trace $tr (A)$ as the sum of the diagonal entries: trace is the finite diagonal sum, with the empty sum equal to zero.

[F5]

Real and complex inner-product spaces and their induced length: the inner product is linear in the first argument, conjugate-linear in the second, and the quadratic form of a nonnegative operator is nonnegative real.

Proof

technique · direct

1.1givenF1F2F4F5algebra

Let $R = P^{1 / 2}$ from [F2] and put $T = R Q R$ . Since $Q$ is nonnegative by [F1], self-adjointness of $R$ and the inner-product identity [F5] give $⟨ T x, x ⟩ = ⟨ Q R x, R x ⟩ \geq 0$ for every $x$ . Thus every diagonal entry $⟨ T e_{j}, e_{j} ⟩$ in an orthonormal coordinate basis is nonnegative real; summing by [F4] gives $tr (T) \geq 0$ . This also holds in dimension zero because the trace is the empty sum.

2.1givenF3step 1.1algebra∎

Since $P = R^{2}$ , [F3] applied to $U = R$ and $V = R Q$ gives $tr (P Q) = tr (R (R Q)) = tr ((R Q) R) = tr (R Q R) = tr (T) \geq 0$ by step 1.1.

Depends on

Used by

Dependency tree · two levels

16 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

Joran van Apeldoorn et al., Quantum SDP-solvers: Better upper and lower bounds (standard reference, not scraped)