on the continuity of the percolation phase transition

Overview

A pinned 28 August 2026 commit in anthropics/formal-math contains a Lean 4 proof of the following long-standing assertion for nearest-neighbour Bernoulli bond percolation:

$$\theta (p_c)=0(d\ge 2).$$

Here $\theta (p)$ is the probability that the origin belongs to an infinite open cluster and $p_c$ is the critical parameter. The difficult cases were $3\le d\le 10$. The formal route has a crisp logical spine: a new covariance inequality on finite weighted graphs yields additive gluing; that settles a finite-graph conjecture of Kozma and Nitzan; their reduction then rules out percolation at $p_c$ on ${\mathbb{Z}}^d$. This post explains that spine rather than reproducing the development file by file.

Status and trust boundary

This is a report on an unrefereed formal artifact, not an independent referee report. Lean checks a derivation of formal statements; it does not decide whether the definitions in the statement file are the intended lattice, product measure, cluster, and critical probability. The release’s statement audit and independent-kernel comparator are therefore central evidence, but the semantic audit remains a human task. All claims below concern the pinned release cited as (Leder, 2026), not the current state of any branch.

🏷️ Critical Percolation on the Lattice

For $p\in [0,1]$, declare each nearest-neighbour edge of ${\mathbb{Z}}^d$ open independently with probability $p$. Write $C(x)$ for the open cluster of $x$, and

$$\theta (p):={\mathbb{P}}_p(|C(0)|=\infty ),p_c:=\inf (\{p\in [0,1]:\theta (p)>0\}\cup \{1\}).$$

The final singleton is the formal convention that keeps the infimum meaningful should $\theta$ vanish identically. Monotonicity makes $\theta$ vanish below $p_c$. The question is whether an infinite cluster can appear at the threshold. For $d=1$, it can: $p_c=1$ and $\theta (1)=1$. The theorem concerns exactly the nontrivial dimensions.

Critical continuity

For nearest-neighbour Bernoulli bond percolation on ${\mathbb{Z}}^d$, $d\ge 2$,

$$\theta (p_c)=0.$$

In the cited release this is the theorem

Percolation.Continuity.CSH.percolationContinuity_allDimensions
  (d : ℕ) (hd : 2 ≤ d) : PercolationContinuity d

with PercolationContinuity d defined as theta (zdGraph d) 0 (criticalProbI d) = 0.

Sparse, near-critical, and highly connected finite windows. The image is only a visual mnemonic: it does not depict an infinite-volume proof or identify the numerical value of $p_c$.

For independent percolation, this equality is equivalent to continuity of $p\mapsto \theta (p)$ on $[0,1]$: below $p_c$ the function is zero, and it is classically continuous on $(p_c,1]$ (van den Berg & Keane, 1984; Grimmett, 1999). Thus the only possible jump lies at $p_c$.

🏷️ The Earlier Boundary of Knowledge

The two-dimensional case follows from planar methods. Harris proved critical nonpercolation, and Kesten identified $p_c({\mathbb{Z}}^2)=1/2$ (Harris, 1960; Kesten, 1980). In high dimensions, the triangle condition implies the same conclusion; the lace expansion established that condition first in sufficiently high dimension and then for $d\ge 11$ (Aizenman & Newman, 1984; Hara & Slade, 1990; Fitzner & van der Hofstad, 2017).

The middle dimensions remained open. Standard sharpness theorems give exponential decay for $p<p_c$, but do not decide what happens at $p=p_c$ (Menshikov, 1986; Aizenman & Barsky, 1987; Duminil-Copin & Tassion, 2016). Duminil-Copin’s ICM survey records the problem explicitly (Duminil-Copin, 2018).

The obstruction was a composition problem: at a fixed parameter, how can highly likely connections through an arbitrarily large collection of relay vertices be glued without paying an error once per relay?

🏷️ The Finite-Graph Bottleneck

Kozma and Nitzan isolate that question for finite graphs with independent edge weights $w_e\in [0,1]$. If $u\leftrightarrow A$ denotes connection from $u$ to some member of $A$, their Conjecture 3 asks for a modulus $\delta (\epsilon )>0$, independent of $|A|$, such that

$$\mathbb{P}(o\leftrightarrow A)>1-\delta \text{and}\mathbb{P}(a\leftrightarrow b)>1-\delta (a\in A)$$

imply $\mathbb{P}(o\leftrightarrow b)>1-\epsilon$. A union bound works for a fixed $A$, but loses a factor proportional to $|A|$; the conjecture says that loss is illusory.

Kozma–Nitzan reduction

