Percolation at criticality

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, Russo proved 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.

For site percolation, the sufficiently high-dimensional result also goes back to Hara and Slade (1990): on p. 335 they explicitly state that their method applies to site percolation and yields the same results, including continuity at criticality. Heydenreich and Matzke (2020) later gave a detailed site-percolation lace-expansion proof; their Theorem 1.1 establishes the triangle condition and Section 1.3 states the consequence \(\theta(p_c)=0\). The proof presented here establishes \(\theta(p_c)=0\) for site percolation for every \(d\geq3\), including the previously unresolved low-dimensional cases. It extends the conditioned-covariance and first-contact strategy of Anthropic's bond proof to independent hyperedges, and 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

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. This rules out a general reduction by independent-bond gadgets. It does not establish how difficult it is to extend a particular proof; here the covariance and first-contact arguments are extended to independent hyperedges.

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.

This comparison is with the original conjecture. The full inequality (1), including the intersection on the left, already follows in the bond model from (GEN) in the preceding proof: take the increasing cluster function \(F(K)=\mathbf1_{\{b\in K\}}\), then bound its first-contact weighted sum by the minimum over \(A\). The contributions here are the extension of that machinery to hyperedges and the site-specific lattice construction.

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 sites outside \(Z\) reached by the exposed open labels \(I\). This record can lose label information even in an ordinary graph. For example, take \(Z=\{z_1,z_2\}\) and two edges \(e_1=\{z_1,u\}\), \(e_2=\{z_2,u\}\). Both singleton label sets have trace \(\{u\}\), although their intersection is empty. 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. For a fixed \(Z\) in ordinary bond percolation, however, different outside vertices are reached directly from \(Z\) through disjoint groups of independent boundary edges. Their reached/not-reached indicators have a product distribution, which is the property used in the original cluster-association proof. A hyperedge can reach several outside vertices at once, so this product structure can fail. The hyperedge induction applies the four functions theorem to the label sets themselves, with their unions, intersections, and product weights. Hyperedge labels remain distinct even when their incident vertex sets coincide, including after vertices are deleted.

Conditional covariance inequalities

The induction first takes label probabilities strictly between zero and one. Fix a site \(x\), a set \(Y\) with \(x\notin Y\), and an increasing function \(f\) of the cluster's vertex set. The disconnection event then has positive probability. Write \[ \kappa(u) \;=\; \operatorname{Cov}\bigl(f(C_x),\ \mathbf{1}\{u \leftrightarrow x\} \ \big|\ x \nleftrightarrow Y \bigr). \] Take distinct sites \(o,v\) outside \(Y\cup\{x\}\) and distinct auxiliary sites \(d_1,\dots,d_\ell\) outside \(Y\cup\{x,o,v\}\). For any function \(h\) of a site, define \[ c_j(u)=\mathbb P\bigl(d_j\leftrightarrow u\mid d_j\nleftrightarrow Y\cup\{x,d_1,\dots,d_{j-1}\}\bigr),\qquad h^{[0]}=h,\quad h^{[j]}(u)=h^{[j-1]}(u)-c_j(u)h^{[j-1]}(d_j). \] The theorem states \[ \kappa^{[\ell]}(o) \;\ge\; \lambda\,\kappa^{[\ell]}(v), \] where \(\lambda=\mathbb P(v\leftrightarrow o\mid v\nleftrightarrow Y\cup\{x,d_1,\dots,d_\ell\})\). With no auxiliary sites, the theorem compares the two nonnegative conditioned covariances. The successive subtraction terms permit induction on the intermediate sites.

The conditioned covariance inequality is proved by strong induction on \(\ell\). Exposing the cluster of \(Y\) leaves independent models on the surviving structures. The law of total covariance also contributes the covariance of conditional means; exposure alone does not identify the original covariance with an average of the remaining covariances. A two-block resampling and telescoping argument handles this contribution. 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 averaged expressions; the four functions theorem controls their products and supplies the required global coefficient. 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 unconditional mean of the increasing cluster function, 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. After clearing conditioning denominators, continuity extends the final finite inequality to label probabilities zero and one.

From (1) to the lattice

Start from \(0<p<1\) and assume \(\theta(p)>0\). Uniqueness and large-box estimates supply the finite connection events used below. The passage to \(\mathbb{Z}^d\) is a renormalization. Arrange 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) supplies the gluing step without sprinkling. The shell estimates give a high probability of reaching an open contact whose conditional probability of continuing to a finite target set is close to one. After fixing a shell pattern, retain the contacts \(A\) with that reliability. Earlier observations fix sites open or closed, and the remaining coordinates have a product law. To apply the single-target inequality, adjoin an auxiliary vertex \(b\), fixed open and adjacent to the target set. Connection to \(b\) now means connection to some open site of that set. The source is also fixed open. Apply (1) under this conditional product law, then average over shell patterns.

The exploration maintains these bounds after every permitted history. Each pending destination has one designated predecessor, and stopping rules protect the unread sites needed for its next move. Successful moves record actual open paths. A failed examination can also disable nearby moves, so the comparison includes this bounded local damage: it retains vertices of a high-density independent field only when their required nearby trials succeed. Disjoint \(3\times3\) blocks give a supercritical independent comparison when the failure probability is sufficiently small.

Fix the geometry and the finite list of prototype events used in these estimates. Their strict probability bounds persist at one common \(q<p\) by finite-event continuity. Translation invariance supplies the same estimates at every location, and the exploration invariants apply them after every permitted history. The construction at \(q\) gives \(\theta(q)>0\). Assuming \(\theta(p_c)>0\) and applying this at \(p=p_c\) contradicts the definition of \(p_c\), proving \(\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\).

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

∀ (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

Source files and verification