Percolation at criticality

Mathematics generated by ChatGPT 5.6, prompted by Ahmed Bou-Rabee, with exposition and formalization support by Claude Opus 5.

Last updated 4 September 2026, 4:51 PM EDT

In Bernoulli bond percolation on \(\mathbb{Z}^d\), each edge is open with probability \(p\), independently of the other edges. The open clusters are the connected components formed by the open edges. In Bernoulli site percolation, each site is open with probability \(p\), independently of the other sites, and the open clusters are the connected components of the open sites. In either model, \(\theta(p)\) is the probability that the origin lies in an infinite open cluster.

Opening more edges or sites can only enlarge clusters, so \(\theta\) is nondecreasing. There is a critical probability \(p_c\) with \(\theta(p)=0\) below it and \(\theta(p)>0\) above it. The question is what happens at \(p_c\) itself.

In two dimensions, \(\theta(p_c)=0\) has been known for decades. For bond percolation the conclusion follows from two theorems: Harris proved that the percolation probability vanishes at \(p=1/2\), and Kesten proved that \(1/2\) is the critical probability. For site percolation it is Russo, who used Kesten's identification of the bond threshold to obtain continuity of \(\theta\) on all of \([0,1]\). Both proofs use methods specific to two dimensions.

In three or more dimensions, \(\theta(p_c)=0\) for bond percolation follows from Anthropic's machine-checked proof of Conjecture 3 of Kozma and Nitzan. Anthropic's proof settled dimensions three to ten, the only cases then open: \(\theta(p_c)=0\) for bond percolation was already known by the lace expansion for \(d\geq19\) by Hara and Slade and for \(d\geq11\) by Fitzner and van der Hofstad.

The proof presented here establishes \(\theta(p_c)=0\) for site percolation for every \(d\geq3\). It first proves inequality (1) below for every finite independent hyperedge model. Applying that inequality to the incidence representation of site percolation supplies the connection estimate used in the block-renormalization argument. The companion page treats the remaining conjectures and questions of the Kozma and Nitzan paper.

Simulations

Each picture has its own slider. Press pause and drag one to hold that lattice at a chosen \(p\).
Gray is the open structure, purple the open cluster of the center. The three-dimensional pictures draw that cluster alone. Each site and each edge carries a fixed random number and is open when it falls below \(p\), so the pictures grow as the sliders move and never rearrange.

One inequality for both models

Fisher observed that bond percolation on a graph is site percolation on the graph whose vertices are its edges, two of them adjacent when they share an endpoint. The converse fails: Gladkov and Zimin proved that bond percolation cannot simulate site percolation even approximately, already near a vertex of degree three. The bond inequality therefore does not automatically imply the site inequality.

Take a finite set of sites and a finite set of labels, attach to each label a set of sites, and declare each label open independently of the others. Two sites are connected when a chain of open labels joins them, consecutive labels in the chain sharing a site.

Attaching every label to exactly two sites makes the labels edges, and the structure is bond percolation. Giving each site a label of its own, attached to that site and to one extra point on each edge at it, makes a label open exactly when its site is open, and two distinct sites are connected in the structure exactly when they are connected in site percolation. This realizes both models as special cases.

The inequality proved here is that for a nonempty set \(A\) of sites and sites \(o\) and \(b\), \[ \mathbb{P}(o \leftrightarrow b,\ o \leftrightarrow A) \;\ge\; \mathbb{P}(o \leftrightarrow A)\,\min_{a \in A}\mathbb{P}(a \leftrightarrow b). \tag{1} \] Read from the right, it says that reaching \(A\) and then continuing to \(b\) from the least favorable point of \(A\) is no better than reaching \(b\) directly. What Kozma and Nitzan conjectured is the corresponding statement for a finite graph, which is the case of labels attached to two sites: \[ \mathbb{P}(o \leftrightarrow b) \;\ge\; \mathbb{P}(o \leftrightarrow A)\,\min_{a \in A}\mathbb{P}(a \leftrightarrow b). \tag{2} \] Inequality (1) generalizes (2) in two ways: a label may be attached to any number of sites, and the event \(\{o \leftrightarrow A\}\) is kept on the left. Discarding that event gives (2) in the bond case. The site representation gives the corresponding site inequality.

