Dense clique family blow-up lemma (source code)

= Dense clique family blow-up lemma
{title2=$|\mathcal M|\ge\eta n^s\Longrightarrow K_s(\lfloor a\log n\rfloor)\subseteq G$}

A family of positively many $s$-cliques forces a logarithmic balanced <graph blow-up>, which can also contain a matching of that many members of the family. To induct on $s$, prune faces with few extensions, apply induction to the remaining $(s-1)$-faces, and use a matching of those faces as one side of a bipartite incidence <graph>. The <common neighbourhood from bipartite density> estimate selects logarithmically many disjoint faces with polynomially many common extension <vertices>.