Diameter of $K_{k+1}$-free graphs with minimum degree $d$: is it at most $(3-2/k)n/d$? (Erdős #612)

Let $G$ be a connected graph on $n$ vertices with minimum degree $d$ and diameter $D$ (the largest shortest-path distance between two vertices). Every connected graph satisfies the general bound $D\leq 3\frac{n}{d+1}+O(1)$; the question is how much forbidding a fixed clique improves it. Erdős, Pach, Pollack, and Tuza originally conjectured two sharp bounds: if $G$ contains no $K_{2r}$ and $(r-1)(3r+2)\mid d$ then $$D\leq \frac{2(r-1)(3r+2)}{2r^2-1}\frac{n}{d}+O(1),$$ and if $G$ contains no $K_{2r+1}$ and $3r-1\mid d$ then $$D\leq \frac{3r-1}{r}\frac{n}{d}+O(1).$$ These original bounds are now known to be FALSE for $r\geq 2$. The current open target is the amended single-case conjecture of Czabarka, Singgih, and Székely: if $G$ is a connected graph on $n$ vertices with minimum degree $d$ that contains no $K_{k+1}$, then $$D\leq \left(3-\tfrac{2}{k}\right)\frac{n}{d}+O(1).$$ Prove or disprove this amended bound, and thereby determine the correct extremal dependence of diameter on $n$, $d$, and the forbidden clique size.

Acceptance. FULLY RESOLVES: settle the amended Czabarka–Singgih–Székely conjecture — either a complete proof (machine-checkable in Lean/Coq preferred, else a full written proof) that every connected $K_{k+1}$-free graph on $n$ vertices with minimum degree $d$ has diameter $D\leq(3-2/k)n/d+O(1)$, or an explicit infinite (parametric) family of connected $K_{k+1}$-free graphs whose diameter provably exceeds $(3-2/k)n/d$ by a positive constant factor, with clique-freeness, minimum degree, vertex count, and diameter all certified. ADVANCES: for a fixed small $k$ (e.g. $k=3$, the $K_4$-free case), construct a connected $K_{k+1}$-free graph family with minimum degree $d$ whose diameter has leading coefficient strictly better than the best lower construction stated in the background (currently $\frac{31}{216}$ for the $K_4$-free case), delivered as an explicit graph generator plus a verifier checking clique-freeness, degree, and diameter; or prove the amended upper bound for a new value of $k$ under the genuine clique-freeness hypothesis (not merely $k$-colourability). Deliver the proof file, or the parametric construction plus verification code and the attained diameter coefficient.