Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-28
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.

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

Statement

Let V be a finite-dimensional real or complex inner product space and let T:V→V be linear. The following are equivalent:

  1. T is non-negative.
  2. T is self-adjoint and every eigenvalue of T is a nonnegative real number.
  3. Some orthonormal basis makes the matrix of T diagonal with nonnegative real diagonal entries.
  4. There exists a linear map S:V→V such that T=S∗S.

Facts & Assumptions

Given: A finite-dimensional real or complex inner product space V and a linear endomorphism T:V→V.

[L1]

A self-adjoint operator on a finite-dimensional real inner product space has an orthonormal eigenbasis (Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis).

[L2]

A normal operator on a finite-dimensional complex inner product space has an orthonormal eigenbasis (Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely).

[L3]

Every nonnegative real number has a unique nonnegative square root (Square roots exist: a unique a≥0 with (a)2=a; the positives are {x2:x≠0}).

Proof

technique · direct
1.1L1L2algebra

Assume T is non-negative. Then T is self-adjoint by Non-negative and positive operators. If V is real, [L1] gives an orthonormal eigenbasis; if V is complex, the identity T=T∗ yields TT∗=T∗T, so [L2] gives an orthonormal eigenbasis. For any eigenvector v≠0 with Tv=λv, the equality ⟨Tv,v⟩=λ∥v∥2 and non-negativity give λ≥0, and self-adjointness makes λ real. Thus claim 1 implies claim 2.

1.2L3algebra

Assume claim 3. If the diagonal entries are λ1,…,λn≥0, then [L3] gives square roots λj≥0; the diagonal operator S with diagonal entries λj satisfies S∗S=T. Thus claim 3 implies claim 4.

2.1step 1.1

In the orthonormal eigenbasis from step 1.1, the matrix of T is diagonal with those nonnegative real eigenvalues on the diagonal. Thus claim 2 implies claim 3.

3.1algebra∎

Assume claim 4, so T=S∗S. Then for every v∈V one has ⟨Tv,v⟩=⟨S∗Sv,v⟩=⟨Sv,Sv⟩≥0, and for all u,v one has ⟨Tu,v⟩=⟨Su,Sv⟩=⟨u,Tv⟩. Hence T is self-adjoint and non-negative. Thus claim 4 implies claim 1.

Depends on

Used by

Dependency tree · two levels

20 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