arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 2610.02335

A Lean~4 Framework for the Radii Polynomial Method

Fengyang Wang
View original source ↗Read source document ↗Export metadata ↓

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.

Explore related subjects

math.DS

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Fengyang Wang. 2026-10-01. A Lean~4 Framework for the Radii Polynomial Method. https://arxiv.org/abs/2610.02335

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Topological structure of the sum of two affine Cantor sets

We introduce a dense subset of affine Cantor sets, termed "generalized homogeneous Cantor sets." We show that for any two members of this class, if their sum set is not a Cantor set, it has a dense interior. If one of them is an affine Cantor set with two mappings, the same result holds. In the contex of affine Cantor sets defined by increasing maps, we introduce a dense subset of their pairs, denoted by $\cal{D}$, such that for every $(K, K') \in \cal{D}$, there are five possible structures for their sum set: a bilateral gap interval, an L, R, M-Cantorval, or a Cantor set. Finally, we present new pairs of affine Cantor sets which have stable intersection, while do not satisfy the Generalized Thickness Test.

math.DS↗
arXiv2026

Similarity and superrigidity for transverse measured groupoids

Let $G$ be a locally compact, second countable, unimodular group and let $(X,μ,Y)$ be an ergodic integrable transverse $G$-system. We show that $G \ltimes X$ endowed with the product measure and the restriction $(G \ltimes X)|_Y$ endowed with the transverse measure are similar ergodic groupoids. As a consequence, we prove a superrigidity phenomenon for higher rank transverse groupoids. More precisely, for $i=1,\ldots,k$, let $\mathbf{G}_i$ be a connected, simply connected, semisimple algebraic group over some local field $κ_i$ of characteristic zero. Let $G_i=\mathbf{G}_i(κ_i)$ be the $κ_i$-points of $\mathbf{G}_i$ and denote by $G=\prod_{i=1}^k G_i$. If we assume that $G$ has higher rank and each factor has positive rank, given an ergodic integrable transverse $G$-system $(X,μ,Y)$, we prove that any unbounded Zariski dense morphism of the transverse groupoid $(G \ltimes X)|_Y$ into either an almost simple or a reductive algebraic group is superrigid.

math.DS↗
arXiv2026

Abelian maximal pattern complexity and extremal words

In this paper, we study the Abelian maximal pattern complexity $p_α^{\ast \mathrm{ab}}(k)$, introduced by Kamae, Widmer and Zamboni, of infinite words $α\in \mathbb{A}^{\mathbb{N}_{0}}$ over finite alphabets $\mathbb{A}$. For recurrent aperiodic words, we determine a lower bound and prove its sharpness. We further give a structural characterization of the words with minimal Abelian maximal pattern complexity. In the general case, we prove that an infinite word $α$ is aperiodic if and only if $\binom{p_{α}^{\ast \mathrm{ab}}(k)}{2}\geq k$ for every $k.$ For aperiodic words over $\ell \geq 2$ letters, each occurring infinitely often, we further prove that $p_{α}^{\ast \mathrm{ab}}(k)\geq m$ whenever $\binom{m}{2}\leq (\ell -1)(k-\ell +2)$, for all $m,k$. Together with a matching construction, this shows that the minimum Abelian maximal pattern complexity in this class is $\sqrt{2(\ell -1)k}+O_{\ell }(1)$. We call a word an Abelian pattern Sturmian word if, at every $k$, its Abelian maximal pattern complexity is the least positive integer $m$ satisfying $\binom{m}{2}\geq k$. We show that a word is Abelian pattern Sturmian if and only if, after relabeling its alphabet, it is the characteristic word of an infinite set $E\subset \mathbb{N}_{0}$ for which the bipartite graph on two disjoint copies of $\mathbb{N}_{0}$, with a left vertex $r$ adjacent to a right vertex $s$ exactly when $r+s\in E$, is a forest.

math.DS↗