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

Two-pass MGS Arnoldi has an explicit local relation and an a posteriori orthogonality bound

Statement

Let $A \in R^{n \times n}$ , $n \geq 1$ , and let the computed starting vector $q_{1}$ be nonzero. Fix $m \geq 1$ and, for $j = 1, \dots, m$ , compute each component of $z_{j} = fl (A q_{j})$ by the length- $n$ rounded dot product of that row with $q_{j}$ . Then perform two complete modified Gram–Schmidt passes: for $p = 1, 2$ and $i = 1, \dots, j$ , compute $h_{i j}^{(p)} = fl (q_{i}^{T} w_{i - 1, j}^{(p)}), w_{i j}^{(p)} = fl (w_{i - 1, j}^{(p)} - h_{i j}^{(p)} q_{i}),$ where $w_{0 j}^{(1)} = z_{j}$ and $w_{0 j}^{(2)} = w_{j j}^{(1)}$ . The vector update is componentwise one rounded product followed by one rounded subtraction. Store $h_{i j} = fl (h_{i j}^{(1)} + h_{i j}^{(2)})$ . Compute $t_{j} = fl ((w_{j j}^{(2)})^{T} w_{j j}^{(2)})$ as a length- $n$ dot product, $β_{j + 1} = fl (\sqrt{t_{j}})$ , and $q_{j + 1} = fl (w_{j j}^{(2)} / β_{j + 1})$ componentwise.

Assume all products, partial sums, square roots, divisions, and updates used here succeed in the operationwise model, so every nonzero exact product and partial sum is normal-range; exact-zero products and sums are permitted. Assume $n u < 1$ , $γ_{n} < 1$ , $2 u < 1$ , and $t_{j} > 0$ . Define $c_{n} = (1 - u) \sqrt{1 - γ_{n}}$ . Then $β_{j + 1} \geq c_{n} ∥ w_{j j}^{(2)} ∥_{2} > 0$ , and the computed columns satisfy $A q_{j} = \sum_{i = 1}^{j} h_{i j} q_{i} + β_{j + 1} q_{j + 1} + e_{j},$ where, writing $δ_{j}^{m v} = z_{j} - A q_{j}$ , $e_{j} = - δ_{j}^{n o r m} - δ_{j}^{m v} - \sum_{p = 1}^{2} \sum_{i = 1}^{j} ζ_{i j}^{(p)} - \sum_{i = 1}^{j} χ_{i j} q_{i},$ with $δ_{j}^{n o r m} = β_{j + 1} q_{j + 1} - w_{j j}^{(2)}$ , $ζ_{i j}^{(p)} = w_{i j}^{(p)} - (w_{i - 1, j}^{(p)} - h_{i j}^{(p)} q_{i})$ , and $χ_{i j} = h_{i j} - (h_{i j}^{(1)} + h_{i j}^{(2)})$ . These errors obey $∥ δ_{j}^{m v} ∥_{2} \leq γ_{n} {(\sum_{a = 1}^{n} {(\sum_{b = 1}^{n} ∣ A_{a b} ∣ ∣ q_{j, b} ∣)}^{2})}^{1 / 2}, ∥ δ_{j}^{n o r m} ∥_{2} \leq u ∥ w_{j j}^{(2)} ∥_{2},$ $∣ h_{i j}^{(p)} - q_{i}^{T} w_{i - 1, j}^{(p)} ∣ \leq γ_{n} ∥ q_{i} ∥_{1} ∥ w_{i - 1, j}^{(p)} ∥_{1},$ $∥ ζ_{i j}^{(p)} ∥_{2} \leq γ_{2} (∥ w_{i - 1, j}^{(p)} ∥_{2} + ∣ h_{i j}^{(p)} ∣ ∥ q_{i} ∥_{2}), ∣ χ_{i j} ∣ \leq u ∣ h_{i j}^{(1)} + h_{i j}^{(2)} ∣ .$

