Lemma 2.1 — $\lambda_1 n \le \rho^{-2}(1/a + 1/b)(|E| - |E_A| - |E_B|)$

Let $G = (V, E)$ be a connected finite simple graph on $n \ge 2$ vertices and $\lambda_1 = \lambda_1(G)$ the second-smallest eigenvalue of its Laplacian. Let $A, B \subseteq V$ be nonempty, and let $\rho \ge 1$ be an integer such that every vertex of $A$ is at graph distance at least $\rho$ from every vertex of $B$ (in particular $A$ and $B$ are disjoint). Put $a = |A|/n$, $b = |B|/n$, and let $E_A$ ($E_B$) be the set of edges with both endpoints in $A$ (in $B$). Then

This is the main tool of the section: a large $\lambda_1$ forces many edges outside two far-apart sets, relative to their sizes. Theorem 2.5, Remark 2.3 and through them Theorems 2.6 and 2.7 are derived from it.

Formalization Note The paper takes $\rho$ to be the distance between $A$ and $B$; the Lean statement takes any integer $\rho \ge 1$ bounding all pairwise distances from below. Since the right-hand side decreases in $\rho$, the two versions are equivalent. $A$ and $B$ are required nonempty so that $a, b > 0$ (Lean's $1/0 = 0$ would otherwise change the statement). Distances are Mathlib's SimpleGraph.dist; all counts are cast to $\mathbb R$ before subtracting.