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 mass-stiffness pencil has real B-orthogonal modes and a residual enclosure
Example
Let the stiffness and mass matrices be The generalized eigenvalues are and , with -orthogonal modes. The trial pair also illustrates a B-metric residual enclosure.
Facts & Assumptions
Given: The displayed real symmetric stiffness and mass matrices.
A Hermitian-definite pencil has a real spectrum and a B-orthonormal eigenbasis: a symmetric and positive-definite have real generalized eigenvalues and an -orthonormal eigenbasis.
A B-dual residual bounds distance to the spectrum of a Hermitian-definite pencil: a nonzero trial vector and real trial value have spectral distance bounded by the -dual residual norm divided by the -norm of the vector.
Regular matrix pencils and homogeneous generalized eigenvalues: the pencil is regular when its determinant polynomial is nonzero.
Verification
The matrix is positive definite because for . Also for . The determinant polynomial is so the pencil is regular and its eigenvalues are .
For , . For , . Their mass inner product is . Thus they are distinct generalized eigenmodes and are -orthogonal; [F1] gives the general real-spectrum and orthogonal-basis conclusion for this pencil.
For and , the residual is . Hence and, since , . The theorem [F2] therefore bounds the distance from to by ; indeed that distance is .
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
11 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
- LAPACK Users' Guide, Generalized Symmetric Definite Eigenproblems (standard reference, not scraped)