Fewest edges of a pancyclic graph: pin down h(n) between log_2 n and log_2 n + log_* n (Erdős #1016)

A graph on $n$ vertices is pancyclic if it contains a cycle on exactly $k$ vertices for every $3 \le k \le n$. Let $h(n)$ be minimal such that there is a pancyclic graph on $n$ vertices with $n + h(n)$ edges. Estimate $h(n)$. In particular, is it true that $$h(n) \ge \log_2 n + \log_* n - O(1),$$ where $\log_* n$ is the iterated logarithm (the number of times $\log_2$ must be applied to $n$ before the result drops to at most $1$)? Together with the known upper bound $h(n) \le \log_2 n + \log_* n + O(1)$, a positive answer would determine $h(n)$ up to an additive constant.

Acceptance. FULLY RESOLVES: a complete proof that $h(n) \ge \log_2 n + \log_* n - O(1)$ (machine-checkable Lean/Coq preferred, else a full written proof), which together with the known upper bound pins $h(n)$ to an additive $O(1)$; OR a proof that $h(n) \le \log_2 n + o(\log_* n) + O(1)$-type improvements of the upper bound showing the conjectured lower bound is false, i.e. constructions with fewer edges, with full proofs of pancyclicity and the counting. ADVANCES: (a) a proof that $h(n) - \log_2 n \to \infty$ (explicitly open per the background), with proof; (b) any lower bound with a strictly larger growth than the $\log_2(n-1) - 1$ bound stated in the background, or any upper-bound improvement strictly below the bound stated in the background, with proof; (c) exact values of $h(n)$ for small $n$ (with witness pancyclic graphs and a proof of minimality by exhaustive search), extending the known data/OEIS A105206, accompanied by the search code and an exhaustiveness certificate; (d) a machine-verified (Lean) proof of either published bound. Deliver the proof file (or compiling Lean sources), or the enumeration code plus the certified table of exact $h(n)$ values and witness graphs.