ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pass

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 π 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.1L1algebra

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)$ .

2.1step 1.1L2L3L4algebra

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.

3.1step 2.1L5L1algebra∎

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.

Remarks

The circle below is the positively oriented contour $γ (t) = 1 + \frac{1}{2} e^{i t}$ : it encloses $1$ and excludes $2$ . The arrows on the right show the action of $P_{E}$ on the standard basis; $T$ acts by $1$ on $C e_{1}$ and by $2$ on $C e_{2}$ . These illustrate the contour computation and invariant summands in steps 2.1 and 3.1; the verification above is independent of the figure.

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)