TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31

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.

In a fixed gauge, the derivative of a simple right eigenvector is obtained by applying the reduced resolvent to the perturbation

Statement

Let $A (t)$ be differentiable, let $λ (t)$ be a simple eigenvalue branch, and let $x (t)$ be the right eigenvector branch chosen in the fixed gauge $y_{0}^{*} x (t) = 1$ , where $y_{0}$ is the left eigenvector at $t = 0$ . If $S$ is the reduced resolvent at $t = 0$ , then

$x^{'} (0) = - S A^{'} (0) x (0) .$

Facts & Assumptions

Given: A differentiable simple eigenpair branch in the fixed gauge $y_{0}^{*} x (t) = 1$ and the reduced resolvent $S$ at $t = 0$ .

[L1]

The reduced resolvent satisfies $S (A - λ I) = I - P$ and $S x = 0$ (The reduced resolvent satisfies the standard projector and inverse identities on the complementary invariant subspace).

[L2]

The eigenvalue derivative is $λ^{'} (0) = y_{0}^{*} A^{'} (0) x (0)$ (Along a differentiable matrix path, a simple eigenvalue satisfies $λ^{'} = y^{*} A^{'} x$ under the normalization $y^{*} x = 1$ ).

Proof

technique · direct

1.1

Differentiate $(A - λ I) x = 0$ at $t = 0$ : $(A^{'} (0) - λ^{'} (0) I) x + (A - λ I) x^{'} = 0.$ Apply $S$ and use [L1]: $x^{'} - P x^{'} = - S (A^{'} (0) - λ^{'} (0) I) x .$ Because the fixed gauge gives $y_{0}^{*} x^{'} (0) = 0$ , the derivative $x^{'} (0)$ lies in $\ker y_{0}^{*}$ , so $P x^{'} (0) = x (y_{0}^{*} x^{'} (0)) = 0$ .

L1L2givenalgebra

2.1

Step 1.1 therefore gives $x^{'} (0) = - S (A^{'} (0) - λ^{'} (0) I) x (0)$ . Since $S x (0) = 0$ by [L1], the $λ^{'} (0)$ term disappears and $x^{'} (0) = - S A^{'} (0) x (0)$ .

L1step 1.1algebra∎

Depends on

Used by

Dependency tree · two levels

8 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

G. W. Stewart and Ji-guang Sun, Matrix Perturbation Theory (standard reference, not scraped)