ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Ordered eigenvalue bisection by exact inertia queries

Example

For the singleton Hermitian family $A = diag (- 1, 2)$ , a valid outward Frobenius upper bound $M = 3$ , tolerance $ε = 3 / 8$ , query budget $B = 8$ , and the scalar pivot plan with threshold $1$ , exact inertia queries return the ordered eigenvalue brackets

λ_{1} (A) \in [- 9 / 8, - 3 / 4], λ_{2} (A) \in [15 / 8, 9 / 4] .

Facts & Assumptions

Given: The singleton matrix family, initial bracket $[- 3, 3]$ , tolerance, budget and fixed pivot plan above.

[F1]

A successful bisection loop preserves each ordered eigenvalue bracket after every exact count below a nonsingular shift (Certified inertia counts maintain ordered eigenvalue brackets).

[F2]

The interval inertia certifier reports the exact inertia on success (The interval block LDL certifier returns the exact inertia on success).

[F3]

The finite bisection procedure uses the initial uniform Frobenius bracket and updates the least unfinished index at each query (Budgeted ordered Hermitian eigenvalue bisection by verified inertia).

[F4]

A successful run's returned intervals enclose the corresponding eigenvalues (The ordered Hermitian bisection certifier returns valid intervals or an inconclusive status).

Verification

1.1givenF2algebra

The Frobenius norm of $A$ is $\sqrt{5} < 3$ , so the stated initial bracket is valid. On each queried shift, the shifted matrix remains diagonal with nonzero scalar pivots; the exact midpoint factorization succeeds, and its interval pivots are degenerate intervals with the same nonzero signs. Thus [F2] certifies the counts shown below.

2.1F1F3step 1.1algebra

For $k = 1$ , the successive shifts $0, - 3 / 2, - 3 / 4, - 9 / 8$ have respectively $1, 0, 1, 0$ negative eigenvalues of $A - τ I$ . The update rule gives brackets $[- 3, 0]$ , $[- 3 / 2, 0]$ , $[- 3 / 2, - 3 / 4]$ , and $[- 9 / 8, - 3 / 4]$ . For $k = 2$ , shifts $0, 3 / 2, 9 / 4, 15 / 8$ have respectively $1, 1, 2, 1$ negative eigenvalues, giving brackets $[0, 3]$ , $[3 / 2, 3]$ , $[3 / 2, 9 / 4]$ , and $[15 / 8, 9 / 4]$ . These are eight successful queries, and both final widths are $3 / 8$ .

3.1F1F2F4step 2.1algebra∎

The exact increasing eigenvalues are $- 1$ and $2$ , which lie in the displayed final intervals. More generally, the interval conclusions follow from [F4] applied to the certified run; no failed-pivot case occurs here.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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 EPrint2015.103 (standard reference, not scraped)