Four-point near-Sidon sets: the best constant $c$ forcing a Sidon subset of size $cn$ (Erdős #757)

A Sidon set is a set whose pairwise differences are all distinct; for a $4$-element Sidon set $B$ the difference set $B-B=\{b-b' : b,b'\in B\}$ has exactly $13$ elements. Let $A\subset\mathbb{R}$ be a set of size $n$ such that every subset $B\subseteq A$ with $\lvert B\rvert = 4$ has $\lvert B-B\rvert\geq 11$ — i.e. at most one difference is 'missing' from each four-point pattern. Find the best constant $c>0$ such that $A$ must always contain a Sidon set of size $\geq cn$. Equivalently (in distance language): if every four points of $A$ determine at least five distinct distances, how large a subset with all pairwise distances distinct is guaranteed?

Acceptance. FULLY RESOLVES: determine the optimal constant $c$ exactly — a proof of $c\geq c_0$ (every size-$n$ set satisfying the 4-subset condition contains a Sidon subset of size $\geq (c_0-o(1))n$) together with a matching construction family showing $c\leq c_0$; machine-checkable (Lean/Coq) preferred, else a complete written proof. ADVANCES: (a) a lower bound on $c$ strictly greater than the best lower bound stated in the background, with full proof; (b) an upper bound strictly smaller than the best upper bound stated in the background, via an explicit infinite family of sets satisfying the hypothesis whose largest Sidon subsets are asymptotically small — with proof, plus verification code for finite members; (c) certified exact values of the finite extremal ratio $\min_A \max\{|S| : S\subseteq A \text{ Sidon}\}/n$ for small $n$ via exhaustive or SAT search with an exhaustiveness certificate; (d) a Lean formalization of the current record bounds. Deliver the proof file, or the construction family + verification code, or the search code + certified table.