Does a dense $K_{2,2,2}$-free graph force a linear-size independent set? (Erdős #579)

Let $K_{2,2,2}$ be the complete tripartite graph with three parts of size $2$ (the octahedron): $6$ vertices, with all edges between different parts. Conjecture (Erdős–Hajnal–Sós–Szemerédi): for every $\delta>0$ there is a constant $c=c(\delta)>0$ such that, whenever $n$ is sufficiently large, every graph $G$ on $n$ vertices that contains no $K_{2,2,2}$ and has at least $\delta n^2$ edges contains an independent set of size at least $cn$. In words: octahedron-freeness together with positive edge density $\gg n^2$ forces an independent set of size $\gg n$.

Acceptance. FULLY RESOLVES: a complete proof that for every $\delta>0$ there is $c(\delta)>0$ such that every large $K_{2,2,2}$-free $n$-vertex graph with $\ge\delta n^2$ edges has an independent set of size $\ge c n$ (Lean/Coq preferred, else a full written proof); OR a disproof — for some fixed $\delta>0$, an explicit construction of $K_{2,2,2}$-free $n$-vertex graphs with $\ge\delta n^2$ edges whose independence number is $o(n)$, with proof. ADVANCES: lower the density threshold below $\delta=1/8$ — prove the implication for some fixed $\delta<1/8$ — with complete proof, strictly improving the best threshold stated in the background; or an extremal construction that narrows the range in which the conclusion could fail. Deliver the proof file, or the construction together with certified edge-density and independence-number data.