Percolation uniqueness on an amenable quasi-transitive graph (source code)

= Percolation uniqueness on an amenable quasi-transitive graph

For a connected infinite <locally finite graph> that is also an <amenable graph> and a <quasi-transitive graph>, an invariant independent <site percolation> law with every orbit parameter strictly between $0$ and $1$ has either no <infinite percolation cluster> or exactly one, almost surely. Invariance and independence give a zero–one law. The <finite-energy property of Bernoulli percolation> excludes a fixed finite number greater than one by opening a finite joining region. Infinitely many clusters would create an <encounter box in percolation> with positive probability; translated disjoint boxes then have positive density, contradicting the boundary count in a <Følner sequence>. The finite-energy hypothesis matters if some orbit parameters are $0$ or $1$.