Conjecture 3 implies $\theta (p_c)=0$ for bond percolation on ${\mathbb{Z}}^d$, in every dimension $d\ge 2$ (Kozma & Nitzan, 2024).

Their renormalisation constructs near-certain box-to-box connections at one fixed parameter. Uniform gluing turns them into percolation in a thick two-dimensional slab. At $p=p_c$, this contradicts the two-dimensional Harris–Kesten input when $d=2$, or critical half-space nonpercolation when $d\ge 3$ (Barsky, Grimmett & Newman, 1991). Thus one finite-graph statement closes the lattice problem.

flowchart TB
    subgraph finite[Finite weighted graphs]
        CSH["Conditioned slack hierarchy<br/>worlds, telescoping, and decoy induction"]
        SUR["Surplus transfer<br/>first-relay decomposition"]
        GLUE["Uniform additive gluing<br/>Conjecture 3, δ(ε) = ε/2"]
        CSH --> SUR --> GLUE
    end

    subgraph lattice[Lattice reduction in d ≥ 3]
        POS["Assume θ(p) > 0"]
        BOX["Near-certain connections<br/>between large boxes"]
        CONTRACT["Explore and contract<br/>to a finite weighted graph"]
        GOOD["Conditional good-box field<br/>on a coarse ℤ²"]
        PEIERLS["Peierls estimate<br/>percolation in a thick slab"]
        HALF["Contradicts critical<br/>half-space nonpercolation"]
        POS --> BOX --> CONTRACT --> GOOD --> PEIERLS --> HALF
    end

    GLUE --> CONTRACT
    HALF --> RESULT["θ(p_c) = 0"]
    PLANAR["d = 2: Harris–Kesten"] --> RESULT

The finite-graph branch is the new argument. The lattice branch shows precisely where gluing is used: contraction presents the many possible box contacts as relays in one finite weighted graph, and uniformity prevents the error from accumulating before the Peierls step.

🏷️ The Conditioned Slack Hierarchy

The new finite-graph ingredient is the conditioned slack hierarchy. It does not estimate $\theta$ directly. Instead, it controls what remains of a positive covariance after relays are removed one at a time.

Fix an owner $x$, an avoided set $Y$, distinct decoys $Z=(z_1,\dots ,z_{\ell })$, and observers $o,v$. Work under

$$\nu =\mathbb{P}(\cdot \mid x\nleftrightarrow Y).$$

For an increasing function $f$ of the owner’s open edge cluster, let

$${\kappa }_f(u):={\mathrm{Cov}}_{\nu }\left(f({\mathcal{E}}_x),1\{u\in C_x\}\right).$$

Writing $Y_j=\{x\}\cup Y\cup \{z_1,\dots ,z_{j-1}\}$, each decoy subtracts the part of a function $\phi$ explained by its cluster:

$${\mathrm{sl}}^0[\phi ]=\phi ,{\mathrm{sl}}^j[\phi ](u)={\mathrm{sl}}^{j-1}[\phi ](u)-c_j(u){\mathrm{sl}}^{j-1}[\phi ](z_j),$$

where $c_j(u)=\mathbb{P}(u\in C_{z_j}\mid z_j\nleftrightarrow Y_j)$. The final transfer uses

$$\tau =\mathbb{P}\left(o\in C_v\mid v\nleftrightarrow Y_{\ell +1}\right).$$

Conditioned slack hierarchy

For every such datum and every increasing $f$,

$${\mathrm{sl}}^{\ell }[{\kappa }_f](o)-\tau {\mathrm{sl}}^{\ell }[{\kappa }_f](v)\ge 0.$$

The formal theorem is Percolation.Continuity.CSH.cshHolds. Its implementation uses a denominator-free polynomial form of the conditional covariances.

At level zero, the statement refines Harris positive association: the covariance between an increasing cluster functional and the event that $x$ reaches $o$ dominates a conditional multiple of the corresponding covariance for $v$. Higher levels preserve that comparison after each decoy’s already-accounted-for contribution has been removed.

Why the price is conditional

On the path $o-x-v$ with both edge weights $1/2$, let $f=1\{v\in C_x\}$. Then ${\kappa }_f(o)=0$ and ${\kappa }_f(v)=1/4$. An unconditioned transfer probability would give a false positive lower bound. But $\mathbb{P}(o\in C_v\mid v\nleftrightarrow x)=0$, so the hierarchy holds at equality. The conditioning is structural, not cosmetic.

🏷️ Proof Architecture

