LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-22

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.

Spectrum of a positive operator is nonnegative

Statement

Assume Countable Choice. If $T$ is a bounded positive operator on a nonzero complex Hilbert space, then $σ (T) \subseteq [0, + \infty)$ .

Facts & Assumptions

[A1]

$T$ is positive when $⟨ T x, x ⟩$ is a real number in $[0, + \infty)$ for every $x$ ; positivity is a condition on the values of the quadratic form and does not presuppose self-adjointness (Self-adjoint, positive, unitary and normal operators).

[A2]

$⟨ T^{*} x, y ⟩ = ⟨ x, T y ⟩$ , and for a fixed $w$ the expansion of $⟨ T x, x ⟩$ at $x + t y$ uses the linear/conjugate-linear inner-product conventions (The Hilbert-space adjoint of a bounded operator, Real and complex inner-product spaces and their induced length). The adjoint algebra laws give $(T - z I)^{*} = T^{*} - \overline{z} I$ (Hilbert-adjoint identities).

[A3]

$∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ for all vectors $u, v$ (Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs).

[A4]

$λ \in ρ (T)$ exactly when $λ I - T$ is bijective with bounded inverse; $σ (T)$ is the complement of $ρ (T)$ (Spectrum and resolvent of a bounded operator).

[A5]

$(ran S)^{⊥} = \ker S^{*}$ and $\overline{ran S} = (\ker S^{*})^{⊥}$ for every bounded $S$ (Kernel–range orthogonality for Hilbert adjoints).

[A6]

$S^{⊥} = {v : ⟨ v, s ⟩ = 0 \forall s \in S}$ and ${0}^{⊥} = H$ (Orthogonality and the orthogonal complement).

[A7]

A Hilbert space is complete for its induced norm; $z = Re z + i Im z$ and $z \notin [0, + \infty)$ means $Im z \neq 0$ or $Re z < 0$ (Hilbert space, Real and imaginary parts, complex conjugation, and modulus, The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

[A8]

Countable Choice is the hypothesis of the adjoint and orthogonality suppliers used below (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · direct

Given: A nonzero complex Hilbert space $H$ , a bounded positive operator $T \in B (H)$ and a scalar $z$ outside $[0, + \infty)$ .

1.1

For $x = 0$ the lower bounds below are immediate. For $x \neq 0$ the number $r : = ⟨ T x, x ⟩ / ∥ x ∥^{2}$ is real and nonnegative, so writing $z = a + b i$ one has $∣ ⟨ (T - z I) x, x ⟩ ∣ = ∣ r - z ∣ ∥ x ∥^{2}$ with $∣ r - z ∣ \geq ∣ b ∣$ always and $∣ r - z ∣ = r + ∣ a ∣ \geq ∣ a ∣$ when $b = 0$ and $a < 0$ .

A1A7algebra

1.2

If $(T^{*} - z I) x = 0$ with $x \neq 0$ , then testing against $x$ and using the adjoint identity gives $⟨ T x, x ⟩ = ⟨ x, T^{*} x ⟩ = \overline{z} ∥ x ∥^{2}$ ; the left side is a nonnegative real number while $z \notin [0, + \infty)$ makes $\overline{z} ∥ x ∥^{2}$ non-real or negative, so $\ker (T^{*} - z I) = {0}$ .

A1A2A7algebra

2.1

If $z \notin R$ then $∥ (T - z I) x ∥ \geq ∣ Im z ∣ ∥ x ∥$ by the estimate and Cauchy–Schwarz, and the same lower bound with $∣ Re z ∣$ holds when $z$ is real and negative; in either case there is $c > 0$ with $∥ (T - z I) x ∥ \geq c ∥ x ∥$ , so $T - z I$ is injective. Its range is closed: if $(T - z I) x_{n} \to u$ , the inequality makes $(x_{n})$ Cauchy, completeness gives $x_{n} \to x$ , and boundedness gives $(T - z I) x = u$ .

step 1.1A3A7algebra

3.1

For such $z$ the orthogonal complement of $ran (T - z I)$ is $\ker (T^{*} - \overline{z} I) = {0}$ , the vanishing being step 1.2 applied to the scalar $\overline{z}$ , which also lies outside $[0, + \infty)$ ; the closed range equals its closure, so $ran (T - z I) = H$ .

step 2.1step 1.2A2A5A6A8

4.1

Hence every $z \notin [0, + \infty)$ lies in $ρ (T)$ : $T - z I$ is bijective with bounded inverse, and its inverse has norm at most $1 / c$ by step 2.1; changing sign gives the bounded inverse of $z I - T$ . Thus $σ (T) \subseteq [0, + \infty)$ .

step 2.1step 3.1A4A7∎

Depends on

Used by

Continuous functional calculus properties Theorem
Positive square root Theorem
Self adjoint norm and spectrum extrema Theorem

Dependency tree · two levels

40 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

Theo Bühler and Dietmar Salamon, Functional Analysis, Lemma 5.49, printed pp.238–240 (standard reference, not scraped)
Dana P. Williams, Lecture Notes on the Spectral Theorem, §4, pp.10–13 (standard reference, not scraped)