CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 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.

A nonreal eigenvector yields an invariant real two-plane and the standard rotation-scaling block

Statement

Let $T : V \to V$ be an endomorphism of a real vector space, identify $V$ with the fixed real form of the canonical conjugation on $V_{C}$ , and suppose $w = u + i v$ with $u, v \in V$ is an eigenvector of $T_{C}$ with eigenvalue $λ = a + b i$ , where $b \neq 0$ . Then $u$ and $v$ are $R$ -linearly independent, ${span}_{R} {u, v}$ is $T$ -invariant, and with respect to the ordered basis $(u, - v)$ the matrix of $T$ restricted to that plane is

$(\begin{array}{cc} a & - b \\ b & a \end{array}) .$

Moreover $σ (w) = u - i v$ is an eigenvector of $T_{C}$ with eigenvalue $\overline{λ} = a - b i$ .

Facts & Assumptions

Given: A real vector space $V$ , an endomorphism $T$ , and an eigenvector $w = u + i v$ of $T_{C}$ with eigenvalue $λ = a + b i$ , where $u, v \in V$ and $b \neq 0$ .

[L1]

Every element of $V_{C}$ is uniquely $u + i v$ with $u, v$ in the fixed real form $V$ (The fixed points of a conjugation form a real vector space whose complexification recovers the ambient complex space).

[L2]

The canonical conjugation interchanges the generalised eigenspaces of $λ$ and $\overline{λ}$ (For a real operator, nonreal generalised eigenspaces of the complexification occur in conjugate pairs).

Proof

technique · direct

1.1

By [L1], the decomposition $w = u + i v$ with $u, v \in V$ is unique. Both $u$ and $v$ are nonzero: if $v = 0$ then $w$ lies in $V$ and $T_{C} w = λ w$ forces $b = 0$ ; symmetrically $u = 0$ would give the same contradiction for the coefficient of $i$ .

L1givenalgebra

2.1

Expanding $T_{C} (u + i v) = λ (u + i v)$ gives $T u + i T v = (a u - b v) + i (b u + a v)$ ; comparing the $V$ - and $i V$ -components, which are unique by [L1], yields $T u = a u - b v$ and $T v = b u + a v$ .

step 1.1algebra

2.2

The conjugate vector is an eigenvector for $\overline{λ}$ : $σ (w) = u - i v$ lies in $G_{\overline{λ}}^{(1)} (T_{C})$ by [L2] applied with $e = 1$ .

step 1.1L2

3.1

The vectors $u, v$ are $R$ -linearly independent: if $u$ and $v$ were dependent, then, since both are nonzero, $v = α u$ for a real $α$ , so $w = (1 + i α) u$ and dividing the eigen-equation by $1 + i α \neq 0$ gives $T_{C} u = λ u$ . But $T_{C} u = T u$ lies in $V$ , while $λ u = a u + b i u$ has nonzero $i$ -component $b u$ , contradicting uniqueness of the components in [L1].

step 1.1step 2.1L1algebra

3.2

The plane is invariant and the block appears: $T u = a u - b v = a u + b (- v)$ and $T (- v) = - (b u + a v) = - b u + a (- v)$ by step 2.1, so in the ordered basis $(u, - v)$ the two columns are $(\binom{a}{b})$ and $(\binom{- b}{a})$ .

step 2.1algebra

4.1

Steps 3.1 and 3.2 prove the independence, invariance and matrix claims, and step 2.2 the conjugate eigenvector claim.

step 2.2step 3.1step 3.2∎

Depends on

Used by

One nonreal eigenvector reconstructs the invariant real plane of a rotation-scaling block Example

Dependency tree · two levels

12 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)