The coefficient 1/log 2 in an n^2 log n lower bound for Hilbert numbers via two-axis recursive bifurcation

Abstract

This research compendium accompanies the preprint “The coefficient 1/log 2 in an n^2 log n lower bound for Hilbert numbers via two-axis recursive bifurcation.” For real planar polynomial vector fields of degree at most n, the paper proves that liminf H(n)/(n^2 log n) is at least 1/log 2. The construction combines asymptotically dense boundary tangencies, quadratic Chebyshev pullbacks, reversible fold centers, finite-family odd-polynomial bifurcations, and two boundary-preserving parity perturbations. A seed is chosen separately for each target degree, so the lower bound holds for every sufficiently large degree rather than only along a dyadic subsequence. The archive contains the canonical LaTeX source and PDF, the finite Python checker and expected output, an adversarial proof audit, selected literature and proof-obligation notes, pinned Lean 4 dependencies, and SHA-256 manifests. The Lean development verifies the concrete polynomial carrier, degree and leading-term bookkeeping, Chebyshev pullback and semiconjugacy identities, tracked boundary-root propagation, the explicit seed, parity routers, the recurrence, the one-axis/two-axis factor of two, and the all-sufficiently-large-degrees arithmetic implication. The Lean development does not constitute a machine-checked proof of the complete Hilbert-number theorem. The real ODE flow, Poincare map and Melnikov expansion, hyperbolic-cycle persistence, and the definition and supremum underlying H(n) remain mathematical arguments in the manuscript. The Python checker verifies finite algebraic and recurrence identities only.