A Lean~4 Framework for the Radii Polynomial Method
Abstract
Understanding nonlinear dynamics is central to many fields of study, yet most nonlinear systems are beyond the reach of closed-form solutions. Numerical simulation is then used to reveal dynamical structures before their existence can be established. This alone, however, leaves the validity of the computed solution unanswered. Rigorous numerical methods address this gap by combining computation with explicit analytic estimates. Among them, the radii polynomial approach, a Newton--Kantorovich type argument, turns a numerical approximation into a proof of existence and uniqueness of a true solution near that approximation. In previous practice, the verification of these inequalities relies on interval-arithmetic libraries and hand-derived algebraic bounds. In this paper, we present a framework for the radii polynomial method in the Lean~4, which turns numerical certificates into fully type-checked theorems about the true solution. A central challenge in this process is to manage the complexity of the formalization. Our approach begins with a family of problems and their common structure. The spaces in which the analysis takes place are developed through universal properties in suitable categories, with extension properties that characterize maps by their action on generators. These properties guide the design of a reusable interface such that problem-specific arguments concentrate on the numerical data and the algebraic bounds that distinguish one equation from another. We formalize a general radii polynomial theorem, develop weighted coefficient algebras and reusable operator estimates, connect finite computational checks to the hypotheses of the theorem, and establish the realization theorems that transport certified coefficient space zeros to analytic solutions of the original equations.
Related
- A Mixed-Adjoint Framework for 2 × 2 Operator Matrices and Their Numerical Radii
- Global Regularity for the 3D Incompressible Navier–Stokes Equations via the Frohmanian Symplectic Tether: Lean 4 Formalization and Conditional Cubic Comparison Framework (v2.1)
- A Hybrid Fibonacci Polynomial–Block-Pulse Method for Fractional Pantograph Differential Equations
- A polynomial method over formal power series
- Second-Order Least Squares as a Special Case of the Polynomial Maximization Method
BibTeX
@misc{wang2026lean4,
title = {{A Lean~4 Framework for the Radii Polynomial Method}},
author = {Fengyang Wang and Konstantin Mischaikow and Marcio Gameiro},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.02335},
eprint = {2610.02335},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.02335},
}
RIS
TY - UNPB
TI - A Lean~4 Framework for the Radii Polynomial Method
AU - Fengyang Wang
AU - Konstantin Mischaikow
AU - Marcio Gameiro
PY - 2026
DA - 2026/10/26
PB - arXiv
DO - 10.48550/arxiv.2610.02335
UR - https://arxiv.org/abs/2610.02335
AB - Understanding nonlinear dynamics is central to many fields of study, yet most nonlinear systems are beyond the reach of closed-form solutions. Numerical simulation is then used to reveal dynamical structures before their existence can be established. This alone, however, leaves the validity of the computed solution unanswered. Rigorous numerical methods address this gap by combining computation with explicit analytic estimates. Among them, the radii polynomial approach, a Newton--Kantorovich type argument, turns a numerical approximation into a proof of existence and uniqueness of a true solution near that approximation. In previous practice, the verification of these inequalities relies on interval-arithmetic libraries and hand-derived algebraic bounds. In this paper, we present a framework for the radii polynomial method in the Lean~4, which turns numerical certificates into fully type-checked theorems about the true solution. A central challenge in this process is to manage the complexity of the formalization. Our approach begins with a family of problems and their common structure. The spaces in which the analysis takes place are developed through universal properties in suitable categories, with extension properties that characterize maps by their action on generators. These properties guide the design of a reusable interface such that problem-specific arguments concentrate on the numerical data and the algebraic bounds that distinguish one equation from another. We formalize a general radii polynomial theorem, develop weighted coefficient algebras and reusable operator estimates, connect finite computational checks to the hypotheses of the theorem, and establish the realization theorems that transport certified coefficient space zeros to analytic solutions of the original equations.
ER -