$\theta(p_c)=0$ for Bernoulli bond percolation on $\mathbb{Z}^d$ in all dimensions $d\ge 2$: a guide to the Lean formalization

Abstract — v1

This is a reader's guide to a Lean 4/Mathlib formalization proving that the percolation probability of nearest-neighbour Bernoulli bond percolation on $\mathbb{Z}^d$ vanishes at the critical point, $\theta(p_c)=0$, for every $d\ge2$; the cases $3\le d\le10$, in particular $\mathbb{Z}^3$, were open. The route is the reduction of Kozma and Nitzan (2024), who conjectured a family of “gluing” inequalities for percolation on arbitrary finite weighted graphs and proved that the weakest of them, their Conjecture 3, implies $\theta(p_c)=0$ on $\mathbb{Z}^d$ for all $d\ge2$. The development proves Conjecture 3 through a stronger additive gluing inequality—if $\mathbb{P}(a\leftrightarrow b)\ge1-t$ for every $a\in A$ then $\mathbb{P}(o\leftrightarrow b)\ge\mathbb{P}(o\leftrightarrow A)-t$—which is in turn derived from a new family of conditioned covariance inequalities for increasing functions of a single open cluster, indexed by finite lists of auxiliary vertices and proved by induction on the list; its first member is the Harris inequality. Kozma–Nitzan's Theorem 6 and every classical input are re-proved inside the library, so the final statement has no hypothesis other than $d\ge2$. The warrant for every claim is the Lean development, not this text.