The following account follows the release’s reader-facing proof sketch (Leder, 2026). Its useful invariant is that every term created by deleting a decoy must be another instance of the hierarchy, with the same later constants. The proof is organized to preserve that invariant.

Worlds and telescoping. Under $\nu$, first explore the cluster $C_Y$ of the avoided set and write $U=V\setminus C_Y$. Conditional on this explored cluster, the unexamined edges of $U$ are fresh independent percolation. Let ${\kappa }_f^U$ be the covariance computed inside this random world, and average its margin:

$$\mathcal{W}[f]:=\mathbb{E}[\mathrm{Marg}[{\kappa }_f^U]].$$

The law of total covariance does not give the hierarchy immediately, because conditioning on the world leaves an extra covariance term. The key identity rewrites that term as the same margin for a new increasing functional $\mathcal{A}f$:

$$\mathrm{Marg}[{\kappa }_f]=\mathcal{W}[f]+\mathrm{Marg}[{\kappa }_{\mathcal{A}f}].$$

Here $\mathcal{A}$ is the two-block Gibbs update that alternately resamples $C_Y$ and the owner’s cluster. Repeating the identity gives a sum of world parts. Since the update has a fixed positive chance to regenerate, ${\mathcal{A}}^{n}f$ tends to a constant, whose covariance vanishes. Thus it is enough to prove $\mathcal{W}[f]\ge 0$ for every increasing $f$.

Unfolding the decoys. Put $X_i=\{x,z_1,\dots ,z_i\}$. The elementary but decisive disjoint decomposition is

$$\{u\leftrightarrow X_i\}=\{u\leftrightarrow X_{i-1}\}\bigsqcup (\{u\in C_{z_i}\}\cap \{z_i\nleftrightarrow X_{i-1}\}).$$

Iterating it alongside the recursion for ${\mathrm{sl}}^i$ rewrites the world part as a horizontal term plus one term for each decoy. After taking covariance with $f$, the $j$th decoy term is a nonnegative scalar times the margin of a lower-level datum: the owner is now $z_j$, the avoided set is $Y_j$, and the remaining decoys are $z_{j+1},\dots ,z_{\ell }$. Its functional is an explicitly constructed increasing excess functional. The induction hypothesis therefore controls every decoy term. This is the reason for the apparently broad statement of the theorem: restricting it to $Y=\varnothing$ or to indicator functions would not survive even one peel.

The horizontal term. What remains compares two observers looking toward the marker set $X=\{x,z_1,\dots ,z_{\ell }\}$. In a fixed world, Harris association and the conditional negative correlation of van den Berg–Häggström–Kahn give the set four-point transfer

$$\mathrm{Cov}(f({\mathcal{E}}_x),1\{o\leftrightarrow X\})\ge \mathbb{P}(o\in C_v\mid v\nleftrightarrow X)\mathrm{Cov}(f({\mathcal{E}}_x),1\{v\leftrightarrow X\}).$$

The remaining issue is that a world has its own transfer price $\tau (U)$, while the hierarchy uses the global price $\tau$. A two-source inequality shows that this discrepancy has the favorable sign after averaging over worlds. Its proof explores two source clusters and applies Gladkov’s decision-tree Harris inequality to the covariance term and the Ahlswede–Daykin four-functions theorem to glue the two explorations (van den Berg, Häggström & Kahn, 2006; Gladkov, 2024; Ahlswede & Daykin, 1978). Hence the horizontal term is nonnegative, then $\mathcal{W}[f]\ge 0$, and telescoping closes the induction.

The closure mechanism

The proof is not an iteration of ordinary FKG. The new content is that every correction created by peeling is re-expressed as a lower-level conditioned covariance statement, and that the global observer price is stable on average under the random-world decomposition.

🏷️ From Slack to Gluing

The hierarchy concerns one owner and two observers. Gluing requires an observer and a whole relay set. The bridge is a surplus that records how much a cluster is worth beyond the first relay it meets.

Fix an increasing $F\ge 0$ and order the relays $R$ so that $m_a:=\mathbb{E}F(C_a)$ is nondecreasing. On the event $\{u\leftrightarrow R\}$, let $\iota (u)$ be the first relay in $C_u$, and let $P_a^u=\{\iota (u)=a\}$. Define

$${\mathrm{Sur}}_u(R):=\mathbb{E}[F(C_u);u\leftrightarrow R]-\sum _{a\in R}\mathbb{P}(P_a^u)m_a.$$

For one relay, ${\mathrm{Sur}}_u(\{x\})$ is exactly the covariance in the hierarchy. For many relays, the needed comparison is the surplus-transfer inequality

