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.
Outward interval block LDL inertia certifier with pivot-inconclusive status
Definition
Input , a nonempty family of Hermitian matrices in enclosed by complex rectangles with real diagonal intervals and conjugate-paired off-diagonal rectangles, a simultaneous permutation of all positions, a partition of the permuted positions into consecutive pivot blocks of sizes one or two, the corresponding structural ordering, and a threshold . The exact midpoint matrix is Hermitian. First run the exact-arithmetic branch of Sparse symmetric-indefinite block LDL* with threshold tests and failure status on that midpoint with this same ordering, block partition and threshold. If it reports pivot-failure, return pivot-inconclusive; this is only failure of this candidate plan.
For a successful candidate plan, independently initialize the interval active matrix from the family enclosure and process the same blocks. At a one-by-one pivot require its real interval to exclude zero and determine its sign. At a two-by-two pivot, outward-enclose its real determinant and trace . Use A Hermitian two-by-two pivot inertia is determined by determinant and trace signs: accept a negative determinant as inertia ; accept a positive determinant together with positive trace as , and with negative trace as . If these signs cannot be established, return pivot-inconclusive with the block index.
For each accepted block form its interval inverse from the scalar reciprocal or the adjugate divided by the determinant interval. Update the trailing Hermitian Schur complement by outward evaluation of . If a required denominator includes zero, an operation is undefined, an enclosure is non-finite, or Hermitian symmetry cannot be maintained, return pivot-inconclusive. At completion sum the certified pivot inertia triples and return certified-inertia with the count and factor/update record.
Every accepted pivot is nonsingular for every matrix represented by the current interval active matrix. A midpoint pivot failure, an interval pivot failure, or an unresolved sign never asserts that a family member is singular. The procedure makes no universal pivot-success or growth claim.
Depends on
- Sparse symmetric-indefinite block LDL* with threshold tests and failure status
- Block LDL congruence adds the Hermitian pivot inertias
- A Hermitian two-by-two pivot inertia is determined by determinant and trace signs
- Real intervals, complex rectangles and ball enclosures
- Outward-rounded interval, rectangle and ball operations
- Outward-rounded operations are inclusion-isotone and enclose DAG evaluations
Used by
Dependency tree · two levels
26 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)