ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generated

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.

Nearly colliding eigenvalue sums make a Sylvester solve sensitive

Example

Let $ε = 10^{- 6}$ , $A = diag (1, 2)$ , $B = diag (- 1 + ε, 0)$ , and $C = E_{11}$ . The Sylvester equation $A X + X B = C$ has a unique solution, its separation is $ε$ , and $X = ε^{- 1} E_{11}$ . Thus a residual of size $δ$ in the $E_{11}$ direction produces a solution error of size $δ / ε$ .

Facts & Assumptions

Given: The matrices and $ε$ in the Example.

[F1]

Sylvester operator and Frobenius separation number: $S_{A, B} (X) = A X + X B$ and $sep (A, - B) = σ_{\min} (S_{A, B})$ in the Frobenius inner product.

[F2]

A Sylvester equation is uniquely solvable exactly when the spectra are disjoint: Unique solvability holds exactly when $σ (A) \cap (- σ (B)) = \emptyset$ .

[F3]

Sylvester separation converts a residual into a forward error bound: $∥ X - \hat{X} ∥_{F} \leq ∥ C - (A \hat{X} + \hat{X} B) ∥_{F} / sep (A, - B)$ when the solution is unique.

Verification

1.1givenF1F2algebra

The eigenvalue sums are $ε, 1, 1 + ε, 2$ , all nonzero, so [F2] gives a unique solution. In the Frobenius-orthonormal matrix-unit basis, $S_{A, B} (E_{i j}) = (a_{i i} + b_{j j}) E_{i j}$ ; its singular values are therefore the four absolute eigenvalue sums, and [F1] gives $sep (A, - B) = ε$ .

2.1givenstep 1.1algebra

The $(i, j)$ equation is $(a_{i i} + b_{j j}) x_{i j} = c_{i j}$ . Since $C = E_{11}$ , the only nonzero entry is $x_{11} = 1 / ε$ , hence $X = ε^{- 1} E_{11}$ and $∥ X ∥_{F} = 1 / ε = 10^{6}$ .

3.1F1F3step 2.1algebra∎

If the right-hand side is perturbed by $δ E_{11}$ , the solution changes by $δ / ε E_{11}$ , whose Frobenius norm is $∣ δ ∣ / ε$ . This attains the separation factor in [F3], verifying the stated sensitivity exactly.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

14 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.