If the generated vectors $q_{1}, \dots, q_{m + 1}$ have full column rank, there is also an explicit conditioning-dependent orthogonality recurrence. Put $ν_{ℓ} = ∣ ∥ q_{ℓ} ∥_{2}^{2} - 1 ∣$ and $c_{ℓ i} = q_{ℓ}^{T} q_{i}$ . For fixed $j$ and $ℓ \leq j$ , set $G_{ℓ j}^{0} = ∣ q_{ℓ}^{T} z_{j} ∣ .$ For each pass $p$ , with $h_{i} = h_{i j}^{(p)}$ and $ζ_{i} = ζ_{i j}^{(p)}$ , define $\begin{aligned} G_{ℓ j}^{p} : = & ν_{ℓ} (G_{ℓ j}^{p - 1} + \sum_{i < ℓ} (∣ h_{i} ∣ ∣ c_{ℓ i} ∣ + ∥ q_{ℓ} ∥_{2} ∥ ζ_{i} ∥_{2})) + (1 + ν_{ℓ}) γ_{n} ∥ q_{ℓ} ∥_{1} ∥ w_{ℓ - 1, j}^{(p)} ∥_{1} \\ + ∥ q_{ℓ} ∥_{2} ∥ ζ_{ℓ} ∥_{2} + \sum_{i > ℓ} (∣ h_{i} ∣ ∣ c_{ℓ i} ∣ + ∥ q_{ℓ} ∥_{2} ∥ ζ_{i} ∥_{2}) . \end{aligned}$ Then the off-diagonal inner products satisfy $∣ q_{ℓ}^{T} q_{j + 1} ∣ \leq \frac{G_{ℓ j}^{2}}{β_{j + 1}} + \frac{u ∥ q_{ℓ} ∥_{2}}{c_{n}} .$ Consequently the Frobenius norm of the Gram defect of $Q_{m + 1}$ is at most ${(\sum_{i = 1}^{m + 1} ν_{i}^{2} + 2 \sum_{1 \leq ℓ < i \leq m + 1} {(\frac{G_{ℓ, i - 1}^{2}}{β_{i}} + \frac{u ∥ q_{ℓ} ∥_{2}}{c_{n}})}^{2})}^{1 / 2},$ where $∥ B ∥_{F} = (\sum_{a, b} ∣ B_{a b} ∣^{2})^{1 / 2}$ . A zero $t_{j}$ is a breakdown branch with no division or new vector; failure of any stated rounding or positivity hypothesis makes the bound inconclusive.

Facts & Assumptions

Given: The real matrix, operationwise model and hypotheses in the Statement, the initial vector $q_{1}$ , and the specified two-pass MGS algorithm.

[F1]

The Arnoldi process for building an orthonormal basis of a Krylov subspace: exact Arnoldi subtracts projections onto existing vectors and normalizes the residual; exact zero residual is breakdown.

[F2]

Operationwise real and complex floating point arithmetic with rounded square roots and fused multiply-add: real arithmetic operations round with relative error at most $u$ when they succeed, exact-zero operations return zero, and positive square roots are correctly rounded; for $k u < 1$ , $γ_{k} = k u / (1 - k u)$ .

[F3]

The computed floating-point dot product obeys componentwise and normwise error bounds: when every exact product, rounded product, and intermediate sum is nonzero normal-range, a length- $n$ dot product differs from its exact dot by at most $γ_{n}$ times the sum of the absolute products.

[F4]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: for real vectors, $∣ x^{T} y ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ .

[F5]

If |delta_i| <= u and n u < 1, then prod (1+delta_i) = 1 + theta_n with |theta_n| <= gamma_n: padding any product of at most $n$ factors $1 + ε$ , $∣ ε ∣ \leq u$ , with factors $1$ allows the published $n$ -factor bound $γ_{n}$ when $n u < 1$ .

Proof

1.1givenF2F3F5algebra

Consider any length- $n$ dot product used here. Each exact product and partial sum is either zero or normal-range. By [F2], an exact-zero operation returns zero and contributes a factor $1 + 0$ , while every nonzero successful operation contributes a factor $1 + ε$ with $∣ ε ∣ \leq u$ . Unrolling the left-to-right sum, each exact product has a coefficient that is a product of at most $n$ such factors; padding with factors $1$ and applying [F5] bounds each coefficient's deviation from $1$ by $γ_{n}$ . Therefore the absolute dot-product error is at most $γ_{n}$ times the sum of the absolute exact products, including when exact-zero products or sums occur. This extends the narrower supplier bound [F3] to the operationwise model's exact-zero cases.

1.2givenF2F5algebra

For one component of an update, write the rounded product as $h q_{i} (1 + ϵ_{1})$ and the rounded subtraction as $(w - h q_{i} (1 + ϵ_{1})) (1 + ϵ_{2})$ , with $∣ ϵ_{1} ∣, ∣ ϵ_{2} ∣ \leq u$ ; an exact-zero operation has its corresponding $ϵ$ equal to zero by [F2]. Subtracting $w - h q_{i}$ and using the triangle inequality bounds the component error by $γ_{2} (∣ w ∣ + ∣ h q_{i} ∣)$ . Taking vector norms gives the stated $ζ$ estimate. The rounded addition combining two pass coefficients has error at most $u ∣ h^{(1)} + h^{(2)} ∣$ , including exact-zero sums, which is the stated $χ$ bound.

2.1givenstep 1.1algebra

Apply step 1.1 to each row dot product defining $z_{j}$ . The absolute error in row $a$ is at most $γ_{n} \sum_{b} ∣ A_{a b} ∣ ∣ q_{j, b} ∣$ . Taking the Euclidean norm of this vector of rowwise bounds proves the displayed $δ_{j}^{m v}$ estimate.

2.2givenF2step 1.1algebra

