TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29

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.

For a real operator, nonreal generalised eigenspaces of the complexification occur in conjugate pairs

Statement

Let $T : V \to V$ be an endomorphism of a real vector space, let $σ = σ_{can}$ be the canonical conjugation of $V_{C}$ , and let $λ \in C$ and $e \geq 1$ . Then

$σ (G_{λ}^{(e)} (T_{C})) = G_{\overline{λ}}^{(e)} (T_{C}) .$

Thus for nonreal $λ$ the generalised eigenspaces of $T_{C}$ for $λ$ and for $\overline{λ}$ are interchanged by the real-linear involution $σ$ , and they have the same real dimension.

Facts & Assumptions

Given: A real vector space $V$ , an endomorphism $T : V \to V$ , a complex scalar $λ$ , and an exponent $e \geq 1$ .

[L1]

A conjugation is conjugate-linear and an involution (Conjugations and real structures on a complex vector space).

[L2]

The complexification of a real operator commutes with the canonical conjugation, because it comes from a real operator (A complex-linear operator comes from a real operator exactly when it commutes with the chosen conjugation).

[L3]

The generalised eigenspace of exponent $e$ is $G_{λ}^{(e)} (T_{C}) = \ker (T_{C} - λ I)^{e}$ (Primary components $\ker q (T)^{e}$ and generalised eigenspaces $G_{λ}^{(e)} (T) = \ker (T - λ I)^{e}$ ).

Proof

technique · direct

1.1

The operator $T_{C}$ commutes with $σ$ by [L2], and $σ$ is an $R$ -linear involution, hence a bijection, with $σ (z w) = \overline{z} σ w$ by [L1].

L1L2

2.1

The powers commute with $σ$ up to conjugation of the scalar: for $w \in V_{C}$ , $σ (T_{C} w - λ w) = T_{C} σ w - \overline{λ} σ w$ by step 1.1 and [L1]; iterating this $e$ times gives $σ (T_{C} - λ I)^{e} = (T_{C} - \overline{λ} I)^{e} σ$ .

step 1.1L1algebra

3.1

If $w \in \ker (T_{C} - λ I)^{e}$ , then $(T_{C} - \overline{λ} I)^{e} σ w = σ (T_{C} - λ I)^{e} w = σ (0) = 0$ , so $σ w \in G_{\overline{λ}}^{(e)} (T_{C})$ by [L3].

step 2.1L3

3.2

Conversely, if $w^{'} \in G_{\overline{λ}}^{(e)} (T_{C})$ , then $w : = σ w^{'}$ satisfies $(T_{C} - λ I)^{e} w = σ (T_{C} - \overline{λ} I)^{e} w^{'} = 0$ , so $w \in G_{λ}^{(e)} (T_{C})$ ; since $σ$ is an involution, the two inclusions combine to the equality $σ (G_{λ}^{(e)} (T_{C})) = G_{\overline{λ}}^{(e)} (T_{C})$ .

step 2.1L1L3

4.1

Because $σ$ is real-linear and bijective by step 1.1, the two generalised eigenspaces have the same real dimension; for nonreal $λ$ they form the conjugate pair interchanged by $σ$ .

step 1.1step 3.2∎

Depends on

Used by

Dependency tree · two levels

14 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

Keith Conrad, Complexification (notes) (standard reference, not scraped)