Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 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.

Continuous functional calculus for bounded self adjoint operators

Statement

Assume AC. For a bounded self-adjoint operator T on a nonzero complex Hilbert space there is a unique isometric unital star-homomorphism C(σ(T))B(H), ff(T), sending the coordinate function z to T, with range C(I,T).

Facts & Assumptions

[A1]

For T=T and a complex polynomial p one has p(T)=maxλσ(T)p(λ), restriction classes of polynomials on σ(T) are well defined, and the class map is isometric (Polynomial calculus is isometric for self adjoint operators).

[A2]

σ(T)R for self-adjoint T, and σ(T) is nonempty and compact: B(H) is a unital complex Banach algebra, the operator spectrum agrees with the spectrum in B(H) by the bounded inverse theorem, and spectra in nonzero unital Banach algebras are nonempty and compact (Spectrum of a self adjoint operator is real, Bounded Hilbert operators form a C star algebra, Bounded inverse theorem, Spectrum is nonempty compact and norm bounded, Spectrum and resolvent of a bounded operator).

[A3]

C(X,C) for compact Hausdorff X denotes the continuous complex-valued functions, with complex function algebras, self-adjointness, unitality and point separation as defined there; the restrictions of polynomials to σ(T) form such an algebra, and for X=σ(T) they are point-separating because the coordinate function separates points (Self-adjoint complex function algebras, unitality, and point separation).

[A4]

Every unital point-separating self-adjoint complex function algebra on a nonempty compact Hausdorff space is uniformly dense in C(X,C) (Complex Stone–Weierstrass dichotomy for separating self-adjoint algebras; the unital case is dense).

[A6]

B(H) is a complex Banach space with submultiplicative norm for composition, so operator-norm Cauchy sequences converge and multiplication is continuous (If (Y) is Banach then (\mathcal B(X,Y)) is Banach, Bounded Hilbert operators form a C star algebra).

[A7]

C(I,T) is the norm closure of the unital -algebra P(T) of -polynomials in T; a unital star-homomorphism between complex C*-algebras is a bounded complex-linear map preserving products and adjoints (C star algebra generated by a normal operator, C star algebra).

[A8]

AC is the hypothesis of the spectral and choice-consuming suppliers (The Axiom of Choice).

Proof

technique · direct

Given: A nonzero complex Hilbert space H, a bounded self-adjoint TB(H), and the set A of restrictions to σ(T) of complex polynomials.

1.1

The spectrum σ(T) is a nonempty compact subset of R.

A2
1.2

The space C(σ(T)) with pointwise operations, conjugation and the supremum norm is a unital commutative C*-algebra: pointwise products and conjugation satisfy the algebra axioms, the supremum norm is submultiplicative and satisfies ff=f2, and completeness follows because a supremum-norm Cauchy sequence of continuous functions has pointwise limits by completeness of C, converges uniformly by the standard estimate, and has continuous limit; A is a unital, self-adjoint and point-separating function algebra inside it, hence uniformly dense.

A3A4A5algebra
1.3

The map Φ:AB(H), pσ(T)p(T), is well defined and is complex-linear, multiplicative, unital, star-preserving (for σ(T)R the conjugate of pσ(T) is pσ(T)) and isometric. For the star identity, write p(z)=j=0majzj: the C*-involution laws and T=T give p(T)=j=0maj(T)j=j=0majTj; on the real spectrum this polynomial equals p(z).

A1A6A7algebra
2.1

For fC(σ(T)) and polynomials pn with pnf1/(n+1) (which exist by density) the sequence pn(T) is Cauchy in operator norm because pn(T)pm(T)=pnpm1n+1+1m+1, so it converges; the limit does not depend on the choice of sequence, since two such sequences differ in norm by at most 2/(n+1).

step 1.3A6A8
3.1

Defining Ψ(f) as that limit makes Ψ:C(σ(T))B(H) complex-linear, unital, multiplicative, star-preserving and isometric: each property holds for polynomial representatives by step 1.3 and passes to the limit by continuity of the algebra operations and the norm in B(H), while the norm identity passes by continuity of the modulus; moreover Ψ(z)=T.

step 2.1step 1.3A6A7algebra
4.1

The range of Ψ is C(I,T): each Ψ(f) is a norm limit of operators pn(T) lying in the unital -algebra generated by T, so the range is contained in its closure; conversely Φ(pσ(T))=p(T) shows that every -polynomial lies in the range, and the range is closed because Ψ is isometric on the complete space established in step 1.2: a convergent sequence of images has Cauchy preimages, whose limit maps to its image limit, so it contains the closure.

step 3.1step 1.2A7
4.2

With step 1.2, the map Ψ is an isometric unital star-homomorphism of complex C*-algebras in the sense of the definition, and Ψ(z)=T.

step 3.1step 1.2A7
4.3

Ψ is the only such map: if Ξ is an isometric unital star-homomorphism with Ξ(z)=T, then Ξ(pσ(T))=p(T)=Ψ(pσ(T)) for every polynomial p, by multiplicativity, unitality and star-preservation; for fC(σ(T)) and approximating polynomials pn with pnf1/(n+1), continuity of both isometric maps gives Ξ(f)=limΞ(pn)=limpn(T)=Ψ(f).

step 3.1step 1.3algebra
5.1

The map ff(T):=Ψ(f) is therefore the unique isometric unital star-homomorphism C(σ(T))B(H) with zT and range C(I,T).

step 4.1step 4.2step 4.3

Depends on

Used by

Dependency tree · two levels

60 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