By step 1.1, $∣ t_{j} - ∥ w_{j j}^{(2)} ∥_{2}^{2} ∣ \leq γ_{n} ∥ w_{j j}^{(2)} ∥_{2}^{2}$ , so $t_{j} \geq (1 - γ_{n}) ∥ w_{j j}^{(2)} ∥_{2}^{2}$ . Correct rounding of the positive square root gives $β_{j + 1} \geq (1 - u) \sqrt{t_{j}}$ , proving the lower bound. Each component division gives $q_{j + 1, a} = (w_{j j, a}^{(2)} / β_{j + 1}) (1 + ϵ_{a})$ with $∣ ϵ_{a} ∣ \leq u$ , including zero components with $ϵ_{a} = 0$ ; hence $∣ δ_{j, a}^{n o r m} ∣ \leq u ∣ w_{j j, a}^{(2)} ∣$ and the displayed vector bound follows.

3.1givenF1step 2.1step 1.2step 2.2algebra

The two-pass updates telescope to $w_{j j}^{(2)} = z_{j} - \sum_{p = 1}^{2} \sum_{i = 1}^{j} h_{i j}^{(p)} q_{i} + \sum_{p = 1}^{2} \sum_{i = 1}^{j} ζ_{i j}^{(p)} .$ Also $h_{i j} = h_{i j}^{(1)} + h_{i j}^{(2)} + χ_{i j}$ , $w_{j j}^{(2)} = β_{j + 1} q_{j + 1} - δ_{j}^{n o r m}$ , and $z_{j} = A q_{j} + δ_{j}^{m v}$ . Substituting these identities into the telescoped equation yields $A q_{j} = \sum_{i} h_{i j} q_{i} + β_{j + 1} q_{j + 1} - δ_{j}^{n o r m} - δ_{j}^{m v} - \sum_{p, i} ζ_{i j}^{(p)} - \sum_{i} χ_{i j} q_{i} .$ This is the stated local Arnoldi relation, whose exact-arithmetic column shape is the one defined in [F1].

4.1givenstep 1.1step 1.2step 3.1algebrainduction

Fix $ℓ \leq j$ and one pass. Before its $i = ℓ$ update, the absolute value of $q_{ℓ}^{T} w_{ℓ - 1, j}^{(p)}$ is at most $G_{ℓ j}^{p - 1} + \sum_{i < ℓ} (∣ h_{i} ∣ ∣ c_{ℓ i} ∣ + ∥ q_{ℓ} ∥_{2} ∥ ζ_{i} ∥_{2})$ by the updates already made in this pass. At $i = ℓ$ , write the computed dot as that exact inner product plus a dot error $δ h$ ; then the new inner product is $(1 - ∥ q_{ℓ} ∥_{2}^{2}) q_{ℓ}^{T} w_{ℓ - 1, j}^{(p)} - ∥ q_{ℓ} ∥_{2}^{2} δ h + q_{ℓ}^{T} ζ_{ℓ}$ . Its absolute value is bounded by the first three terms in the definition of $G_{ℓ j}^{p}$ . Each later update $i > ℓ$ changes that inner product by $- h_{i} c_{ℓ i} + q_{ℓ}^{T} ζ_{i}$ , bounded by the corresponding summand there. Thus $∣ q_{ℓ}^{T} w_{j j}^{(p)} ∣ \leq G_{ℓ j}^{p}$ for both passes.

5.1givenstep 2.2step 4.1F4algebra∎

Step 4.1 with $p = 2$ gives $∣ q_{ℓ}^{T} w_{j j}^{(2)} ∣ \leq G_{ℓ j}^{2}$ . Since $β_{j + 1} q_{j + 1} = w_{j j}^{(2)} + δ_{j}^{n o r m}$ , [F4] and step 2.2 yield $∣ q_{ℓ}^{T} q_{j + 1} ∣ \leq G_{ℓ j}^{2} / β_{j + 1} + u ∥ q_{ℓ} ∥_{2} ∥ w_{j j}^{(2)} ∥_{2} / β_{j + 1} \leq G_{ℓ j}^{2} / β_{j + 1} + u ∥ q_{ℓ} ∥_{2} / c_{n} .$ Each diagonal entry of $Q_{m + 1}^{T} Q_{m + 1} - I$ has absolute value $ν_{i}$ , and each off-diagonal entry is bounded by the preceding inequality. Summing the squares of all entries proves the Frobenius Gram-defect bound.

Depends on

Used by

A computed GMRES correction has an explicit finite-precision residual gap Theorem

Dependency tree · two levels

24 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, Accuracy and Stability of Numerical Algorithms, 2nd ed., §§19.8–19.13, printed pp. 415–430 (standard reference, not scraped)
Gene H. Golub and Charles F. Van Loan, Matrix Computations, 4th ed., §§5.2.8–5.2.9, printed pp. 249–255 (standard reference, not scraped)