Four-step path lemma for a dense bipartite graph (source code)

= Four-step path lemma for a dense bipartite graph
{title2=$|B|\geq\rho n/4,\quad\#\text{ four-edge walks}\geq\rho^5n^3/4096$}

Let a <bipartite graph> have $n$ vertices in each class and at least $\rho n^2$ edges. There is a subset $B$ of one class with $|B|\geq\rho n/4$ such that every pair of its vertices has at least $\rho^5n^3/4096$ four-edge walks between them. Declare a pair of left vertices bad if it has fewer than $\tau n$ common neighbours, with $\tau=\rho^2/32$. For a random right vertex $y$, put $U=N(y)$ and let $b(U)$ count ordered bad pairs inside $U$. Then $\mathbb E|U|\geq\rho n$ and $\mathbb Eb(U)\leq\tau n^2$. Some $y$ has $|U|-16b(U)/(\rho n)\geq\rho n/2$, so $|U|\geq\rho n/2$ and $b(U)\leq|U|^2/8$. Remove vertices with more than $|U|/4$ bad partners. At least half remain. For any two remaining vertices, at least $|U|/2$ middle vertices are good partners of both. Each supplies at least $(\tau n)^2$ walks, giving the bound.