$$\mathbb{P}(v\nleftrightarrow R){\mathrm{Sur}}_o(R)\ge \mathbb{P}(o\leftrightarrow v,v\nleftrightarrow R){\mathrm{Sur}}_v(R).$$

To prove it, remove the top relay $a_s$ from $R$. On the event that $a_s$ misses the other relays, the events that $u$ reaches $R\setminus \{a_s\}$ and that $u$ belongs to $C_{a_s}$ are disjoint. The first part is the induction hypothesis on the relay set; the second is a hierarchy covariance for $a_s$. Crucially, after $a_s$ is removed it becomes the first decoy, so its conditioned constants are exactly those required for the lower-level hierarchy. A second hierarchy application controls the resulting correction. This is the finite-graph version of the closure mechanism above: relays do not disappear during the induction; they become decoys.

The surplus-transfer inequality implies that the surplus at $o$ is nonnegative. Equivalently, the value of $C_o$ on reaching $A$ is at least the value of its first relay:

$$\mathbb{E}[F(C_o);o\leftrightarrow A]\ge \sum _{a\in A}\mathbb{P}(P_a^o)\mathbb{E}F(C_a).$$

Now set $F(C)=1\{b\in C\}$. Then $m_a=\mathbb{P}(a\leftrightarrow b)$, so the failure of $o$ to reach $b$ localizes at its first relay. If every relay fails to reach $b$ with probability at most $t$, the first-relay bound gives the additive gluing inequality

$$\mathbb{P}(o\leftrightarrow b)\ge \mathbb{P}(o\leftrightarrow A)-t.$$

The important point is the absence of $|A|$ on the right. Taking $t=\epsilon /2$ proves Conjecture 3 with the explicit modulus $\delta (\epsilon )=\epsilon /2$. The release extends the result from edge weights in $(0,1)$ to $[0,1]$ by polynomial closure.

The stronger multiplicative Conjecture 1 is not proved in general. The development records it for three relays only; its remaining variants and the associated Kozma–Nitzan questions are still open.

🏷️ The Lattice Conclusion

For $d=2$, the conclusion is the classical Harris–Kesten route: Harris proves critical nonpercolation at $p=1/2$, and Kesten proves that this parameter is $p_c({\mathbb{Z}}^2)$.

For $d\ge 3$, the reduction is a contradiction argument at a fixed parameter. Assume $\theta (p)>0$. Large boxes then connect to suitable far-away targets with probability arbitrarily close to one. The target lemma converts one such high-probability connection into another: explore the cluster from an inner box to a shell, use the relevant uniqueness input to funnel many possible contact points into one macroscopic cluster, contract the explored configuration to a finite weighted graph, and apply near-one gluing to the contracted target. The paper uses a local-uniqueness input at this point; the release instead re-proves uniqueness of the infinite cluster, which it records as sufficient. The role of Conjecture 3 is exactly to prevent the error from accumulating over the many possible contact points.

This lemma is iterated on a coarse copy of ${\mathbb{Z}}^2$ embedded in

$$L_r={\mathbb{Z}}^2\times [-5r,5r{]}^{d-2}\subset {\mathbb{Z}}^d.$$

Each explored macroscopic site is good with conditional probability greater than $1-\epsilon$, even after the earlier exploration has been revealed. The formal development does not leave the final stochastic-domination step implicit: for $\epsilon \le 2^{-32}$ it proves an explicit Peierls contour estimate, producing an infinite cluster in $L_r$ and hence in the slab $S_{10r}$.

Apply this at $p=p_c$. A slab lies in a half-space, while the Barsky–Grimmett–Newman half-space theorem gives ${\theta }_{\mathbb{H}}(p_c)=0$ (Barsky, Grimmett & Newman, 1991). The slab cluster is impossible, so the assumption $\theta (p_c)>0$ was false. Together with the $d=2$ case, this proves the displayed all-dimensions theorem.

🏷️ What the Formal Artifact Checks

The cited release is arranged as a statement file, a proved twin, a comparator, and an audit record. Challenge.lean defines the lattice graph, product bond measure, open cluster, $\theta$, $p_c$, and PercolationContinuity; Solution.lean proves a definitionally identical statement using the library; the comparator asks Lean and the independent nanoda kernel to replay the compared proof.

Recorded mechanical evidence

The release audit records a successful full lake build, axiom reports for the main theorems containing only propext, Classical.choice, and Quot.sound, two deliberate sorry placeholders in the challenge statement file, no axiom declarations, and successful replay by nanoda. These checks establish the stated formal derivations conditional on the Lean kernel and the audited statement surface; they do not establish that the statement surface has the intended informal meaning.

