Second-order term of $g_3(n)$: largest $A\subseteq[n]$ with every product $<3$ times represented (Erdős #796)

For $k\ge 2$ let $g_k(n)$ be the largest possible size of a set $A\subseteq\{1,\ldots,n\}$ such that every integer $m$ has fewer than $k$ representations $m=a_1a_2$ with $a_1<a_2$ and $a_1,a_2\in A$. The leading asymptotics of $g_k(n)$ are known; Erdős asked for the second-order term when $k=3$: is it true that $$g_3(n)=\frac{\log\log n}{\log n}\,n+(c+o(1))\frac{n}{\log n}$$ for some constant $c$?

Acceptance. FULLY RESOLVES: a complete proof (Lean/Coq preferred, else full written) that $g_3(n)=\frac{\log\log n}{\log n}n+(c+o(1))\frac{n}{\log n}$ for an explicit or existentially determined constant $c$ — i.e. that the normalised residual $\big(g_3(n)-\frac{\log\log n}{\log n}n\big)\frac{\log n}{n}$ converges — or a proof that no single such $c$ exists (the residual does not converge). ADVANCES: narrow the gap between the best proven lower and upper constants $c_1\le c_2$ bracketing the residual (improving, in words and with proof or a reproducible certificate, on the values obtainable from the background's [Er64d]/Tang bounds); prove that the second-order term has order $n/\log n$, ruling out the $(\log n)^2$ scale; or a reproducible exact computation of $g_3(n)$ over a certified range of $n$ with the optimisation code and a fitted estimate of $c$ with error bars. Deliver the proof, the improved bracket with proof, or the computation code plus certified $g_3(n)$ values and a fitted $c$.