Infinite Sidon sets: is $\liminf A(x)(\log x/x)^{1/2}=0$, or can $(\log x)^c$ stay positive? (Erdős #1191)

Let $A\subset\mathbb{N}$ be an infinite Sidon set (all pairwise sums $a+b$ with $a\le b$ distinct) and write $A(x)=\lvert A\cap[1,x]\rvert$ for its counting function. Two questions: (1) Is it true that for every infinite Sidon set $$\liminf_{x\to\infty} \frac{A(x)}{x^{1/2}}(\log x)^{1/2}=0?$$ (2) Does there exist an infinite Sidon set $A$ and some $c>0$ such that $$\liminf_{x\to\infty} \frac{A(x)}{x^{1/2}}(\log x)^{c}>0?$$

Acceptance. FULLY RESOLVES: a complete proof (machine-checkable preferred, else full written proof) answering question (1) — either that the liminf is $0$ for every infinite Sidon set, or an explicit infinite Sidon set with proof that its liminf is positive (which would also answer (2) with $c=1/2$); or answering question (2) — an explicit infinite Sidon set and $c>0$ with proof that $\liminf A(x)(\log x)^c/x^{1/2}>0$, or a proof that no such set exists. A submission fully answering either numbered question with proof counts as resolving; state clearly which. No finite computation can settle these. ADVANCES: (a) an explicit admissible constant $c$ in Erdős's theorem ($\liminf A(x)(\log x)^{1/2}/x^{1/2}\le c$ for all infinite Sidon sets), or any strict improvement of the weight function beyond $(\log x)^{1/2}$ stated in the background, with proof; (b) a construction of an infinite Sidon set with $\liminf A(x)g(x)/x^{1/2}>0$ for any weight $g$ growing faster than the polynomial-loss constructions stated in the background (e.g. beating $A(x)\gg x^{\sqrt{2}-1}$ at every scale), with proof; (c) a proof of (1) restricted to a natural class (e.g. perfect difference set unions, greedy-type sets); (d) a Lean formalization of Erdős's liminf upper bound theorem. Deliver the proof file or the construction plus proof.