Trifurcation boundary-counting lemma (source code)

= Trifurcation boundary-counting lemma
{title2=$|\{v\in W:v\text{ trifurcates}\}|\leq|\partial^+W|$}

For a finite <graph vertex> <set> $W$ in a <locally finite graph>, let $\partial^+W$ be its exterior <graph neighbours>. The number of <trifurcation vertices in percolation> lying in $W$ is at most $|\partial^+W|$.

For each cluster meeting $W$, contract its <connected components of a graph> outside $W$ to terminal <graph vertices>, keeping only those adjacent to $W$. The resulting incidence <graph> is finite and connected. Each trifurcation <graph vertex> in $W$ separates at least three groups of terminals, because every infinite branch must leave the <finite set> $W$. Take a minimal subtree connecting all terminals. Each such trifurcation is unavoidable in that subtree and has <degree of a vertex> at least three. All leaves are terminals. The <tree> identity $\sum_v(\deg(v)-2)=-2$ bounds the number of these branching <graph vertices> by the number of leaves minus two, hence by the number of terminals. Different terminals, even across different clusters, can be assigned different exterior <graph neighbours>. Summing proves the bound. For square boxes in $\mathbb Z^2$, the boundary has order $n$ and the volume has order $n^2$.