A formal proof can be compelling evidence for a major theorem without turning provenance into peer review. A serious audit begins with the release’s AUDIT.md, then unfolds the definitions in Challenge.lean, and finally traces the dependency path from the hierarchy through additive gluing to the lattice theorem.

🏷️ Scope and Open Directions

The claimed theorem covers nearest-neighbour Bernoulli bond percolation on ${\mathbb{Z}}^d$. It does not automatically settle site percolation, other lattices, long-range models, or dependent percolation. Nor does it provide critical exponents, a quantitative bound on $\theta (p)$ as $p\downarrow p_c$, or a critical cluster-tail estimate.

The reusable mathematical contribution, if independently validated, is narrower and more portable than the headline: a conditioned covariance hierarchy that prevents relay-by-relay loss in a finite-graph gluing argument. Whether it has consequences beyond the Kozma–Nitzan reduction is a natural next question.

Links

• on more than two thirds of the zeta zeros on the critical line — another post about an AI-produced Lean artifact, where the distinction between kernel checking, statement auditing, and mathematical acceptance is equally important.
• on high-dimensional cover times and random interlacements — random interlacements provide a neighbouring high-dimensional probability model whose vacant set raises related percolation questions.
• on self-avoiding walks and the honeycomb connective constant — the planar tools behind the two-dimensional endpoint belong to the same broad percolation tradition as the methods discussed there.

🐻  Ahlswede, R. & Daykin, D.E. 1978. An inequality for the weights of two families of sets, their unions and intersections. Zeitschrift für Wahrscheinlichkeitstheorie und Verwandte Gebiete 43(3), 183–185.

🐻  Aizenman, M. & Newman, C.M. 1984. Tree graph inequalities and critical behavior in percolation models. Journal of Statistical Physics 36(1–2), 107–143.

🐻  Aizenman, M. & Barsky, D.J. 1987. Sharpness of the phase transition in percolation models. Communications in Mathematical Physics 108(3), 489–526.

🐻  Barsky, D.J., Grimmett, G.R. & Newman, C.M. 1991. Percolation in half-spaces: equality of critical densities and continuity of the percolation probability. Probability Theory and Related Fields 90(1), 111–148.

🐻  van den Berg, J. & Keane, M. 1984. On the continuity of the percolation probability function. In Conference in modern analysis and probability (New Haven, Conn., 1982), pp. 61–65. Contemporary Mathematics, Providence, RI: American Mathematical Society.

🐻  van den Berg, J., Häggström, O. & Kahn, J. 2006. Some conditional correlation inequalities for percolation and related processes. Random Structures & Algorithms 29(4), 417–435.

🐻  Duminil-Copin, H. 2018. Sixty years of percolation. In Proceedings of the International Congress of Mathematicians—Rio de Janeiro 2018. Vol. IV. Invited lectures, pp. 2829–2856. , Hackensack, NJ: World Scientific.

🐻  Duminil-Copin, H. & Tassion, V. 2016. A new proof of the sharpness of the phase transition for Bernoulli percolation on \mathbbZ^d. L’Enseignement Mathématique 62(1–2), 199–206.

🐻  Fitzner, R. & van der Hofstad, R. 2017. Mean-field behavior for nearest-neighbor percolation in d > 10. Electronic Journal of Probability 22(43), 1–65.

🐻  Gladkov, N. 2024. Percolation Inequalities and Decision Trees.

🐻  Grimmett, G. 1999. Percolation 2nd ed., Berlin: Springer-Verlag,p.

🐻  Hara, T. & Slade, G. 1990. Mean-field critical behaviour for percolation in high dimensions. Communications in Mathematical Physics 128(2), 333–391.

🐻  Harris, T.E. 1960. A lower bound for the critical probability in a certain percolation process. Proceedings of the Cambridge Philosophical Society 56, 13–20.

🐻  Kesten, H. 1980. The critical probability of bond percolation on the square lattice equals \frac12. Communications in Mathematical Physics 74, 41–59.

🐻  Kozma, G. & Nitzan, S. 2024. A reduction of the θ(p_c)=0 problem to a conjectured inequality.

🐻  Leder, J. 2026. θ(p_c) = 0 for Bernoulli bond percolation on \mathbbZ^d in all dimensions d \ge 2, in Lean 4 / Mathlib.

🐻  Menshikov, M.V. 1986. Coincidence of critical points in percolation problems. Doklady Akademii Nauk SSSR 288(6), 1308–1311.