Rhombus-free edge bound (source code)

= Rhombus-free edge bound

A graph-theoretic rhombus is two triangles sharing an edge. Every rhombus-free graph on $n\geq4$ vertices has at most
$$
e(T_2(n))=\left\lfloor\frac{n^2}{4}\right\rfloor
$$
edges. If the graph is triangle-free this is Turán's theorem. Otherwise remove a triangle: every remaining vertex has at most one neighbor in it, and induction bounds the edge count by
$\lfloor(n-3)^2/4\rfloor+n\leq\lfloor n^2/4\rfloor$.