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 poorly aligned start delays the largest Ritz value and requires the start-angle factor
Example
Let and Verify that , bound the largest two-step Ritz value by , and compare the resulting gap with the Chebyshev bound from Lanczos largest Ritz values obey a Chebyshev start-angle bound, including degenerate branches. The comparison must show that deleting the start-angle factor would make this particular bound false.
Facts & Assumptions
Given: The diagonal matrix and unit starting vector specified above.
Lanczos largest Ritz values obey a Chebyshev start-angle bound, including degenerate branches: for a simple top eigenvalue, is the maximum Rayleigh quotient on and the stated Chebyshev error bound includes .
Verification
Since , the vector is unit. Also . Set Direct dot products give and . The vectors are independent because their first coordinates would force a proportionality factor , while the second coordinates would force factor . Hence is two-dimensional and equals .
We have For every unit , . By [F2], so . Its Rayleigh quotient satisfies since . Taking the maximum gives , so .
The top eigenspace is , hence . The unwanted interval is , and its affine exterior point is , so . The theorem's bound is which is valid but large. If its factor were deleted, the proposed right side would be , contradicting step 1.2. Thus this start cannot support that angle-free bound.
Depends on
Used by
Nothing in the library uses this result yet.
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
- Youcef Saad, Iterative Methods for Sparse Linear Systems, 2nd ed., §6.11.1, printed pp. 209–210 (standard reference, not scraped)
- David Bindel, Matrix Computations (CS 6210), Cornell University, Fall 2012, Lectures 38–39 (standard reference, not scraped)