LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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 regular pencil has no nonzero vector in both kernels

Statement

If $(A, B)$ is a regular pencil and $x \in C^{n}$ satisfies $A x = 0$ and $B x = 0$ , then $x = 0$ .

Facts & Assumptions

Given: A regular pencil $A - λ B$ of order $n \geq 1$ .

[F1]

Regular matrix pencils and homogeneous generalized eigenvalues: regularity means $\det (A - λ B)$ is a nonzero polynomial.

[F2]

For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix: determinant is defined by the finite Leibniz sum.

[F3]

A nonzero polynomial of degree $n$ over an integral domain has at most $n$ distinct roots: a nonzero polynomial of degree $d$ over an integral domain has at most $d$ distinct roots.

[F4]

A finite-dimensional linear operator over a field is invertible if and only if its determinant is nonzero: a finite-dimensional operator is invertible exactly when its determinant is nonzero.

Proof

1.1givenF1F4algebraassume-contra

Suppose $x \neq 0$ and $A x = B x = 0$ . Then $(A - λ B) x = 0$ for every $λ \in C$ , so $A - λ B$ is not invertible. By [F4], $f (λ) = \det (A - λ B) = 0$ for every complex $λ$ .

2.1givenF1F2F3step 1.1contradictiondischarge-contradiction∎

By [F2], $f$ has degree at most $n$ . If $f$ were nonzero, [F3] would bound its number of distinct complex roots by $n$ , while step 1.1 gives every $λ \in C$ as a root. In particular, the $n + 1$ distinct numbers $0, 1, \dots, n$ would all be roots, contradicting [F1].

Depends on

Used by

Every regular real or complex pencil has a generalized Schur form Theorem

Dependency tree · two levels

23 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

Daniel Kressner, Numerical Methods and Software for General and Structured Eigenvalue Problems (PhD dissertation, 2004), Chapter 2: The QZ Algorithm (standard reference, not scraped)
LAPACK Users' Guide, Generalized Nonsymmetric Eigenproblems (standard reference, not scraped)