# Critical percolation on every quasi-transitive graph

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Critical bond and site percolation on the cubic lattice](../../preprints/Critical-bond-and-site-percolation-on-the-cubic-lattice-September-24-2026/paper.pdf)
- [No percolation at criticality on quasi-transitive graphs](../../preprints/No-percolation-at-criticality-on-quasi-transitive-graphs-September-24-2026/paper.pdf)

## Scope

The critical-percolation question asks whether an infinite cluster can remain at the threshold. The formalized result proves that, at their respective critical probabilities, nearest-neighbor bond and site percolation on $\mathbb Z^3$ almost surely have no infinite cluster. Equivalently, almost surely every vertex belongs to a finite cluster in each model.

The formalization proves absence of an infinite cluster at criticality for Bernoulli bond percolation on every infinite connected locally finite quasi-transitive graph with critical probability $p_c<1$. At $p=p_c$, the probability that any infinite cluster exists is zero. The graph model permits bond multiplicities.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| No infinite critical clusters on $\mathbb Z^3$ | [CriticalZ3.lean](../ComparatorChallenges/CriticalZ3.lean) |
| No infinite cluster at the critical probability | [CriticalPercolation.lean](../ComparatorChallenges/CriticalPercolation.lean) |