TheoremStatement: AI-adaptedProof: AI-generatedPipeline-generatedprecheck passaudited 2026-08-30

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 local Householder backward-error bound yields a backward-stable QR factorisation

Statement

Let $A \in M_{m \times n} (R)$ with $m \geq n$ . Assume Householder QR is executed in the standard relative floating-point model with unit roundoff $u$ and $m u < 1$ . Suppose that at each step $k = 0, \dots, n - 1$ the computed reflector ${\hat{H}}_{k}$ is orthogonal and its action on the active trailing block is exact for one perturbation $E_{k}$ satisfying ${\hat{H}}_{k} (A^{(k)} + E_{k}) = A^{(k + 1)}, ∥ E_{k} ∥_{F} \leq 3 γ_{m} ∥ A^{(k)} ∥_{F},$ where $A^{(0)} = A$ and $γ_{m} = m u / (1 - m u)$ . Then the computed factors $\hat{Q}, \hat{R}$ satisfy

$A + Δ A = \hat{Q} \hat{R}$ for some matrix $Δ A$ with $∥ Δ A ∥_{F} \leq ((1 + 3 γ_{m})^{n} - 1) ∥ A ∥_{F},$

In particular, under the displayed local-step bound the algorithm is backward stable: the computed factorisation is exact for a nearby matrix whose relative Frobenius perturbation is $O (u)$ .

Facts & Assumptions

Given: A matrix $A \in M_{m \times n} (R)$ with $m \geq n$ , unit roundoff $u$ with $m u < 1$ , and computed orthogonal Householder reflectors ${\hat{H}}_{k}$ satisfying the local-step identities and bounds in the statement.

[L1]

Successive Householder reflectors produce QR by applying orthogonal transformations to shrinking trailing blocks (Successive Householder or Givens transformations produce full and reduced QR factorisations with the standard dense operation counts).

[L2]

The quantity $γ_{m} = m u / (1 - m u)$ is the standard accumulated relative error factor when $m u < 1$ (If |delta_i| <= u and n u < 1, then prod (1+delta_i) = 1 + theta_n with |theta_n| <= gamma_n).

[L3]

Frobenius norm is invariant under left and right orthogonal multiplication (Spectral and Frobenius norms are unitarily invariant, are given by singular values, and satisfy the sharp rank comparison).

[A1]

For each $k$ , the computed local step satisfies ${\hat{H}}_{k} (A^{(k)} + E_{k}) = A^{(k + 1)}, ∥ E_{k} ∥_{F} \leq 3 γ_{m} ∥ A^{(k)} ∥_{F} .$

Proof

technique · convert each floating-point step into an exact step for a nearby trailing block and sum the transported perturbations

1.1

The local-step hypothesis [A1] supplies a perturbation $E_{k}$ for every active block and an exact orthogonal update ${\hat{H}}_{k} (A^{(k)} + E_{k}) = A^{(k + 1)}$ with $∥ E_{k} ∥_{F} \leq 3 γ_{m} ∥ A^{(k)} ∥_{F}$ .

A1L2

2.1

Embed each $E_{k}$ into the original matrix size by padding zeros outside the active block and transport it back through the previous computed reflectors. Because every ${\hat{H}}_{k}$ is orthogonal, [L3] preserves the Frobenius norm of each transported perturbation. Summing the $n$ transported perturbations gives a single matrix $Δ A$ such that $A + Δ A = \hat{Q} \hat{R}$ and $∥ Δ A ∥_{F} \leq \sum_{k = 0}^{n - 1} ∥ E_{k} ∥_{F} \leq 3 γ_{m} \sum_{k = 0}^{n - 1} ∥ A^{(k)} ∥_{F} .$

step 1.1L1L3algebra

2.2

From step 1.1 and [L3], $∥ A^{(k + 1)} ∥_{F} = ∥ {\hat{H}}_{k} (A^{(k)} + E_{k}) ∥_{F} = ∥ A^{(k)} + E_{k} ∥_{F} \leq ∥ A^{(k)} ∥_{F} + ∥ E_{k} ∥_{F} \leq (1 + 3 γ_{m}) ∥ A^{(k)} ∥_{F} .$ Since $A^{(0)} = A$ , induction gives $∥ A^{(k)} ∥_{F} \leq (1 + 3 γ_{m})^{k} ∥ A ∥_{F}$ for every $k$ .

step 1.1L3inductionalgebra

3.1

Substituting step 2.2 into step 2.1 yields $∥ Δ A ∥_{F} \leq 3 γ_{m} \sum_{k = 0}^{n - 1} (1 + 3 γ_{m})^{k} ∥ A ∥_{F} = ((1 + 3 γ_{m})^{n} - 1) ∥ A ∥_{F} .$ This is the stated backward bound.

step 2.1step 2.2algebra

4.1

Step 3.1 proves the displayed estimate, and step 2.1 gives the nearby factorisation identity.

step 2.1step 3.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

20 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

Tobin A. Driscoll and Richard J. Braun, Fundamentals of Numerical Computation, Section 3.4 (standard reference, not scraped)
David Bindel, CS 4220: Numerical Analysis, Least squares and QR (standard reference, not scraped)