Alphabeta MathHow 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.
The ordered Hermitian bisection certifier returns valid intervals or an inconclusive status
Statement
For every completed run of Budgeted ordered Hermitian eigenvalue bisection by verified inertia on a family of dimensional Hermitian matrices, each returned interval for index contains for every admitted matrix . A blocked or budget-exhausted result preserves the same enclosure guarantee but may have width greater than the requested tolerance. Failure to certify a shift is not evidence of a singular family member.
Facts & Assumptions
Given: A nonempty Hermitian family with sound finite interval enclosure, positive tolerance and a finite query budget.
Outward interval bounds enclose every family entry and every computed norm upper bound (Outward-rounded operations are inclusion-isotone and enclose DAG evaluations).
Every eigenvalue lies in the interval given by a uniform Frobenius norm bound (Hermitian eigenvalues lie within a certified Frobenius bound).
A successful interval LDL inertia result is the exact uniform inertia for every shifted family member (The interval block LDL certifier returns the exact inertia on success).
Inertia-guided midpoint updates preserve ordered eigenvalue brackets, and an inconclusive query leaves its bracket unchanged (Certified inertia counts maintain ordered eigenvalue brackets).
Proof
If the interval norm calculation succeeds, [F1] makes its returned an upper bound for every . By [F2], every eigenvalue of every member lies in , so all initial brackets are valid.
At a successful shift, [F3] supplies one inertia for every and its zero count is checked to be zero. Its negative count is therefore exactly the number of eigenvalues of each below . The algorithm's update is the successful query of [F4]; on pivot failure or a zero pivot it leaves the interval unchanged, which is the inconclusive branch of [F4].
Apply [F4] to each index, treating later unexecuted queries after a blocked index or budget exhaustion as no-op inconclusive queries. Each bracket therefore continues to contain the corresponding ordered eigenvalue for every family member. Certified updates halve its width, while statuses only describe why the requested tolerance or query count may not have been reached.
Depends on
- Budgeted ordered Hermitian eigenvalue bisection by verified inertia
- Certified inertia counts maintain ordered eigenvalue brackets
- Hermitian eigenvalues lie within a certified Frobenius bound
- The interval block LDL certifier returns the exact inertia on success
- Outward-rounded operations are inclusion-isotone and enclose DAG evaluations
Used by
Cited to discharge well-definedness by Budgeted ordered Hermitian eigenvalue bisection by verified inertia.
Dependency tree · two levels
19 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
- Nicholas J. Higham, Numerical Linear Algebra and Matrix Analysis, MIMS EPrint 2015.103, §5.6 (standard reference, not scraped)
- Siegfried M. Rump, Verification methods: Rigorous results using floating-point arithmetic, Acta Numerica 19 (2010), §§5.1–5.5 (standard reference, not scraped)