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

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

Example

Let $T : R^{2} \to R^{2}$ have matrix

$A = (\begin{array}{cc} 1 & - 1 \\ 1 & 1 \end{array}) .$

The eigenvalue $λ = 1 + i$ has the eigenvector $w = (1, - i) = u + i v$ with $u = (1, 0)$ and $v = (0, - 1)$ . The corollary reconstructs from $w$ alone the $T$ -invariant real plane ${span}_{R} {u, v} = R^{2}$ and the rotation-scaling block: in the ordered basis $(u, - v) = (e_{1}, e_{2})$ the matrix of $T$ is the displayed $A$ itself, which has the standard form $(\begin{matrix} a & - b \\ b & a \end{matrix})$ with $a = b = 1$ .

Facts & Assumptions

Given: The operator $T$ with the displayed matrix $A$ and the vector $w = (1, - i)$ .

[L1]

A nonreal eigenvector $u + i v$ with eigenvalue $a + b i$ , $b \neq 0$ , yields independent $u, v$ , an invariant real plane, and the matrix $(\begin{matrix} a & - b \\ b & a \end{matrix})$ in the ordered basis $(u, - v)$ (A nonreal eigenvector yields an invariant real two-plane and the standard rotation-scaling block).

Verification

technique · direct

1.1

The characteristic polynomial is $\det (x I - A) = (x - 1)^{2} + 1 = x^{2} - 2 x + 2$ , whose roots are $1 \pm i$ , both nonreal.

algebra

1.2

For $λ = 1 + i$ , the equation $(A - λ I) w = 0$ is $- i x - y = 0$ and $x - i y = 0$ , so $y = - i x$ ; the choice $x = 1$ gives $w = (1, - i) = u + i v$ with $u = (1, 0)$ and $v = (0, - 1)$ .

algebra

2.1

Applying [L1] with $a = b = 1$ : $u$ and $v$ are $R$ -linearly independent, ${span}_{R} {u, v} = R^{2}$ is $T$ -invariant, and in the ordered basis $(u, - v) = (e_{1}, e_{2})$ the matrix of $T$ is $(\begin{matrix} a & - b \\ b & a \end{matrix}) = (\begin{matrix} 1 & - 1 \\ 1 & 1 \end{matrix}) = A$ .

L1step 1.2

2.2

The conjugate vector $σ (w) = (1, i)$ is an eigenvector with eigenvalue $1 - i$ , as recorded in [L1].

L1step 1.2

3.1

Steps 2.1 and 2.2 reconstruct the invariant plane and the block from the single nonreal eigenvector.

step 2.1step 2.2∎

Depends on

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

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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