Finite-Precision Symmetric Krylov Methods: Exact Rounding Examples, Block Paige Identities,and a Variable-Block Lanczos Model
Mohit Sinha
math.NA
Sep 8, 2026 · v1
TL;DR
Key rounding constructions, precision bounds, convergence estimates, and block Lanczos Gram identities are formalized in twelve Lean 4/Mathlib modules with a public repository.
Abstract
Short-recurrence Krylov methods that are equivalent in exact arithmetic often diverge in floating-point arithmetic. To illustrate this, we provide an exactly representable two-cycle for steepest descent with a recursively updated residual. A complementary convergence theorem gives a sufficient condition under which the stored residual decreases geometrically. We then show that a second positive definite family yields different outcomes for a Hestenes–Stiefel Conjugate Gradient (CG) implementation and a direct Lanczos–Galerkin approach. CG finds the exact solution after four updates, whereas the two-step projected system becomes inconsistent. Under stated perturbation and transfer hypotheses, a common spectral enclosure gives comparable convergence bounds. For a dense, left-to-right evaluation order, we prove a sufficient precision bound for a prescribed backward error within $n$ updates for an $n\times n$ matrix, together with a computable stopping test and specified exponent-range assumptions. We use polynomial estimates and numerical experiments to examine the trade-off between working precision and the number of CG iterations needed to achieve a prescribed backward error. We also compare results on inexact matrix-vector products and preconditioning with the frameworks of Paige and Greenbaum. For block Lanczos, we analyze Householder orthogonalization and singular-value truncation as the block size changes. Under componentwise and normwise error bounds, the computed coefficients satisfy a controlled local recurrence and an exact block Lanczos relation for a nearby symmetric problem in a larger space. A block form of Paige's identity bounds the overlap with a Ritz vector along its residual coordinate direction. An inter-block recurrence describes the evolution of overlap, and a Gram-matrix argument gives a count of additional nearby Ritz values.
Problem
Short-recurrence Krylov methods such as steepest descent, CG and Lanczos are equivalent in exact arithmetic but can behave differently in floating point. The work seeks explicit rounding examples, precision bounds for CG backward error, and a finite-precision analysis of variable-block Lanczos.
Approach
Exactly representable constructions show a steepest-descent two-cycle and a case where CG reaches the exact solution while Lanczos–Galerkin gives an inconsistent projected system. A sufficient precision bound for prescribed backward error within n CG updates is proved for left-to-right evaluation. Block Lanczos with Householder orthogonalization and SVD truncation is analyzed through a block Paige identity and Gram-matrix arguments. The constructions are checked by exact rational simulation, and the main proofs are formalized in Lean 4 with Mathlib.
Results
The proofs establish the two-cycle and the CG/Lanczos separation for IEEE precisions under stated exponent-range assumptions. They also give a computable stopping test with a precision bound and a controlled block recurrence for a nearby symmetric problem in a larger space, with counts of nearby Ritz values. Twelve Lean modules build against pinned Mathlib and are released on GitHub.