TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

A finite computed Francis similarity sequence has a conditional normwise backward-error bound

Statement

Let $A$ be the input, set ${\hat{H}}_{0} = A$ , and include every Hessenberg and QR update and every pure deflation write among stages $j = 1, \dots, m$ . Each pure deflation is an identity-transform stage with zero arithmetic coefficient. The finite reduction's represented product is $Q = P_{1} \dots P_{m}$ (with $P_{j} = I$ for a pure deflation stage), and its final matrix is $\hat{T} = {\hat{H}}_{m}$ , after any finite successful prefix or completed run. Suppose ${\hat{H}}_{j} = P_{j}^{*} ({\hat{H}}_{j - 1} + E_{j} + D_{j}) P_{j}, ∥ E_{j} ∥_{F} \leq α_{j} ∥ {\hat{H}}_{j - 1} ∥_{F},$ where $D_{j}$ is the signed additive change from exact deflation zero writes (zero minus each overwritten value) and each $P_{j}$ is the exact stored-vector representative. Then $\hat{T} = Q^{*} (A + Δ) Q, ∥ Δ ∥_{F} \leq \sum_{j} α_{j} ∥ {\hat{H}}_{j - 1} ∥_{F} + \sum_{j} ∥ D_{j} ∥_{F} .$ The conditional assertion holds for any certified nonnegative $α_{j}$ . For the actual specified real/complex arithmetic, Left and right scaled Householder errors give a concrete similarity bound proves $α_{j} = a_{j} + b_{j} + a_{j} b_{j}$ under its arithmetic/range and active-dimension hypotheses: use the target-overwrite left coefficient when a matrix column is targeted, the separate-block left coefficient for an external polynomial vector, and always the right separate-block coefficient. It covers initialization as well as all chase steps. Identity branches have zero arithmetic error. Deflation remains separate.

If the finite reduction returns certificate status certified and accumulator $C_{a c c}$ , then also $\sum_{j} α_{j} ∥ {\hat{H}}_{j - 1} ∥_{F} + \sum_{j} ∥ D_{j} ∥_{F} \leq C_{a c c},$ so $C_{a c c}$ is a reported upper bound for $∥ Δ ∥_{F}$ . This completes a concrete implementation-level normwise backward bound. A rounded dense realization of $Q$ retains its separate orthogonality residual. Budget, stagnation, Schur-type-undecided and arithmetic/invariant failures retain their statuses; a backward bound for a finite prefix does not establish a completed Schur form or unconditional convergence. No same-size forward eigenvalue error is inferred for a nonnormal matrix. A norm certificate requires exact evaluation or rigorous outward allowances, not an uncorrected rounded diagnostic.

Facts & Assumptions

Given: The finite exact-factor representation and local relations; for the concrete instance use the successful operationwise arithmetic and actual overwrite choices.

[F1]

Finite-budget computed Francis Schur reduction with explicit statuses records all factors, target operations and signed additive deflation writes with finite controls and explicit statuses; on a certified return it supplies $C_{a c c}$ and the $ρ, C$ outward recurrence.

[F2]

Local unitary-similarity perturbations accumulate as a backward perturbation turns the finite local relations into a backward perturbation bounded by the sum of their Frobenius norms.

[F3]

Left and right scaled Householder errors give a concrete similarity bound proves the actual matching real/complex two-sided coefficient $a + b + a b$ .

[A1]

For the general conditional assertion, the displayed local inequalities with nonnegative $α_{j}$ are hypotheses. For the specified arithmetic they are supplied by [F3], rather than a false universal $3 γ_{m}$ claim.

Proof

1.1givenF1F2A1algebra

Apply [F2] to the finite recorded sequence in [F1], with initial $H_{0} = A$ and initial factor $U_{0} = I$ . It gives $\hat{T} = Q^{*} (A + Δ) Q$ with $∥ Δ ∥_{F} \leq \sum_{j} (∥ E_{j} ∥_{F} + ∥ D_{j} ∥_{F})$ . Substituting [A1] proves the conditional bound.

2.1F1F3step 1.1algebra

For the actual arithmetic, [F3] supplies each required $E_{j}$ and its coefficient from the actual matrix-target or separate-panel use. Substitution into step 1.1 proves the concrete bound. No step uses Schur convergence, so the finite-prefix assertion and the retained status distinctions follow.

3.1F1step 1.1step 2.1algebrainduction∎

On a certified return, initialize $ρ_{0} \geq ∥ A ∥_{F}$ and $C_{0} = 0$ as specified in [F1]. Assume inductively that $ρ_{j - 1} \geq ∥ {\hat{H}}_{j - 1} ∥_{F}$ . The local relation and unitary invariance give $∥ {\hat{H}}_{j} ∥_{F} \leq (1 + α_{j}) ∥ {\hat{H}}_{j - 1} ∥_{F} + ∥ D_{j} ∥_{F} .$ Since the outward evaluator uses ${\overset{ˉ}{α}}_{j} \geq α_{j}$ and ${\overset{ˉ}{β}}_{j} \geq ∥ D_{j} ∥_{F}$ , its recurrence yields $ρ_{j} \geq ∥ {\hat{H}}_{j} ∥_{F}$ and $C_{j} \geq C_{j - 1} + α_{j} ∥ {\hat{H}}_{j - 1} ∥_{F} + ∥ D_{j} ∥_{F}$ . Induction from $j = 0$ proves $C_{m} \geq \sum_{j} α_{j} ∥ {\hat{H}}_{j - 1} ∥_{F} + \sum_{j} ∥ D_{j} ∥_{F}$ . The returned $C_{a c c} = C_{m}$ therefore dominates the bound in step 1.1.

Depends on

Used by

Nothing in the library uses this result yet.

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

David Bindel, CS 6210 Matrix Computations, Hessenberg QR iteration (standard reference, not scraped)