A Lean~4 Framework for the Radii Polynomial Method

Abstract

Computer-assisted proofs in dynamics establish results about nonlinear systems by rigorous numerical computation. Their correctness rests on a trusted base of interval-arithmetic libraries and analytic estimates checked by hand. We formalize in Lean~4 a framework for the radii polynomial method, which certifies an exact solution near a numerical approximation by verifying four norm bounds and the resulting polynomial inequality. Weighted coefficient algebras provide the common setting for polynomial equations and initial value problems in Taylor and Chebyshev series. Their universal properties construct the bounded operators and the evaluation maps, and the universal property of the free commutative algebra makes polynomial substitution commute with evaluation. Finite/tail reductions turn the four norm bounds into finite rational inequalities, which are checked in Lean. The radii theorem then yields an exact coefficient solution, and realization theorems carry it to a solution of the original equation. The worked examples are a square-root branch given by a convergent power series and polynomial initial value problems, among them the Lorenz system, for which the library proves existence, uniqueness within the trajectory ball, and analyticity of the function-level solution.