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.
Scalar eigenvalue stability does not control nonnormal matrix growth
Example
Take , , and one-stage RKC1. Both eigenvalues of lie in the scalar stability interval, but the matrix step expands a vector in Euclidean norm.
Facts & Assumptions
Given: The real matrix and step in the Example, the RKC1 polynomial, and the Euclidean norm; use linear fields on all of with exact evaluation.
First-order stabilized explicit Runge–Kutta–Chebyshev step: for the output is , so for the matrix update is .
RKC stability polynomials and certified negative-real intervals: the scalar RKC1 stability interval for is ; its matrix nonexpansion conclusion requires both self-adjointness and for every , with .
The Euclidean inner product on : for .
Verification
The matrix is nonnormal: while . Its two eigenvalues are , so those of are both and the scalar stability factor is .
The one-stage update is It sends to , whose Euclidean norm is . Therefore eigenvalue-wise scalar stability does not imply Euclidean nonexpansion here. However, for , , so this matrix also violates the nonpositivity hypothesis in [F2].
To test omission of self-adjointness while retaining nonpositivity, take and , still with . For every , . Both eigenvalues of are , so , , and . Yet and sends to , increasing its Euclidean norm from to . Thus the self-adjoint hypothesis in [F2] cannot be omitted even when nonpositivity and the spectral step restriction are retained.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
31 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
- B.P. Sommeijer, L.F. Shampine, and J.G. Verwer, RKC: An explicit solver for parabolic PDEs, §§1–2 (standard reference, not scraped)
- Ibrahim Almuslimani and Gilles Vilmart, Explicit Stabilized Integrators for Stiff Optimal Control Problems, §2.2.1 (standard reference, not scraped)