Does the mean-square gap of the sumset of a finite Sidon set tend to infinity? (Erdős #153)

A finite set $A\subseteq\mathbb{Z}$ is a Sidon set (a $B_2$ set) if all pairwise sums $a+a'$ ($a\le a'$) are distinct, equivalently every nonzero integer has at most one representation as a difference of two elements of $A$. For a finite Sidon set $A$ write its sumset in increasing order as $A+A=\{s_1<s_2<\cdots<s_t\}$ (so $t=\binom{|A|+1}{2}$). Is it true that the mean square of the consecutive gaps of the sumset, $$\frac{1}{t}\sum_{1\le i<t}(s_{i+1}-s_i)^2,$$ tends to infinity as $\lvert A\rvert\to\infty$? In other words, must the gaps of $A+A$ become, on average of their squares, unboundedly large for large Sidon sets?

Acceptance. FULLY RESOLVES: a complete proof (machine-checkable in Lean/Coq preferred, else fully written) that $\frac{1}{t}\sum_{1\le i<t}(s_{i+1}-s_i)^2\to\infty$ as $\lvert A\rvert\to\infty$ over all finite Sidon sets, OR a construction of an infinite family of finite Sidon sets with $\lvert A\rvert\to\infty$ along which this mean-square gap stays bounded, with a proof of the bound. ADVANCES (each with proof or a reproducible certificate): a proof that the quantity is bounded below by an explicit increasing function of $\lvert A\rvert$ (e.g. $\gg\log\lvert A\rvert$), strictly improving on any bound stated in the background; a matching upper bound on the extremal (slowest-growing) family; or a rigorously verified computation extending the mean-square-gap data for optimal/near-optimal Sidon sets to a new record size, with the search code and the Sidon-verification certificate. Deliver the written/formalised proof, or the construction, or the search program plus the tabulated statistic and its exhaustiveness/verification certificate.