LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

State values at self-adjoint elements lie in the spectral interval

Statement

Assume the Axiom of Choice. Let $A$ be a C*-algebra, let $a = a^{*} \in A$ and let $ω$ be a state of $A$ (States and positive functionals on a C star algebra). Then $\min σ (a) \leq ω (a) \leq \max σ (a),$ where the spectrum is computed in $A$ if $A$ is unital and in its minimal unitization otherwise (Minimal C star unitization).

Facts & Assumptions

Given: AC; a C*-algebra $A$ with ambient unital C*-algebra $B$ ( $B = A$ if $A$ is unital, $B = A^{+}$ otherwise); a self-adjoint $a \in A$ ; a state $ω$ of $A$ .

[F1]

Positive functionals satisfy Cauchy–Schwarz: $∣ ω (b^{*} c) ∣^{2} \leq ω (c^{*} c) ω (b^{*} b)$ ; states have norm $1$ , so $∣ ω (x) ∣ \leq ∥ x ∥$ and $ω (x^{*} x) \geq 0$ (States and positive functionals on a C star algebra).

[F2]

$A$ has a two-sided approximate unit $(u_{λ})$ of positive contractions, so $u_{λ} x \to x$ and $∥ u_{λ} ∥ \leq 1$ (Positive contractive approximate units for C star algebras and ideals).

[F3]

Positivity/order and calculus: for self-adjoint $x$ , $σ (x) \subseteq R$ and $∥ x ∥ = \max ∣ σ (x) ∣$ ; $a \geq 0$ iff $σ (a) \subseteq [0, \infty)$ ; the positive elements form a cone; $0 \leq x \leq y$ implies $∥ x ∥ \leq ∥ y ∥$ ; the continuous calculus makes $a - m 1$ and $M 1 - a$ positive for $m = \min σ (a)$ , $M = \max σ (a)$ ; the unitization is a unital C*-algebra containing $A$ (Positive calculus and order estimates in a C star algebra, Minimal C star unitization, C star algebra).

Proof

technique · direct

Given: AC, a C*-algebra $A$ , a self-adjoint $a \in A$ and a state $ω$ .

1.1F1F2

For every $x \in A$ one has $ω (x^{*}) = \overline{ω (x)}$ . Indeed, for $z \in C$ the element $(u_{λ} + z x)^{*} (u_{λ} + z x) = u_{λ}^{2} + z u_{λ} x + \overline{z} x^{*} u_{λ} + ∣ z ∣^{2} x^{*} x$ is positive, so $P (z) : = ω (u_{λ}^{2}) + z ω (u_{λ} x) + \overline{z} ω (x^{*} u_{λ}) + ∣ z ∣^{2} ω (x^{*} x) \geq 0$ for all $z$ ; taking $z = 1$ and $z = i$ shows $ω (u_{λ} x) + ω (x^{*} u_{λ}) \in R$ and $ω (u_{λ} x) - ω (x^{*} u_{λ}) \in i R$ , hence $ω (x^{*} u_{λ}) = \overline{ω (u_{λ} x)}$ . Since $x^{*} u_{λ} = (u_{λ} x)^{*}$ and both $u_{λ} x \to x$ and $x^{*} u_{λ} \to x^{*}$ in norm by [F2], boundedness of $ω$ gives the claim in the limit.

1.2F1F2

For every $x \in A$ one has $∣ ω (x) ∣^{2} \leq ω (x^{*} x)$ . Indeed, Cauchy–Schwarz [F1] applied to $(b, c) = (u_{λ}, x)$ gives $∣ ω (u_{λ} x) ∣^{2} \leq ω (x^{*} x) ω (u_{λ}^{2})$ ; now $ω (u_{λ}^{2}) \leq ∥ u_{λ}^{2} ∥ \leq 1$ by [F1] and [F2], and $ω (u_{λ} x) \to ω (x)$ .

2.1F1F3step 1.1step 1.2

The canonical extension $ω^{+} (x + z 1) : = ω (x) + z$ is a positive linear functional on $B = A^{+}$ with $ω^{+} (1) = 1$ . Linearity and unitality are immediate. Every element of $A^{+}$ is $x + z 1$ , and $(x + z 1)^{*} (x + z 1) = x^{*} x + \overline{z} x + z x^{*} + ∣ z ∣^{2} 1$ , so steps 1.1 and 1.2 give $ω^{+} ((x + z 1)^{*} (x + z 1)) = ω (x^{*} x) + 2 Re (z \overline{ω (x)}) + ∣ z ∣^{2} \geq ∣ ω (x) ∣^{2} - 2 ∣ z ∣ ∣ ω (x) ∣ + ∣ z ∣^{2} = (∣ ω (x) ∣ - ∣ z ∣)^{2} \geq 0$ ; positivity extends to sums of such squares by linearity. When $A$ is unital, the order estimate $x^{*} x \leq ∥ x ∥^{2} 1$ and Cauchy--Schwarz give $∣ ω (x) ∣^{2} \leq ω (1) ω (x^{*} x) \leq ω (1)^{2} ∥ x ∥^{2}$ . Therefore $1 = ∥ ω ∥ \leq ω (1) \leq ∥ ω ∥ ∥ 1 ∥ = 1$ , so $ω (1) = 1$ . In this case take $B = A$ and $ω^{+} = ω$ .

3.1F1F3step 2.1

The unital positive functional $ω^{+}$ satisfies $∣ ω^{+} (x) ∣^{2} \leq ∥ x ∥^{2}$ for every $x \in B$ : by [F3], $x^{*} x \leq ∥ x^{*} x ∥ 1 = ∥ x ∥^{2} 1$ and positivity of $ω^{+}$ gives $ω^{+} (x^{*} x) \leq ∥ x ∥^{2} ω^{+} (1) = ∥ x ∥^{2}$ ; Cauchy–Schwarz [F1] with the unit gives $∣ ω^{+} (x) ∣^{2} \leq ω^{+} (1) ω^{+} (x^{*} x) \leq ∥ x ∥^{2}$ . In particular $ω^{+}$ is bounded with norm $1$ .

3.2F3step 2.1

Write $m : = \min σ (a)$ and $M : = \max σ (a)$ , finite real numbers by [F3]. The calculus makes $a - m 1$ and $M 1 - a$ positive elements of $B$ , hence algebraically positive by [F3]; positivity of $ω^{+}$ from step 2.1 therefore gives $ω^{+} (a - m 1) = ω (a) - m \geq 0$ and $ω^{+} (M 1 - a) = M - ω (a) \geq 0$ . Thus $m \leq ω (a) \leq M$ , and in particular $ω (a)$ is real.

4.1givenF2F3∎

The Axiom of Choice is inherited from the approximate-unit, calculus and unitization suppliers of [F1]–[F3]; the extension and spectral arguments add no further choice (The Axiom of Choice).

Depends on

Used by

States of a concretely represented C star algebra are weak star limits of finite sums of vector states Lemma

Dependency tree · two levels

27 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

Bachir Bekka and Pierre de la Harpe, Unitary Representations of Groups, Duals, and Characters (arXiv:1912.07262v1, 16 December 2019) (standard reference, not scraped)
Bachir Bekka, Pierre de la Harpe and Alain Valette, Kazhdan's Property (T) (Cambridge University Press 2008; author-hosted complete text) (standard reference, not scraped)