Estimate g(n): the largest sum-avoiding subset guaranteed inside every n-element set of reals (Erdős #787)

For a finite set $A\subset\mathbb{R}$, say $B\subseteq A$ is sum-avoiding in $A$ if $b_1+b_2\notin A$ for all distinct $b_1,b_2\in B$. Let $g(n)$ be the largest integer such that EVERY set $A\subset\mathbb{R}$ with $\lvert A\rvert=n$ contains a sum-avoiding subset $B$ with $\lvert B\rvert\geq g(n)$. Estimate $g(n)$.

Acceptance. FULLY RESOLVES: a proof determining the growth type of $g(n)$ — upper and lower bounds of matching shape (e.g. $g(n)=(\log n)^{\alpha+o(1)}$ for an explicit $\alpha$, or $g(n)=\exp(\Theta(\sqrt{\log n}))$), closing the polylog-versus-$\exp(\sqrt{\log})$ gap described in the background; machine-checkable (Lean/Coq) preferred, else a complete written proof with all steps. ADVANCES: (a) a proven lower bound strictly stronger than the best lower bound stated in the background (Beker's $(\log n)^{1+1/68+o(1)}$) — e.g. a larger explicit exponent or a qualitatively larger bound; (b) a proven upper bound strictly stronger than the $\exp(\sqrt{\log n})$ bound stated in the background (e.g. an improved constant in the exponent, via an explicit construction with proof); (c) certified small-$n$ data: explicit witness sets $A\subset\mathbb{Z}$ with $\lvert A\rvert=n$ together with verification code certifying the exact maximum sum-avoiding subset size of each, giving upper bounds on $g(n)$ at concrete $n$ beyond what the constructions cited in the background yield; (d) a Lean formalisation of one of the known bounds. Deliver the proof file, or the witnesses plus verification code.