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.
C star spectral radius equals norm for normal elements
Statement
Assume the Axiom of Choice (The Axiom of Choice). Let be a unital complex C*-algebra (C star algebra, Unital Banach algebra) and let be normal (Self-adjoint positive unitary and normal elements). Then
where is the spectral radius (Spectral radius).
Facts & Assumptions
Given: An assumed Axiom of Choice, a unital complex C*-algebra , and a normal element .
and for all , and the norm is submultiplicative (C star algebra).
is normal when , and is self-adjoint when ; a self-adjoint element is normal (Self-adjoint positive unitary and normal elements).
Under the Axiom of Choice, for every (Spectral radius formula, Spectral radius, The Axiom of Choice).
Proof
For every normal one has : by [L1] and [L2], and, since , the element ; so , whence .
By induction on , for the normal element : the case is ; if , then is normal (a power of a normal element commutes with its adjoint, since and commute), so [step 1.1] applies to and gives .
By [L3] the limit exists, and the sequence is a strictly increasing sequence of indices, so the subsequence converges to ; hence .
Remarks
- No continuous functional calculus is used, and no assumption that the spectrum is real is made: the whole content is the C*-identity plus the spectral radius formula.
- The normality hypothesis is exactly what makes the power norms a subsequence of geometric form: for a general element only holds, and the limit can be strictly smaller.
Depends on
Used by
Dependency tree · two levels
24 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
- Vahid Shirbisheh, Lectures on C-star Algebras, v2 — Lemma 3.1.30 and Proposition 3.1.32, printed pp. 64–65 (standard reference, not scraped)
- Dana P. Williams, Lecture Notes on the Spectral Theorem — §4, printed pp. 9–11 (standard reference, not scraped)