Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-28
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.

A normal endomorphism is a sum of its eigenvalues times pairwise orthogonal projections, and each spectral projection is a polynomial in the endomorphism

Statement

Let V be a finite-dimensional complex inner product space and let T:VV be normal. If λ1,,λr are the distinct eigenvalues of T, then there are pairwise orthogonal projections P1,,Pr such that

T=j=1rλjPj,

each Pj projects onto the eigenspace Eλj(T), and every Pj is a polynomial in T.

Facts & Assumptions

Given: A finite-dimensional complex inner product space V and a normal endomorphism T:VV with distinct eigenvalues λ1,,λr.

[L2]

Self-adjoint idempotents are exactly orthogonal projections (An endomorphism is an orthogonal projection exactly when it is idempotent and self-adjoint).

[L3]

In the primary decomposition, each primary projection is a polynomial in the endomorphism (Each projection in the primary decomposition is a polynomial in the endomorphism).

Proof

technique · direct
1.1

By [L1], V has an orthonormal eigenbasis. If V=0, then there are no eigenvalues and T=0 is the empty sum. Otherwise V=Eλ1(T)Eλr(T) with the summands pairwise orthogonal; if Pj is the orthogonal projection onto Eλj(T) and v=v1++vr with vjEλj(T), then Tv=λ1v1++λrvr=j=1rλjPjv, hence T=j=1rλjPj.

L1
2.1

Because the eigenspaces are pairwise orthogonal and the Pj are the corresponding orthogonal projections, one has Pj2=Pj, Pj=Pj, and PiPj=0 for ij, so the Pj are pairwise orthogonal projections in the sense of [L2].

L2step 1.1
3.1

Since T is diagonalisable with distinct eigenvalues, its primary decomposition is exactly the direct sum of the eigenspaces Eλj(T). Therefore [L3] identifies each projection onto Eλj(T) with a polynomial in T.

L3step 1.1

Depends on

Used by

Dependency tree · two levels

16 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