ExampleConstruction: Literature-sourcedVerification: 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.

Riesz projection for a matrix with separated spectrum

Example

Assume the Axiom of Choice (The Axiom of Choice). Let $T : = diag (1, 2) \in M_{2} (C)$ , acting on the standard basis $e_{1}, e_{2}$ of $C^{2}$ . Its spectrum is $σ (T) = {1, 2}$ (Spectrum in a finite-dimensional matrix algebra), the subset $E : = {1}$ is clopen in the spectrum, and the Riesz spectral projection (Riesz spectral projection) is

$P_{E} = diag (1, 0) \in M_{2} (C),$

the operator of orthogonal projection onto $C e_{1}$ . Consequently $ran (P_{E}) = C e_{1}$ and $\ker (P_{E}) = C e_{2}$ are the two invariant summands of Riesz spectral projection properties, and the restrictions of $T$ to them have spectra ${1}$ and ${2}$ respectively.

Facts & Assumptions

Given: The Axiom of Choice, the diagonal matrix $T = diag (1, 2)$ , the spectral subset $E = {1}$ , and the circle $γ (t) : = 1 + \frac{1}{2} e^{i t}$ , $0 \leq t \leq 2 π$ , which separates $1$ from $2$ and lies in the resolvent set of $T$ .

[L1]

$M_{2} (C)$ with the operator norm is a unital Banach algebra and $σ (A) = {λ : \det (λ I - A) = 0}$ (Spectrum in a finite-dimensional matrix algebra).

[L2]

The Riesz projection is the calculus value of the locally constant function $χ_{E}$ , equivalently the resolvent contour integral $\frac{1}{2 π i} \int_{Γ} χ_{E} (z) (z I - T)^{- 1} d z$ over a cycle with index $1$ on $E$ and $0$ on $σ (T) ∖ E$ (Riesz spectral projection).

[L3]

For a closed cycle, $\frac{1}{2 π i} \int_{γ} (z - a)^{m} d z$ equals $1$ for $m = - 1$ and $0$ otherwise when $γ$ winds once around $a$ (On a positively oriented circle about a, the integral of (z-a)^m is zero for every integer m except -1, and is 2 pi i for m=-1).

[L4]

A uniformly convergent sequence of continuous functions on a contour may be integrated term by term (A uniformly convergent sequence of continuous integrands on a fixed contour permits passage of the limit through the complex line integral).

[L5]

The range and kernel of a Riesz projection are closed invariant summands, and the restriction spectra are the corresponding spectral parts (Riesz spectral projection properties).

Verification

technique · direct

1.1

Resolvent: for $z \notin {1, 2}$ one has $(z I - T)^{- 1} = diag ((z - 1)^{- 1}, (z - 2)^{- 1})$ , and the circle $γ$ of radius $1 / 2$ about $1$ avoids both spectral points; on it the resolvent is the diagonal pair of scalar functions $1 / (z - 1)$ and $1 / (z - 2)$ .

L1algebra

2.1

Contour integral: by [L3], $\frac{1}{2 π i} \int_{γ} \frac{d z}{z - 1} = 1$ because $γ$ is the circle about $1$ . On this circle $∣ z - 1 ∣ = 1 / 2$ , and $\frac{1}{z - 2} = - \frac{1}{1 - (z - 1)} = - \sum_{n \geq 0} (z - 1)^{n}$ uniformly: the tail after degree $N$ has modulus at most $2^{- N - 1} / (1 - 1 / 2)$ . Each term has integral zero by [L3], so [L4] gives $\int_{γ} d z / (z - 2) = 0$ . Hence $P_{E} = \frac{1}{2 π i} \int_{γ} (z I - T)^{- 1} d z = diag (1, 0)$ , the locally constant characteristic function of ${1}$ evaluated on the diagonal.

step 1.1L2L3L4algebra

3.1

The projection $diag (1, 0)$ is idempotent, commutes with $T$ and has $ran (P_{E}) = C e_{1}$ , $\ker (P_{E}) = C e_{2}$ ; both are $T$ -invariant, $T ∣_{C e_{1}}$ is multiplication by $1$ and $T ∣_{C e_{2}}$ is multiplication by $2$ , so the two restrictions have spectra ${1}$ and ${2}$ ; this agrees with [L5] and the separation of the spectral parts.

step 2.1L5L1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

31 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

Theo Bühler and Dietmar A. Salamon, Functional Analysis — equation (5.26) and Theorem 5.25(vi), printed pp. 226–228 (standard reference, not scraped)
Vahid Shirbisheh, Lectures on C-star Algebras, v2 — §2.5, printed pp. 48–50 (standard reference, not scraped)