Hierarchical Melnikov Realization: Logarithmic Factor Improvement to Hilbert Number Lower Bounds
Chaoyang Qin, Xiaoming Sun
math.DS
Oct 8, 2026 · v1
math.CA
TL;DR
The full limit-cycle construction and the H(d) lower bounds are formalized in Lean 4 with Mathlib, with no placeholders or project axioms.
Abstract
The second part of Hilbert's 16th problem is one of the most fundamental open problems in the qualitative theory of ordinary differential equations and dynamical systems. A central unresolved question is whether the Hilbert number $H(d)$ is finite for arbitrary polynomial degree $d$. (A very recent manuscript from OpenAI asserts the finiteness of $H(d)$; see the remark at the end of this paper.) In the absence of a general upper bound theory, most existing work constructs explicit perturbed polynomial systems to obtain improved lower bounds for $H(d)$, while rigorous upper bound estimates remain largely unavailable. This paper focuses on improving the quantitative lower bound for polynomial systems through a systematic Hierarchical Melnikov Realization framework. We construct perturbed dynamics based on an anisotropic Chebyshev Hamiltonian, where hierarchically selected perturbation coefficients generate simple zeros of the first-order Melnikov function simultaneously across multiple disjoint period annuli. Two distinct 3-adic filtrations supply the necessary logarithmic correction factors, and a Borel–Gauss analysis establishes the required local rank condition under sufficiently strong anisotropy. As the main result of this work, we prove that $H(d)=Ω\bigl(d^2\ln^2 d\bigr)$, which improves the previously known lower bound by a factor of $\ln d$. The full construction of limit cycles and the resulting dynamical bounds are formally certified using Lean 4 formal verification.
Problem
The second part of Hilbert's 16th problem asks about the Hilbert number H(d), the maximum number of limit cycles of degree-d planar polynomial vector fields. The best known lower bound was of order d^2 ln d.
Approach
Perturbed systems are built from an anisotropic Chebyshev Hamiltonian with n^2 nondegenerate centers. Hierarchically chosen perturbation coefficients produce simple zeros of the first-order Melnikov function across many period annuli at once. Two 3-adic filtrations supply the logarithmic factors, and a Borel–Gauss analysis gives the needed local rank condition. The construction is formalized in Lean 4 with Mathlib, covering Poincaré return maps, hyperbolicity, and the counting bounds.
Results
The paper proves H(d) = Ω(d^2 ln^2 d), improving the previous lower bound by a factor of ln d. The Lean development proves existence of polynomial vector fields with injective families of hyperbolic limit cycles meeting explicit bounds for every d ≥ 31. The proof uses no unproved placeholders and no project-specific axioms.
