Avoiding a sum-free set: a continuum-size $A$ with $A+A$ disjoint from $S$? (Erdős #949)

Let $S\subseteq\mathbb{R}$ be a sum-free set, meaning there are no $a,b,c\in S$ (not necessarily distinct) with $a+b=c$. Must there always exist a set $A\subseteq\mathbb{R}\setminus S$ of cardinality continuum such that $A+A\subseteq\mathbb{R}\setminus S$? That is, both $A$ and every pairwise sum $a+a'$ with $a,a'\in A$ avoid $S$, while $\lvert A\rvert=\mathfrak{c}$.

Acceptance. FULLY RESOLVES: a complete proof (machine-checkable in Lean/Coq preferred, given the Lean formalisation and the AlphaProof precedent on the Sidon variant) either that for every sum-free $S\subseteq\mathbb{R}$ there exists $A\subseteq\mathbb{R}\setminus S$ with $\lvert A\rvert=\mathfrak{c}$ and $A+A\subseteq\mathbb{R}\setminus S$, OR a counterexample: an explicitly described sum-free $S$ admitting no continuum-sized $A$ with $A+A\subseteq\mathbb{R}\setminus S$, with proof. ADVANCES: a proof establishing the property for a class of sum-free sets strictly larger than the already-settled Sidon case (e.g. all measurable $S$, or $S$ of a specified structural type), with full proof; or a proof of the general case under an explicitly stated additional hypothesis, or a reduction to a checkable finitary statement. Deliver the proof / formal development or the certified counterexample.