Girth versus chromatic number: do $g_k(n)/\log n$ and $\log h^{(m)}(n)/\log n$ have limits? (Erdős #626)

Let $k\geq 4$ and let $g_k(n)$ denote the largest $m$ such that there is a graph on $n$ vertices with chromatic number $k$ and girth $>m$ (i.e. containing no cycle of length $\leq m$). Does $$\lim_{n\to\infty}\frac{g_k(n)}{\log n}$$ exist? Conversely, if $h^{(m)}(n)$ is the maximal chromatic number of a graph on $n$ vertices with girth $>m$, does $$\lim_{n\to\infty}\frac{\log h^{(m)}(n)}{\log n}$$ exist, and what is its value?

Acceptance. FULLY RESOLVES: proofs (machine-checkable Lean/Coq preferred, else full written proofs) settling BOTH displayed questions: (a) for every $k\geq 4$, whether $\lim_n g_k(n)/\log n$ exists (and if so its value), and (b) for every $m$, whether $\lim_n \log h^{(m)}(n)/\log n$ exists together with its value. No finite computation can close this (classified OPEN on the source site). ADVANCES: settling either question alone, or for a single $k$ or $m$ (the first open target: the even case $m=4$, i.e. the exponent for graphs with no cycle of length $\leq 4$); narrowing the constant gap in the two-sided bound on $g_k(n)/\log n$ stated in the background (improving Kostochka's lower constant or Erdős's upper constant), with proof; proving the odd-$m$ conjectured value $2/(m+1)$ is attained in the limit for any odd $m$; or a reproducible exact-values computation of $g_k(n)$ or $h^{(m)}(n)$ for small parameters (with SAT/ILP code and machine-verifiable optimality certificates) extending what is in the literature. Deliver the proof file, or the code plus certificates and the resulting table of exact values.