Let $G$ be a graph on $n$ vertices in which every degree occurs at most twice, and the number of distinct degrees is $>(\frac{1}{2}+\epsilon)n$. Must $G$ contain a trivial (empty or complete) subgraph of size 'much larger' than $\log n$?

1False ↔2  ∀ (ε : ℝ),3    0 < ε →4      ∀ (C : ℝ),5        ∀ᶠ (n : ℕ) in Filter.atTop,6          ∀ (G : SimpleGraph (Fin n)),7            (∀ (d : ℕ), {v | (G.neighborSet v).ncard = d}.ncard ≤ 2) →8              (1 / 2 + ε) * ↑n < ↑(Set.range fun v => (G.neighborSet v).ncard).ncard →9                ∃ s, Erdos1037.IsTrivialSet G s ∧ C * Real.log ↑n < ↑s.ncard