分层梅尔尼科夫实现：希尔伯特数下界的对数因子改进
Hierarchical Melnikov Realization: Logarithmic Factor Improvement to Hilbert Number Lower Bounds
- State Key Lab of Processors, Institute of Computing TechnologyChinese Academy of Sciences（处理器国家重点实验室，中国科学院计算技术研究所）
- School of Computer Science and TechnologyUniversity of Chinese Academy of Sciences（中国科学技术大学计算机科学与技术学院）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本文针对希尔伯特第16问题，提出分层梅尔尼科夫实现框架，构造受扰多项式系统将希尔伯特数下界提升至Ω(d²ln²d)，并通过Lean 4完成形式化验证。
AI中文摘要：
希尔伯特第16问题的第二部分是常微分方程与动力系统定性理论中最基础的公开问题之一，核心未解决问题是对任意多项式次数d，希尔伯特数H(d)是否有限（OpenAI最新手稿断言H(d)有限，见本文末尾注记）。在缺乏通用上界理论的情况下，现有多数工作通过构造显式受扰多项式系统来改进H(d)的下界，而严格上界估计仍基本缺失。本文聚焦于通过系统的分层梅尔尼科夫实现框架改进多项式系统的定量下界：基于各向异性切比雪夫哈密顿量构造受扰动力学，分层选取的扰动系数在多个不相交周期环域上同时生成一阶梅尔尼科夫函数的简单零点；两种不同的3进滤子提供所需的对数修正因子，Borel–Gauss分析在足够强的各向异性下建立了所需的局部秩条件。本文主要结果为证明H(d)=Ω(d²ln²d)，较此前已知下界提升了ln d倍；极限环的完整构造及所得动力学界均通过Lean 4形式化验证得到正式认证。
英文摘要：
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.
