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

Version 1.2.0 of the research compendium for the preprint “The coefficient 1/log 2 in an n^2 log n lower bound for Hilbert numbers via two-axis recursive bifurcation.” The primary record file is the same 17-page manuscript PDF published in version 1.1.0. This version updates the repository snapshot to include the concrete Lean 4 certificate for the polynomial carrier, exact degree and leading-term bookkeeping, the Chebyshev pullback and semiconjugacy identities, tracked productive boundary-root propagation, the explicit seed, parity routers, and the algebraic one-stage package. The recurrence, two independent constant computations, the exact one-axis/two-axis factor of two, and an all-sufficiently-large-degrees epsilon lower-bound theorem remain kernel checked. The package also includes a namespace-wide axiom-dependency audit and a dedicated statement of the formalization boundary. The Lean development is not a machine-checked proof of the complete Hilbert-number theorem. Its dynamical semantics and analytic one-stage realization remain explicit caller-supplied hypotheses: the development does not formalize the real ODE flow, the Poincare map and Melnikov expansion, hyperbolic-cycle persistence, or the definition and supremum underlying H(n). Those points remain mathematical arguments in the manuscript and were separately audited. The Python checker likewise verifies finite algebraic and recurrence identities only; it is not a substitute for the analytic proof. The record also contains the canonical LaTeX source, the finite Python checker and expected output, the adversarial proof audit, selected literature and proof-obligation notes, pinned Lean dependencies, and SHA-256 manifests. This is a non-peer-reviewed preprint submitted to arXiv as submission 7939202 and awaiting a public identifier.