An $n^2 \log n$ lower bound with coefficient $1/\log 2$ for the Hilbert number of polynomial systems

This record accompanies the preprint “An n^2 log n lower bound with coefficient 1/log 2 for the Hilbert number of polynomial systems.” For real planar polynomial vector fields of degree at most n, the paper proves the candidate bound liminf H(n)/(n^2 log n) ≥ 1/log 2. The construction combines asymptotically dense nondegenerate quadratic boundary tangencies, quadratic Chebyshev pullbacks, finite families of reversible centers, simultaneous odd-polynomial Melnikov bifurcations, and two successive boundary-vanishing perturbations. The initial system is chosen separately for each target degree, so the bound holds for every sufficiently large degree rather than only along a dyadic subsequence. Version 1.6.0 contains only publication-related materials: the canonical 27-page PDF, the self-contained LaTeX source, and a curated verification supplement containing the Python checker, Lean 4 sources with pinned dependencies, a reader-facing verification-scope document, and the software license. The Lean development machine-checks the concrete polynomial algebra, multiscale exponent and determinant calculations, typed two-axis family assembly conditional on supplied analytic cycle-family witnesses, and the recurrence and all-degree asymptotic arithmetic. It is not a machine-checked proof of the complete Hilbert-number theorem: the analytic center theorem, Poincaré–Pontryagin expansion, common perturbation thresholds, and hyperbolic persistence remain mathematical arguments in the manuscript.