A union bound over \(A\) gives an error proportional to \(|A|\), and the sets \(A\) the lattice argument produces are the faces of large blocks, whose size grows without bound. Inequality (1) has no factor of \(|A|\).

Proof of the finite inequality

Failure of positive association under conditioning

Harris's inequality states that two increasing events under a product measure are positively associated. A more flexible form is the four functions theorem of Ahlswede and Daykin: if four nonnegative functions of a set satisfy \[ f_1(I)\,f_2(J) \;\le\; f_3(I \cup J)\,f_4(I \cap J) \] for every pair \(I,J\), then the same inequality holds for their sums over all sets.

Positive association need not survive conditioning on a disconnection event. On the path \(x - z - y\) with both edges open with probability \(1/2\), conditioned on \(x\) not reaching \(y\), the two edges are open with conditional probability \(1/3\) each and never together. Two increasing events have negative conditional covariance.

Conditional association of clusters

van den Berg, Häggström and Kahn proved conditional association for increasing functions of a cluster in ordinary bond percolation. The proof here extends this statement to finite independent hyperedge models. It proceeds by induction on the number of sites, exposing the labels meeting a fixed set \(Z\) and applying the four functions theorem to their subsets.

Write \(T(I)\) for the set of sites outside \(Z\) that the open exposed labels \(I\) reach. For a graph, a label meets \(Z\) in one endpoint and reaches one site outside it, so \(T(I)\) determines \(I\) and the two records carry the same information. For hyperedges, the set of reached sites need not determine the exposed labels: two labels attached to the same sites have the same trace, and so do a label reaching \(\{a,b\}\) and one reaching \(\{b,c\}\) once \(b\) has been exposed. In general, \[ T(I \cup J) = T(I) \cup T(J), \qquad T(I \cap J) \subseteq T(I) \cap T(J), \] and the second inclusion can be strict. Thus \(T\) preserves unions but not intersections. The induction is therefore indexed by the labels themselves. After deleting a cluster, the remaining distinct labels retain their product law; a record containing only reached sites would identify labels with the same trace.

Conditional covariance inequalities

The induction requires a comparison between conditioned covariances at two sites. Fix a site \(x\), a set \(Y\) its cluster must avoid, and an increasing function \(f\) of the labels of that cluster, and write \[ \kappa(u) \;=\; \operatorname{Cov}\bigl(f,\ \mathbf{1}\{u \leftrightarrow x\} \ \big|\ x \nleftrightarrow Y \bigr). \] The theorem is that for two further sites \(o\) and \(v\) and any finite list \(d_1,\dots,d_\ell\) of others, a certain alternating sum, in which the contribution of each \(d_j\) is subtracted off in turn, satisfies \[ \kappa^{[\ell]}(o) \;\ge\; \lambda\,\kappa^{[\ell]}(v), \] where \(\lambda\) is the probability that \(v\) reaches \(o\) given that \(v\) avoids everything named. With \(Y\) empty, no \(d_j\), and \(f\) the indicator that \(x\) reaches \(v\), this reduces to Harris's inequality. The successive subtraction terms permit induction on the intermediate sites.

The conditioned covariance inequality is proved by strong induction on \(\ell\) in three steps. The cluster of \(Y\) is exposed first, which turns the conditioned covariance into an average of unconditioned covariances over the structures that survive, and a telescoping argument reduces the covariance inequality to the nonnegativity of that average. The sites \(d_j\) are then removed one at a time by an exact identity, and the error each removal makes is itself a conditioned covariance with a shorter list, so the induction hypothesis applies to it. The remaining term is a comparison of \(o\) with \(v\) inside a single surviving structure; averaging gives the factor \(\lambda\). The last two steps use inequalities about two clusters, including a form of Harris's inequality valid at a stopping time of an exploration.

Induction on the intermediate set

Inequality (1) follows by induction on the size of \(A\). Order the sites of \(A\) by the conditional mean of \(f\), and in each configuration select the first one that the source reaches. Every configuration in which the source reaches \(A\) selects exactly one site, so these events form a partition. No error is summed over \(A\), and the estimate does not degrade as \(A\) grows.

From (1) to the lattice

