Global Convergence and Reliable Stopping in a Safeguarded Modified Anderson–Björck Method
Latchezar Tomov, Nedelcho Ganchovski
math.NA
Oct 9, 2026 · v1
TL;DR
Global convergence, bracket invariants, and binary64 rounding-error bounds of the switching criterion are formalized in Lean 4 using mathlib and FloatLib.
Abstract
The modified Anderson-Bjorck (modAB) method was first proposed in 2023 by Ganchovski and Traykov for solving nonlinear equations in structural mechanics. It was improved further in 2026 by introducing better switching criteria with account to function symmetry, and bisection fallback based on measuring the bracket reduction rate. Although the algorithm demonstrated superior performance across a great variety of functions, it lacked formal mathematical analysis and proof of convergence. In addition, some discrepancies were noted by L. Tomov in the latest version that need to be addressed: premature application of the Anderson-Bjorck (AB) correction on the first AB step, caused by retaining the endpoint-update record from the preceding bisection step, and using the corrected endpoint ordinates in symmetry factor calculation instead of the true residuals. The purpose of the present paper is to provide rigorous mathematical proof of global convergence in exact arithmetic, remove the above discrepancies, and provide floating-point safeguards for interpolation, switching and stopping, with explicit treatment of infinite and NaN values, underflow, overflow and round-off errors. These safeguards do not certify the accuracy of the supplied function values. Additional performance improvement was introduced by allowing for early bisection fallback when AB fails to make progress on reducing either the bracket width or the residual, while retaining a finite bound on consecutive exceptions to the prescribed width condition.
Problem
The modified Anderson–Björck (modAB) bracketing root-finder had no formal convergence proof. Its implementation also had flaws: a premature AB correction after bisection, and symmetry factors computed from corrected ordinates instead of true residuals.
Approach
The method is reformulated so that true function values are kept separate from AB-modified ordinates. Global convergence is proved by combining bracket invariants with a geometrically shrinking reference width per AB phase and a bisection fallback. A finite number of residual-based exceptions is allowed. Floating-point safeguards handle NaN, infinity, underflow and overflow, and stopping. The switching criterion's rounding analysis, the bracket and width bounds, and exact-arithmetic convergence are checked in Lean 4 with mathlib and FloatLib, including a translation of the 17-operation C# switching expression.
Results
The method is proved to converge globally in exact arithmetic, with an explicit iteration bound (C=32, factor 7). Formally verified error bounds are given for the binary64 switching test. A corrected C# implementation and a revised benchmark validated against reference roots show improved performance on the test set.
