Alphabeta Math
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.

C star spectral radius equals norm for normal elements

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let A be a unital complex C*-algebra (C star algebra, Unital Banach algebra) and let aA be normal (Self-adjoint positive unitary and normal elements). Then

r(a)  =  a,

where r(a) is the spectral radius (Spectral radius).

Facts & Assumptions

Given: An assumed Axiom of Choice, a unital complex C*-algebra A, and a normal element aA.

[L1]

xx=x2 and x=x for all xA, and the norm is submultiplicative (C star algebra).

[L2]

x is normal when xx=xx, and x is self-adjoint when x=x; a self-adjoint element is normal (Self-adjoint positive unitary and normal elements).

[L3]

Under the Axiom of Choice, r(x)=limkxk1/k=infk1xk1/k for every xA (Spectral radius formula, Spectral radius, The Axiom of Choice).

Proof

technique · direct
1.1

For every normal dA one has d2=d2: by [L1] and [L2], d22=(d2)(d2)=dddd and, since dd=dd, the element dddd=(dd)(dd)=(dd)2; so d22=(dd)2=(dd)(dd)=dd2=d4, whence d2=d2.

L1L2algebra
2.1

By induction on n0, a2n=a2n for the normal element a: the case n=0 is a=a; if a2n=a2n, then a2n is normal (a power of a normal element commutes with its adjoint, since a and a commute), so [step 1.1] applies to d=a2n and gives a2n+1=(a2n)2=a2n2=a2n+1.

step 1.1L2algebra
3.1

By [L3] the limit r(a)=limkak1/k exists, and the sequence k=2n is a strictly increasing sequence of indices, so the subsequence a2n1/2n=a converges to r(a); hence r(a)=a.

step 2.1L3algebra

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 a2na2n 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