LemmaStatement: AI-adaptedProof: 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.

Characteristic roots preserve separated cluster counts under matrix perturbation

Statement

Let $A_{n}, A \in C^{d \times d}$ with $A_{n} \to A$ entrywise. Let $U_{1}, \dots, U_{s}$ be pairwise disjoint open disks whose boundaries contain no eigenvalue of $A$ and which together contain every eigenvalue of $A$ . Then, for all sufficiently large $n$ , each $U_{j}$ contains exactly the same number of eigenvalues of $A_{n}$ , counted with algebraic multiplicity, as of $A$ .

Facts & Assumptions

Given: Matrices $A_{n}, A$ , the open disks $U_{j}$ , and the hypotheses in the Statement.

[F1]

For $A \in M_{n} (F)$ , the characteristic polynomial is $χ_{A} (x) = \det (x I_{n} - A)$ when $n \geq 1$ , with $χ_{A} (x) = 1$ for the unique $0 \times 0$ matrix: $χ_{A} (z) = \det (z I - A)$ is monic of degree $d$ for $d \geq 1$ ; its coefficients are polynomial expressions in the entries of $A$ , and $χ_{A} = 1$ when $d = 0$ .

[F2]

A complex polynomial of degree $n$ has exactly $n$ roots counted with multiplicity: a degree- $d$ complex polynomial with $d \geq 1$ factors into exactly $d$ linear roots counted with multiplicity, and the multiset is unique.

[F3]

Bolzano-Weierstrass: every bounded real sequence has a convergent subsequence: every bounded real sequence has a convergent subsequence.

Proof

Given: $A_{n}, A, U_{1}, \dots, U_{s}$ as in the Statement.

1.1F1givenalgebra

If $d = 0$ , every characteristic polynomial is $1$ by [F1], so every disk contains zero roots and the conclusion is immediate. For the remainder assume $d \geq 1$ . The coefficients of $χ_{A_{n}}$ converge to those of $χ_{A}$ because determinants are finite sums of products of matrix entries. They are therefore uniformly bounded. For a monic polynomial $z^{d} + \sum_{k < d} a_{k} z^{k}$ , every root satisfies $∣ z ∣ \leq 1 + \max_{k < d} ∣ a_{k} ∣$ : outside that disk, $\sum_{k < d} ∣ a_{k} ∣ ∣ z ∣^{k} < ∣ z ∣^{d}$ by the finite geometric-sum bound, so the polynomial cannot vanish. Hence all roots of all sufficiently large $χ_{A_{n}}$ lie in one fixed bounded disk.

2.1F2F3step 1.1construct

For each $n$ , list the $d$ roots of $χ_{A_{n}}$ with multiplicity in the canonical lexicographic order by real part and then imaginary part; [F2] supplies the finite multiset, and this ordering requires no choice. The resulting sequence of root lists is bounded in $R^{2 d}$ . Applying [F3] successively to its $2 d$ real coordinates gives a subsequence on which every root in the list converges.

3.1F1F2step 1.1step 2.1algebra

Along that subsequence, the factorization $χ_{A_{n}} (z) = \prod_{k = 1}^{d} (z - λ_{n, k})$ converges coefficientwise to $\prod_{k = 1}^{d} (z - λ_{k})$ . By step 1.1 the same coefficient limit is $χ_{A}$ , so uniqueness in [F2] shows that the limiting list is exactly the root multiset of $χ_{A}$ , including multiplicities.

4.1step 2.1step 3.1givencontradiction∎

If the asserted disk counts failed for infinitely many $n$ , restrict to those indices and repeat step 2.1. Since no root of $χ_{A}$ lies on any disk boundary, each convergent root sequence from step 3.1 is eventually in the same disk as its limit, or outside all the disks if its limit is outside them; hence the disk counts eventually equal the multiplicities of the limiting roots. This contradicts the chosen indices. Therefore the counts agree for all sufficiently large $n$ .

Depends on

Used by

Dependency tree · two levels

15 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

Yuri A. Kuznetsov, Elements of Applied Bifurcation Theory, 2nd ed., Springer (standard reference, not scraped)
J. E. Marsden and M. McCracken, The Hopf Bifurcation and Its Applications, Springer-Verlag, 1976 (standard reference, not scraped)