发表机构
Rutgers University（罗格斯大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该工作用 Lean~4 形式化半径多项式方法，通过验证四个范数界和多项式不等式，在数值近似附近证明精确解，并在 Lorenz 系统等实例中验证了存在性、唯一性与解析性。
AI 中文摘要
动力学中的计算机辅助证明通过严格的数值计算建立关于非线性系统的结果。其正确性依赖于可信的区间算术库基础和手工验证的解析估计。我们在 Lean~4 中形式化了一个半径多项式方法的框架，该方法通过验证四个范数界及由此产生的多项式不等式，在数值近似附近证明精确解的存在。加权系数代数为多项式方程和泰勒及切比雪夫级数中的初值问题提供了共同背景。它们的泛性质构造了有界算子和求值映射，自由交换代数的泛性质使得多项式替换与求值可交换。有限/尾部归约将四个范数界转化为有限的理性不等式，并在 Lean 中检查。半径定理随后产生精确的系数解，实现定理将其转化为原始方程的解。工作示例包括由收敛幂级数给出的平方根分支和多项式初值问题，其中包括 Lorenz 系统，该库证明了函数级解在轨迹球内的存在性、唯一性及解析性。
英文摘要
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.
