This repository contains Lean 4 formalizations of algebraic identities, convergence estimates, and spectral results used in the accompanying manuscript on finite-precision symmetric Krylov methods.
The current manuscript is available as a PDF.
Install elan, then run
lake exe cache get
lake build
The files lean-toolchain and lake-manifest.json pin Lean and Mathlib to
version v4.32.1.
| Module | Formalized content |
|---|---|
Problem215.lean |
A two-cycle and its residual identities under abstract round-to-nearest assumptions |
RoundTiesToEven.lean |
Nearest-integer rounding, even tie-breaking, exact integers, and sign symmetry |
BinaryRounding.lean |
Binary significand rounding, subnormal spacing, and asymmetric rounding intervals around powers of two |
Problem215IEEE.lean |
Derivation of the local rounding identities and the two-cycle for bounded-exponent binary formats |
Problem215IEEEExecution.lean |
Finite scalar arithmetic and the true-residual identities at every step of the checked two-cycle |
Problem216.lean |
Algebraic consequences of the stored coefficients and iterate in the Conjugate Gradient and Lanczos separation example |
Problem217.lean |
Local rounding and algebraic facts for the first-step zero-denominator example |
ConditionedNstepBound.lean |
Generic perturbation estimates and forward-to-backward-error bounds |
BlockLanczosCore.lean |
Gram identities, finite telescoping identities, and symmetric-completion algebra |
BlockLanczosGlobal.lean |
Variable-block indexing, nilpotence, and enlarged-space recurrence identities |
BlockLanczosNorms.lean |
Spectral-norm estimates for transport, truncation, completion, and recurrence bounds |
ScalarConvergence.lean |
Finite-spectrum steepest-descent contraction, local-error estimates, and residual stopping tests |
BlockProjection.lean |
Projected recurrence, orthogonal residual decomposition, and the Schur-complement rank formula |
BlockLanczosPaige.lean |
Block Paige identities and bounds, inter-block overlap recurrence, and the overlap-generated trial space |
BlockPaigeFreedom.lean |
The dimension of the affine solution set of the block Paige equations |
RitzMultiplicity.lean |
Eigenvalue counts from trial-space residual bounds and singular-value estimates for physical rank |
KrylovCertificates.lean imports all sixteen modules.
For Problem 2.15, the binary rounding proof applies to every significand
precision p >= 2 under the example's exponent bounds. The precision includes
the leading significand bit. The bounds are verified for binary16, binary32,
binary64, and binary128. Each scalar operation in the checked recurrence is
rounded separately, and every step returns finite values with a nonzero
division denominator. The recursively updated residual equals the true
residual and has squared Euclidean norm two throughout the trajectory.
The rounding model uses the standard binary spacing for normal and subnormal values and rounds a scaled significand to the nearest even integer at ties. It represents signed infinities explicitly and identifies both signed zeros with their common real value. Michael L. Overton's Numerical Computing with IEEE Floating Point Arithmetic, second edition describes the floating-point representation and correctly rounded arithmetic used here.
The sources contain no sorry, admit, custom axiom declaration, or
unsafe declaration. The reported foundational dependencies are
propext, Classical.choice, and Quot.sound.
The module names Problem215, Problem216, Problem217, and the block
Lanczos modules refer to Problems 2.15--2.19 in Linear Systems and Eigenvalue
Problems: Open Questions from a Simons Workshop,
arXiv:2602.05394v3.
The enlarged-space construction in the block modules extends the scalar construction in Tyler Chen, A Simple Stability Analysis of the Lanczos Algorithm in Finite Precision Arithmetic, arXiv:2608.21268v1.
Licensed under the Apache License, Version 2.0.