The passage to \(\mathbb{Z}^d\) is a renormalization. Partition the lattice into blocks of a fixed size, declare a block occupied when a prescribed connection occurs inside it, and compare the occupied blocks with site percolation on a coarse lattice whose sites are the blocks. If the occupied blocks percolate on the coarse lattice, the open structure percolates on \(\mathbb{Z}^d\).

The required estimate states that a block already known to be occupied is joined to a neighboring block with conditional probability close to one, given everything examined so far.

Grimmett and Marstrand obtain the required neighboring-block estimate by sprinkling. They open further sites, working at \(p+\gamma\) rather than at \(p\), and conclude that percolation at \(p\) forces percolation in a slab of finite width at \(p+\gamma\), for every \(\gamma>0\). They state that they cannot take \(\gamma=0\), and at \(p=p_c\) this only gives a slab percolating at \(p_c+\gamma\).

Inequality (1) gives the neighboring-block estimate without sprinkling. Condition on the configuration in a shell around the block. That fixes the states on the shell and exposes a set \(A\) of open sites there, each of which reaches the neighboring block with conditional probability at least \(1-\delta\). Take \(o\) to be the source and \(b\) the target in the neighboring block: the two factors on the right of (1) are the probability that \(o\) reaches \(A\), which the previous step made close to one, and the minimum over \(A\), which is at least \(1-\delta\). Since these conditional bounds hold whatever the exploration has already revealed, the occupied blocks dominate independent site percolation at density \(1-\rho\) on the coarse lattice, and \(\rho\) is chosen small enough for that to percolate.

Every probability used in the construction concerns finitely many sites and is strictly above its threshold at \(p\), so the same finite list of inequalities still holds at some \(q<p\). Rerunning the construction at \(q\) gives \(\theta(q)>0\). Applied at \(p=p_c\) this contradicts the definition of \(p_c\), and the conclusion is \(\theta(p_c)=0\).

The Lean declaration assumes \(d\geq3\). For \(d=2\), the slab \(\mathbb{Z}^2 \times \{0,\dots,k\}^{d-2}\) is the full plane, so the slab construction gives no reduction. The planar site result is Russo's theorem.

Lean formalization

The finite hyperedge inequality, incidence representation of site percolation, block construction, parameter decrease, and criticality argument are formalized in Lean 4 with Mathlib. The hyperedge model, the connection events, the percolation probability and the critical parameter are definitions in the files; the critical parameter is proved to lie in \([0,1]\), so \(\theta(p_c)\) is defined and the conclusion needs no side condition.

The Lean development also proves the monotonicity and finite-event continuity estimates used in the block construction and in the decrease from \(p\) to \(q<p\).

Verified statements

Inequality (1) is proved in Lean for arbitrary finite independent hyperedge models. Lean also proves \(\theta(p_c)=0\) for site percolation on \(\mathbb Z^d\) for every \(d\geq3\), with no mathematical hypothesis other than \(3\leq d\). Every local Lean file used in this proof was compiled again from source. A separate check reported the public statement

∀ (d : ℕ), 3 ≤ d → thetaSite d (criticalProbSiteI d) = 0

After unfolding the definitions of thetaSite and the lattice graph, the conclusion is

∀ (d : ℕ), 3 ≤ d →
  (prodBernoulli fun _ => criticalProbSiteI d).real
    {ω | {y | 0 ∈ ω ∧
             (SimpleGraph.fromRel fun x y =>
                (SimpleGraph.hasse (Fin d → ℤ)).Adj x y ∧
                x ∈ ω ∧ y ∈ ω).Reachable 0 y}.Infinite}
  = 0

The companion theorem site_phase_transition proves \(0<p_c<1\), vanishing of \(\theta\) at and below \(p_c\), and positivity at some parameter below one.

Lean lists exactly the axioms propext, Classical.choice, and Quot.sound. The Lean files used in the proof contain no sorry, admit, native_decide, or added axiom.

Nothing here is assumed and nothing is conjectured. The result is unconditional.

The classical statement \(\theta(p_c)=0\) for two-dimensional site percolation is not part of this Lean declaration.

Source files and manuscript

site-percolation-criticality.pdf A rough mathematical manuscript covering the finite hyperedge inequality, block renormalization, and stability after decreasing the parameter. It has not yet received much human review.
Lean sources The directory contains 193 Lean modules, the public theorem, and every local Lean file needed to compile it. The modules build on Anthropic's Percolation library and Mathlib.