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

Provenance and review status. The Lean sources of this development—definitions, statements and proofs, together with the statement file Challenge.lean, its proved twin Solution.lean and the metadata—were written by an AI system (Anthropic’s Claude models) working under my direction; no human wrote or edited the Lean code, and the first drafts of this guide were produced in the same way. Correctness rests on mechanical checking: the Lean 4 kernel accepts every file with no sorry outside the two deliberate placeholders of Challenge.lean, no added axioms and no unsafe code, and the main theorems depend only on the standard axioms propext, Classical.choice, Quot.sound; the compared theorems are additionally replayed in the independent nanoda kernel by the Lean comparator (see AUDIT.md). Neither the development nor this guide has yet been refereed by human mathematicians or by anyone independent of me; the only review so far was carried out by AI systems. Mechanical checking does not cover whether the formal statements express the intended mathematics: readers should satisfy themselves that Challenge.lean states the theorem of Section 2 (box “Statements to audit”).

1 Introduction

1.1 The model and the question

Bernoulli bond percolation on $\mathbb{Z}^d$, introduced by Broadbent and Hammersley [9], declares every nearest-neighbour edge of $\mathbb{Z}^d$ open with probability $p\in[0,1]$, independently; $\mathbb{P}_p$ is the product measure and $C_0$ the set of vertices joined to the origin by open paths. The percolation probability is $\theta(p):=\mathbb{P}_p(|C_0|=\infty)$ and the critical probability $p_{\mathrm{c}}=p_{\mathrm{c}}(\mathbb{Z}^d):=\inf\{p:\theta(p)>0\}$ satisfies $0<p_{\mathrm{c}}<1$ for $d\ge2$ [22 Theorem (1.10)]. Since $\theta$ is non-decreasing, vanishes on $[0,p_{\mathrm{c}})$, and is continuous on $(p_{\mathrm{c}},1]$ [36], [22 Theorem (8.8)]—the last fact resting on the uniqueness of the infinite cluster [2, 10]—$\theta$ is continuous on $[0,1]$ if and only if

i.e. if and only if there is almost surely no infinite cluster at the critical point [22 §8.3]. That (1) holds for every $d\ge2$ is conjectured—“open since at least the 80s” [29 p. 1]—and recorded as open in [22 pp. 14, 202–203], [13 Conjecture 1]. This guide describes a formal proof of (1) for all $d\ge2$.

1.2 What was known

Two dimensions. Harris [26] proved $\theta(\tfrac12)=0$ on $\mathbb{Z}^2$ and Kesten [27] proved $p_{\mathrm{c}}(\mathbb{Z}^2)=\tfrac12$, building on Russo [31] and Seymour–Welsh [32]; together these give (1) for $d=2$. Harris’ paper also contains the correlation inequality that bears his name (in general form Fortuin–Kasteleyn–Ginibre [18]), which with the van den Berg–Kesten inequality [37] is the basic tool of the subject. Sharpness—exponential decay of the cluster radius for $p<p_{\mathrm{c}}$, due to Menshikov [30] and Aizenman–Barsky [3], with short proofs by Duminil-Copin–Tassion [15, 16]—does not decide (1). High dimensions. Aizenman–Newman [5] introduced the triangle condition and Barsky–Aizenman [6] showed that it implies (1); Hara–Slade [24] verified it by the lace expansion in high dimension ($d\ge19$ [25 Thm. 2.7]), and Fitzner–van der Hofstad [17] reached $d\ge11$. Thus (1) was known for $d=2$ and $d\ge11$ and open for $3\le d\le10$. Restricted geometries. Barsky–Grimmett–Newman [7] proved by a block argument at fixed $p$ that a half-space does not percolate at its critical point, which by Grimmett–Marstrand [23] equals $p_{\mathrm{c}}(\mathbb{Z}^d)$, so $\theta_{\mathbb{H}}(p_{\mathrm{c}})=0$ [22 Thms. (7.2), (7.35)]; Duminil-Copin–Sidoravicius–Tassion [14] proved that slabs $\mathbb{Z}^2\times\{0,\dots,k\}$ do not percolate at their own critical points. As Kozma and Nitzan stress [29 §1], in the block arguments the step from a finite-size criterion back to percolation needs an extra feature (the half-space, or an increase of $p$); that step in $\mathbb{Z}^d$ itself, at fixed $p$, was missing.

1.3 The Kozma–Nitzan reduction

Kozma and Nitzan [29] proposed to supply the missing step by an inequality for percolation on finite graphs with arbitrary edge probabilities. For such a graph, vertices $o,b$ and a vertex set $A$, with $\{o\leftrightarrow A\}$ the event that $o$ is joined to some vertex of $A$, their Conjecture 1 [29 p. 3] is

of which they write: “We were not able to prove or disprove this conjecture. Our belief that it holds is based on some (admittedly restricted) numerical evidence and on some simple cases where we were able to prove it.” They prove a stronger “pre-FKG” form for $|A|=2$, for several configurations with $|A|=3$, and for $o$ close to $A$ [29 Theorems 1–5]; they formulate variants (Conjecture 2; Conjecture 4 for monotone functions of the cluster [29 p. 32]); and they isolate the weakest statement of the family, Conjecture 3 [29 p. 15]: for every $\varepsilon>0$ there is $\delta>0$ such that, for any finite weighted graph and any $A,o,b$, $\mathbb{P}(o\leftrightarrow A)>1-\delta$ and $\mathbb{P}(a\leftrightarrow b)>1-\delta$ for all $a\in A$ imply $\mathbb{P}(o\leftrightarrow b)>1-\varepsilon$. The content is that $\delta$ does not depend on $|A|$ (for bounded $|A|$ the union bound gives $\delta=\varepsilon/(|A|+1)$). Their main theorem is the reduction [29 Theorem 6]: if Conjecture 3 holds, then $\theta(p_{\mathrm{c}})=0$ on $\mathbb{Z}^d$ for every $d\ge2$, proved by a one-step renormalisation at fixed $p$ (Section 3.1). The paper is an arXiv preprint (v1, January 2024); Gladkov [19 §1] reports the conjectured inequality as open, and we are not aware of a proof in print of any of Conjectures 1–4 beyond the cases above.

1.4 What the formalization adds, and what it does not

The development proves Conjecture 3 (Corollary 2.3) through the additive gluing inequality (Theorem 2.2): if $\mathbb{P}(a\leftrightarrow b)\ge1-t$ for all $a\in A$ then $\mathbb{P}(o\leftrightarrow b)\ge\mathbb{P}(o\leftrightarrow A)-t$—weaker than (2), since $\mathbb{P}(o\leftrightarrow A)(1-t)\ge\mathbb{P}(o\leftrightarrow A)-t$, and stronger than Conjecture 3 (take $t=\delta=\varepsilon/2$). Additive gluing is derived from a family of conditioned covariance inequalities for increasing functions of a single open cluster, the conditioned slack hierarchy (Theorem 2.5), the one new object; its level-zero, unconditioned member is the Harris inequality. Kozma–Nitzan’s Theorem 6 with everything it invokes, and every correlation inequality used, are re-proved inside the library, so the formal statement carries no hypothesis other than $2\le d$. Our contribution is the finite-graph inequality; the reduction, and the insight that an inequality uniform in $|A|$ is what the renormalisation approach requires, are Kozma and Nitzan’s.

Not claimed. Conjectures 1 (2), 2 and 4 are neither proved nor stated in the release (the three-relay case of (2) is proved, Remark 3.2). Nothing is proved about the rate at which $\theta(p)\to0$, critical exponents or the value of $p_{\mathrm{c}}$; nothing new about site percolation, other lattices, or slabs (the slab theorem of [14] is formalised as a literature input only). Continuity of $\theta$ on $[0,1]$, classically equivalent to (1), is not part of the formal statement. No lace expansion, triangle condition or numerics are used.

1.5 How to read this guide, and what to verify

The repository¹ is laid out as a Palomar submission: a statement file Challenge.lean importing only Mathlib, which defines the lattice, the measure, $\theta$, $p_{\mathrm{c}}$ and the proposition PercolationContinuity d and states two theorems with placeholder proofs; its twin Solution.lean, proving the same theorems from the library Percolation; the comparator configuration comparator.json; and AUDIT.md, which lists what was mechanically checked and how to reproduce it. To decide whether the theorem is proved: read Challenge.lean (Section 2, box), run the build and comparator as in README.md, inspect the axiom listing. To see how: read Section 3 with the docstrings it names and Section 4. Where this text and a Lean statement differ, the Lean statement is what has been proved.

2 Main results

Notation. A finite weighted graph is a finite set $V$ with a weight $w_e\in[0,1]$ on every unordered pair $e$ of distinct vertices (weight $0$ = absent edge); $\mathbb{P}=\mathbb{P}_w$ makes each pair $e$ open with probability $w_e$ independently (in Lean, $V=\mathrm{Fin}\,n$, prodBernoulli w). $C_u$ is the vertex set of the open cluster of $u$, $\mathcal{C}_u$ the set of open pairs inside it (the edge cluster); $\{u\leftrightarrow v\}=\{v\in C_u\}$ (openConn u v), $\{u\leftrightarrow A\}=\bigcup_{a\in A}\{u\leftrightarrow a\}$; “increasing” means monotone for inclusion, and increasing functions of the edge cluster $\mathcal{C}_x$ include those of the vertex cluster $C_x=\{x\}\cup V(\mathcal{C}_x)$; $\mathbb{E}[\xi;B]:=\mathbb{E}[\xi\mathbf{1}_B]$ for an event $B$.

Theorem 2.1 ($\theta(p_{\mathrm{c}})=0$ in all dimensions). For every integer $d\ge2$, nearest-neighbour Bernoulli bond percolation on $\mathbb{Z}^d$ satisfies $\theta(p_{\mathrm{c}})=0$, where $\theta(p)=\mathbb{P}_p(|C_0|=\infty)$ and $p_{\mathrm{c}}=\inf\bigl(\{p\in[0,1]:\theta(p)>0\}\cup\{1\}\bigr)$. Lean: Percolation.Continuity.CSH.percolationContinuity_allDimensions (for all $d$, $2\le d\to{}$PercolationContinuity d) in Percolation/Continuity/MainTheorem.lean, where PercolationContinuity d := theta (zdGraph d) 0 (criticalProbI d) = 0 (Percolation/Literature/CriticalContinuity.lean). Comparator-checked form over Mathlib-only definitions: BondPercolation.percolation_continuity in Solution.lean, against Challenge.lean. The case $d=3$, $\theta(p_{\mathrm{c}}(\mathbb{Z}^3))=0$, is CSH.percolationContinuity_three, comparator-checked as BondPercolation.percolation_continuity_Z3.

The ‘$\cup\{1\}$’ only fixes the degenerate case $\theta\equiv0$; that this $p_{\mathrm{c}}$ equals $\sup\{p:\theta(p)=0\}$, and the equivalence with continuity of $\theta$ on $[0,1]$, are standard and not part of the formal statement.

Theorem 2.2 (additive gluing). Let $G$ be a finite weighted graph, $A$ a set of vertices, $o,b$ vertices and $t\ge0$. If $\mathbb{P}(a\leftrightarrow b)\ge1-t$ for every $a\in A$, then

Lean: CSH.additiveGluing_holds : Statements.AdditiveGluing (MainTheorem.lean; statement in Continuity/Statements.lean).

For $|A|=1$ this is the union bound; the content is that it does not deteriorate with $|A|$.

Corollary 2.3 (Kozma–Nitzan’s Conjecture 3). For every $\varepsilon>0$ there is $\delta>0$ ($\delta=\varepsilon/2$) such that for every finite weighted graph, every $A$ and all $o,b$: $\mathbb{P}(o\leftrightarrow A)>1-\delta$ and $\mathbb{P}(a\leftrightarrow b)>1-\delta$ for all $a\in A$ imply $\mathbb{P}(o\leftrightarrow b)>1-\varepsilon$. Lean: CSH.kozmaNitzan_conjecture3_holds : KozmaNitzan2024_conjecture3 (MainTheorem.lean); the statement, typed from [29 p. 15] in Literature/KozmaNitzanReduction.lean, coincides with Statements.NearOneGluing by Iff.rfl (nearOneGluing_iff_conjecture3, Continuity/OfGluing.lean).

The hierarchy: what the next definition encodes. For an increasing $f$ and any vertex $u$ the Harris inequality gives $\operatorname{Cov}(f(\mathcal{C}_x),\mathbf{1}\{u\in C_x\})\ge0$: nonnegative slack between $f$ and “the cluster of the owner $x$ reaches $u$”. The hierarchy compares the slack seen at two observers: at level $0$ it says that the slack at $o$ is at least the fraction $\tau$ of the slack at $v$, $\tau$ being the conditional probability that $o$ hangs on the cluster of $v$. When Section 3.4 removes relays one at a time, each removed vertex survives as a decoy $z_j$ which has already explained the part $c_j(u)\times(\text{slack at }z_j)$ of the slack at $u$; the level forms $\operatorname{sl}^j$ below subtract these parts, decoy by decoy, before the comparison is made. The induction proving the hierarchy (Section 3.3) runs in the complement of the cluster of an avoided set $Y$, which is why the covariances are conditioned on $\{x\nleftrightarrow Y\}$ (the constants $c_j,\tau$ are nevertheless computed under $\mathbb{P}$, Remark 3.1). We write $\mathrm{CSH}(Y;x;Z;o,v)$ for the assertion of Theorem 2.5 for the datum with avoided set $Y$, owner $x$, decoy list $Z$ and observers $o,v$ (in Lean CSHHolds w x Y D o v).

Definition 2.4 (datum, constants, level forms). Let $V$ be finite with weights in $(0,1)$ on all pairs (in Lean, on every element of Sym2 V; diagonal pairs never matter). A datum is an owner $x\in V$, an avoided set $Y\subseteq V\setminus\{x\}$, a list $Z=(z_1,\dots,z_\ell)$ of distinct decoys ($\ell$ is the level) and two distinct observers $o,v$, the named vertices $x,o,v,z_1,\dots,z_\ell$ pairwise distinct and outside $Y$. Put $\nu:=\mathbb{P}(\,\cdot\mid x\nleftrightarrow Y)$, $Y_j:=\{x\}\cup Y\cup\{z_1,\dots,z_{j-1}\}$ ($1\le j\le \ell+1$), and define the decoy constants and the observer constant

computed under $\mathbb{P}$, not $\nu$. For a real function $\varphi$ on $V$ the level forms are $\operatorname{sl}^0[\varphi]:=\varphi$,

Lean: CSH.avoidConst, decoyList, obsConst, slForm, cshMarg in Continuity/CSH/Defs.lean.

Theorem 2.5 (the conditioned slack hierarchy). For a datum as above and an increasing real function $f$ of sets of pairs, let $\kappa_f(u):=\operatorname{Cov}_\nu\bigl(f(\mathcal{C}_x),\mathbf{1}\{u\in C_x\}\bigr)$, $u\in V$. Then

At level $0$ this reads

and at level $1$ with $Y=\emptyset$ it reads $\kappa_f(o)-c(o)\kappa_f(z)\ge\tau\,[\kappa_f(v)-c(v)\kappa_f(z)]$ with $c(u)=\mathbb{P}(u\in C_z\mid z\nleftrightarrow x)$, $\tau=\mathbb{P}(o\in C_v\mid v\nleftrightarrow\{x,z\})$. Lean: CSH.cshHolds, concluding CSHHolds w x Y D o v (MainTheorem.lean; Lean’s D is the decoy list $Z$; CSHHolds, cshMargin in CSH/Defs.lean). The formal margin is (6) times $\mathbb{P}(x\nleftrightarrow Y)^2>0$, each conditional covariance being carried in the polynomial form $\mathbb{P}(x\nleftrightarrow Y)\mathbb{E}[f(\mathcal{C}_x);x\nleftrightarrow Y,x\leftrightarrow u]-\mathbb{E}[f(\mathcal{C}_x);x\nleftrightarrow Y]\mathbb{P}(x\nleftrightarrow Y,x\leftrightarrow u)$ (CSH.covD); CSH.cshAll repackages the hypotheses over Fin n.

For $Y=\emptyset$ and $f=\mathbf{1}\{v\in\cdot\,\}$, (7) is the Harris inequality: with $q:=\mathbb{P}(x\leftrightarrow v)$ one has $\kappa_f(o)=\mathbb{P}(o,v\in C_x)-q\,\mathbb{P}(o\in C_x)$, $\kappa_f(v)=q(1-q)$ and $\tau\kappa_f(v)=q\,\mathbb{P}(o\in C_v,\,v\nleftrightarrow x)$ (the factor $1-q=\mathbb{P}(v\nleftrightarrow x)$ cancels against the conditioning in $\tau$), so that by $\{o\leftrightarrow\{x,v\}\}=\{o\in C_x\}\sqcup\{o\in C_v,\,v\nleftrightarrow x\}$ the inequality $\kappa_f(o)\ge\tau\kappa_f(v)$ reads $\mathbb{P}(o\leftrightarrow\{x,v\},\,x\leftrightarrow v)\ge q\,\mathbb{P}(o\leftrightarrow\{x,v\})$. In general (7) says that, given that the owner avoids $Y$, the correlation of $f$ with “the owner reaches $o$” is at least the part of its correlation with “the owner reaches $v$” that is transported from $v$ to $o$ at the price $\tau$.

3 Proof sketch

Roadmap. The proof has four steps, and it is easiest to read them from the lattice down to the finite graph. Step 1 (Section 3.1) is Kozma and Nitzan’s theorem: if the near-one gluing statement (Conjecture 3) holds on every finite weighted graph, then $\theta(p_{\mathrm{c}})=0$ on $\mathbb{Z}^d$ for every $d\ge2$. The mechanism is a renormalisation at fixed $p$: an infinite cluster at $p$ lets one grow, box by box and with conditional probability close to one at each step, an infinite cluster inside a two-dimensional slab of $\mathbb{Z}^d$, gluing being exactly what carries the cluster from one box into the next; but no slab percolates at $p_{\mathrm{c}}$. This step is re-proved in the library and nothing in it is new. Step 2 (Section 3.2) observes that Conjecture 3 follows at once from the additive gluing inequality (3). Step 3 (Section 3.4) derives additive gluing from the conditioned slack hierarchy: gluing through a set $A$ of relays is proved by removing the relays one at a time, and what makes the induction close is a transfer inequality comparing a covariance seen from one observer with the same covariance seen from another; the removed relays do not disappear but survive as “decoys” whose influence is discounted, and the transfer inequality with $\ell$ decoys is precisely level $\ell$ of the hierarchy. Step 4 (Section 3.3), the heart of the work, proves the hierarchy by induction on the level: conditioning on the cluster of the avoided set splits the margin into a “horizontal” part, controlled by the Harris inequality, a negative-correlation inequality of van den Berg–Häggström–Kahn and a new two-source inequality, plus one term per decoy which is a margin of lower level. The simplest instance of level zero is the Harris inequality itself. We present Step 4 before Step 3, because Step 3 consumes its notation. Schematically (each arrow is a theorem of the development; beside it, what it consumes):

The labels are those of the Lean docstrings, each defined where it is first displayed: (S5) is a surplus-transfer inequality between two observers, (S5D) the same with decoys, (GEN) a first-relay lower bound for a general increasing functional and (AG-loc) its indicator case, a localised union bound (Section 3.4); (T), (U), (H) and Hpart are the three steps and the horizontal term of Section 3.3. Every subsection follows the pattern Goal / Idea / The inequality / Why it holds / In Lean.

3.1 From Conjecture 3 to $\theta(p_{\mathrm{c}})=0$: the theorem of Kozma and Nitzan (Step 1)

Goal. Conjecture 3 $\Rightarrow$ $\theta(p_{\mathrm{c}})=0$ on $\mathbb{Z}^d$ for every $d\ge2$ [29 Theorem 6]. Idea. Suppose $\theta(p)>0$. Then large boxes are joined to far-away targets with probability close to one, and gluing says that such near-certain connections can be chained without losing probability at each link, however many candidate link points there are. Chaining them along a planar grid of boxes builds, at the same $p$, an infinite cluster confined to a thick two-dimensional slab; applied at $p=p_{\mathrm{c}}$ this contradicts the fact that slabs, which sit inside a half-space, do not percolate at $p_{\mathrm{c}}(\mathbb{Z}^d)$. For $d=2$ the conclusion is classical. Nothing in this step is new; we follow [29 §4] and record where the formal route differs from print.

The statement is the implication KozmaNitzan2024_thm6 (Literature/KozmaNitzanReduction.lean), proved as KozmaNitzan2024_thm6_holds (KozmaNitzanTheorem6SlabCritical.lean). Why it holds. $d=2$: Harris’ $\theta(\tfrac12)=0$ and Kesten’s $p_{\mathrm{c}}(\mathbb{Z}^2)=\tfrac12$ (percolationContinuity_two, CriticalContinuity.lean; harris_theta_half_holds, kesten_criticalProb_Z2_holds); the library gets $\theta(\tfrac12)=0$ from RSW estimates [31, 32] as in [8 Ch. 3] and $p_{\mathrm{c}}\le\tfrac12$ by self-duality [22 Thm. (11.11)] with sharpness in the form of [16] (perc_sharpness_holds). $d\ge3$: with $S_k=\{0\le x_1\le k\}$ the slab and $\mathbb{H}=\{x_1\ge0\}$, (a) if Conjecture 3 holds and $\theta(p)>0$ then some slab percolates at the same $p$ (KozmaNitzan2024_slabPercolation_holds, KozmaNitzanTheorem6OfSlab.lean); (b) no slab percolates at $p_{\mathrm{c}}(\mathbb{Z}^d)$ (theta_slab_criticalProb_zd_eq_zero_holds); (a) at $p=p_{\mathrm{c}}$ contradicts (b).

Half (b): $\theta_{S_k}(p_{\mathrm{c}})\le\theta_{\mathbb{H}}(p_{\mathrm{c}})$ by monotonicity in the graph (theta_induce_mono_holds), and $\theta_{\mathbb{H}}(p_{\mathrm{c}}(\mathbb{Z}^d))=0$ is [7 Thm. 1.1] in the form [22 Thm. (7.35)] (BarskyGrimmettNewman1991_holds, HalfSpaceProofs.lean), proved for all $d\ge3$ by the block construction of [22 §7.3, Lemmas (7.36), (7.52)] (BGNd.lemma_7_36C, theta_pos_tall, theta_pos_flat): if $\theta_{\mathbb{H}}(p_{\mathrm{c}})>0$, bricks on $\partial\mathbb{H}$ would be “good” with probability above a universal threshold, hence (finitely many edges) also at some $p'<p_{\mathrm{c}}$, forcing $\theta(p')>0$. Deviation: [29 p. 25] and [22 (7.38)] take (b) from the Aizenman–Grimmett strict inequality $p_{\mathrm{c}}(S_k)>p_{\mathrm{c}}$ [4]; the formal proof avoids it (a.s. no open cluster of $\mathbb{H}$ is both infinite and of bounded height, BGNd.measure_percolatesVia_inter_heightLE_eq_zero). The slab theorem of [14] is formalised (DuminilCopinSidoraviciusTassion2016_holds) but off the main path.

Half (a): fix $d\ge3$ and $p$ with $\theta(p)>0$. Conjecture 3 enters only through the target lemma [29 Lemma 10] (KozmaNitzan.targetLemma, KozmaNitzanTargetLemma.lean): for every $\varepsilon$ there is $\delta$ such that, in any finite weighted graph containing a copy $\Lambda$ of a lattice box with sub-box $\Lambda_0$ and a “target” $\mathsf T\subseteq\Lambda$ reachable from every point near $\Lambda_0$ through a scaled hittable geometry [29 p. 16] (a region and a face such that, at this $p$, a large box is joined to the scaled face inside the scaled region with probability tending to one), $\mathbb{P}(o\leftrightarrow\Lambda_0)>1-\delta$ implies $\mathbb{P}(o\leftrightarrow\mathsf T)>1-\varepsilon$ for all $o\notin\Lambda$. The proof explores the cluster of $o$ inwards until a shell of $\Lambda_0$ is crossed by many branches, attaches seeds (bounded open edge sets at selected contact points [29 p. 19]), uses local uniqueness in mesoscopic boxes to funnel everything into one cluster, contracts the revealed configuration to a finite graph, and applies Conjecture 3 there with $\mathsf T$ wired to a point. Inputs: the square-root trick [22 (11.14)] (sqrt_trick_holds) and local uniqueness [29 Lemma 7], which Kozma and Nitzan take from Cerf [11] while noting that uniqueness of the infinite cluster suffices; the library takes that route, re-proving uniqueness [2, 10], [22 Thm. (8.1)] (Grimmett1999_numInfiniteClusters_le_one_holds). Then come the corridor lemma [29 Lemmas 11–12] (KozmaNitzanCorridor.lean) and the renormalisation [29 pp. 25–31] (KozmaNitzanScheme, -Steps, -Theorem6.lean): an exploration of macroscopic sites of $\mathbb{Z}^2\hookrightarrow\mathbb{Z}^d$ inside the region $L_r=\mathbb{Z}^2\times[-5r,5r]^{d-2}$, each examined site being good with conditional probability $>1-\varepsilon$ given the past [29 (33)] (KozmaNitzan.KSch.fail_bound). Deviation: where [29 p. 25] conclude by domination of a supercritical site process (“we skip the details”), the library runs an explicit Peierls contour estimate with $\varepsilon\le2^{-32}$ (DualContours.lean, HistorySiteRenormalization.lean), obtaining an infinite cluster in $L_r$, hence in the slab $S_{10r}$ (KozmaNitzan.exists_slab_theta_pos_of_three_le). Conjecture 3 is applied only to finite graphs built from finitely many boxes with edges contracted or deleted.

3.2 From additive gluing to Conjecture 3 (Step 2)

Goal. Theorem 2.2 $\Rightarrow$ Corollary 2.3. Why. Put $\delta=\varepsilon/2$; under the hypotheses of Conjecture 3, (3) with $t=\varepsilon/2$ gives $\mathbb{P}(o\leftrightarrow b)\ge\mathbb{P}(o\leftrightarrow A)-\varepsilon/2>1-\varepsilon$. In Lean: additiveGluingSuffices_proof (AdditiveGluing/Suffices.lean), CSH.conjecture3_of_csh. Illustration (not part of the development). On the $4$-cycle $o\,a_1\,b\,a_2$ with all weights $\tfrac12$ and $A=\{a_1,a_2\}$, enumeration of the $16$ configurations gives $\mathbb{P}(o\leftrightarrow A)=\tfrac34$, $\mathbb{P}(a_i\leftrightarrow b)=\tfrac9{16}$, $\mathbb{P}(o\leftrightarrow b)=\tfrac7{16}$; (3) with $t=\tfrac7{16}$ reads $\tfrac7{16}\ge\tfrac34-\tfrac7{16}=\tfrac5{16}$.

We now turn to the finite-graph inequalities themselves: first the hierarchy (Step 4), then the derivation of additive gluing from it (Step 3).

3.3 The conditioned slack hierarchy (Step 4)

Goal. Theorem 2.5: for every datum and every increasing $f$, $\operatorname{Marg}[\kappa_f]\ge0$. Throughout §§3.3–3.4 all weights lie in $(0,1)$, so every event “$u$ is joined to no vertex of a given set not containing $u$” has positive probability; the lattice symbols $p,d,k,S_k$ of §§1–3.1 do not occur. The symbols used more than once are:

Idea (see also the paragraph before Definition 2.4). Harris gives nonnegative slack $\operatorname{Cov}(f(\mathcal{C}_x),\mathbf{1}\{u\in C_x\})\ge0$ at every vertex $u$; gluing needs more, namely that the slack seen at $o$ is at least the fraction $\tau$ of the slack seen at $v$, $\tau$ being the chance that $o$ hangs on $v$’s cluster, because that is what lets a connection be passed from $v$ to $o$ (level $0$). A relay $z$ removed in Step 3 has already explained the part $c(u)\times(\text{slack at }z)$ of the slack at $u$; level $\ell$ says the transfer survives $\ell$ such discounts. The induction works in the complement of the cluster of a vertex set $Y$, whence $\nu$; the constants $c_j,\tau$ are nevertheless global (Remark 3.1).

Level $0$ is (7): $\kappa_f(o)\ge\tau\,\kappa_f(v)$ with $\tau=\mathbb{P}(o\in C_v\mid v\nleftrightarrow\{x\}\cup Y)$. The conditioning in $\tau$ cannot be dropped: on the path $o\!-\!x\!-\!v$ with both weights $\tfrac12$, $Y=\emptyset$ and $f=\mathbf{1}\{v\in\cdot\,\}$, the two edges are independent, so $\kappa_f(o)=0$ while $\mathbb{P}(o\leftrightarrow v)\,\kappa_f(v)=\tfrac14\cdot\tfrac14>0$; the conditioned price $\mathbb{P}(o\in C_v\mid v\nleftrightarrow x)$ is $0$. Illustration (not part of the development). On the triangle $\{x,o,v\}$ with all weights $\tfrac12$, $Y=\emptyset$, $f=\mathbf{1}\{v\in\cdot\,\}$, enumeration of the $8$ configurations gives $\kappa_f(o)=\tfrac7{64}$, $\kappa_f(v)=\tfrac{15}{64}$, $\tau=\tfrac13$, so the level-$0$ margin is $\tfrac7{64}-\tfrac13\cdot\tfrac{15}{64}=\tfrac1{32}>0$.

Level $1$ with $Y=\emptyset$: the worked example. One decoy $z$; the statement is $\kappa_f(o)-c(o)\kappa_f(z)\ge\tau\,[\kappa_f(v)-c(v)\kappa_f(z)]$ with $c(u)=\mathbb{P}(u\in C_z\mid z\nleftrightarrow x)$, $\tau=\mathbb{P}(o\in C_v\mid v\nleftrightarrow\{x,z\})$ and plain covariances ($\nu=\mathbb{P}$). The mechanism of the whole proof is already visible here. Put $X:=\{x,z\}$, $\mathcal E:=\{z\nleftrightarrow x\}$, $\rho:=\mathbb{P}(\cdot\mid\mathcal E)$ and, for a vertex set $K\not\ni x$, $\Phi(K):=\mathbb{E}\bigl[f(\mathcal{C}_x)-f(\mathcal{C}^{-K}_x)\bigr]$, where $\mathcal{C}^{-K}_x\subseteq\mathcal{C}_x$ is the owner’s cluster in $G\setminus K$ (pairs meeting $K$ deleted); thus $\Phi\ge0$ and $\Phi$ is increasing in $K$. Since $\{u\leftrightarrow X\}=\{u\in C_x\}\sqcup(\{u\in C_z\}\cap\mathcal E)$ and $\{z\in C_x\}$ is the complement of $\mathcal E$, one gets $\kappa_f(u)-c(u)\kappa_f(z)=\operatorname{Cov}(f(\mathcal{C}_x),\mathbf{1}\{u\leftrightarrow X\})-\operatorname{Cov}\bigl(f(\mathcal{C}_x),(\mathbf{1}\{u\in C_z\}-c(u))\mathbf{1}_{\mathcal E}\bigr)$, and the last covariance equals $\mathbb{E}[f(\mathcal{C}_x)(\mathbf{1}\{u\in C_z\}-c(u))\mathbf{1}_{\mathcal E}]$ because its second argument has mean $0$ by the choice of $c$. Condition on $C_z=K$: on $\mathcal E$ the set $K$ misses $x$, and given $C_z=K$ the configuration off $K$ is a fresh percolation on $G\setminus K$ (the Markov property, (K2) below), so $\mathbb{E}[f(\mathcal{C}_x)\mid C_z=K]=\mathbb{E} f(\mathcal{C}^{-K}_x)=\mathbb{E} f(\mathcal{C}_x)-\Phi(K)$; the constant $\mathbb{E} f(\mathcal{C}_x)$ integrates to $0$ once more, and centring at $c(u)=\mathbb{E}_\rho\mathbf{1}\{u\in C_z\}$ turns what is left into a covariance:

Taking (9) at $u=o$ minus $\tau$ times (9) at $u=v$, the level-one margin equals

The first bracket is nonnegative by the set version (13) below of level $0$, for the marker set $X$ (Harris and (K2)(b)). The second bracket is exactly the level-$0$ margin of the datum with owner $z$, avoided set $\{x\}$, no decoys and the same observers, at the functional $\Phi$—its observer constant $\mathbb{P}(o\in C_v\mid v\nleftrightarrow\{z\}\cup\{x\})$ is again $\tau$—so it is nonnegative by level $0$. Thus level $1$ at $Y=\emptyset$ already consumes level $0$ with the non-empty avoided set $\{x\}$ at a functional $\Phi$ that is not an indicator: the induction forces the hierarchy to be stated for all avoided sets and all increasing $f$ (the peeling of Section 3.4 independently needs $Y=R'\neq\emptyset$). Once $Y\neq\emptyset$ the covariances live under $\nu$ and the computation above must be done conditionally on the cluster of $Y$: that is where the worlds and the two-source inequality below come from; at $Y=\emptyset$ there is a single world, $\tau(U)=\tau$, and (14) is an identity.

General form. Definition 2.4 performs the $\ell$ discounts successively—the $j$-th decoy is conditioned to avoid the owner, $Y$ and the earlier decoys, which is what $Y_j$ records—and Theorem 2.5 asserts $\operatorname{Marg}[\kappa_f]\ge0$. Two algebraic facts are used: $\operatorname{Marg}[\varphi]=\sum_u\lambda(u)\varphi(u)$ over $u\in\{o,v,z_1,\dots,z_\ell\}$ (CSH.cshMarg_eq_sum_single), and, with $\operatorname{Marg}'$ the form of $z_2,\dots,z_\ell$ (same $c_2,\dots,c_\ell,\tau$),

(CSH.cshMarg_cons). Since $f\mapsto\operatorname{Marg}[\kappa_f]$ is linear and vanishes on constants, (6) is a finite family of polynomial inequalities in the weights.

Inputs. The proof of Theorem 2.5 uses four published inequalities, all re-proved in the library:

(K1) the Harris inequality [26], [22 Thm. (2.4)];

(K2) conditional association [34 Thms. 1.3–1.5, Remark 1]: for vertex sets $V_1,V_2$, given $\{V_1\nleftrightarrow V_2\}$, (a) two increasing functions of $\mathcal{C}_{V_1}:=\bigcup_{s\in V_1}\mathcal{C}_s$ are positively correlated, (b) an increasing function of $\mathcal{C}_{V_1}$ and one of $\mathcal{C}_{V_2}$ are negatively correlated; and the Markov property of cluster exploration [34 Lemmas 2.3–2.4] (off the explored cluster of $V_1$ the configuration is a fresh percolation);

(K3) Gladkov’s decision-tree Harris–Kleitman inequality [19 Thm. 3.2] (classical case [26, 28]): if a decision tree run on two independent configurations $(\omega_1,\omega_2)$ reveals a random set $\mathcal S$ of coordinates, then $(\mathbb{P}\otimes\mathbb{P})(\omega_1\in\mathsf A,\ \omega_1\!\to_{\mathcal S}\omega_2\in\mathsf B)\ge\mathbb{P}(\mathsf A)\mathbb{P}(\mathsf B)$ for increasing events $\mathsf A,\mathsf B$, $\omega_1\!\to_{\mathcal S}\omega_2$ being $\omega_1$ on $\mathcal S$ and $\omega_2$ elsewhere; for the tree exploring the cluster $C_N$ of a set $N$, with exploration $\sigma$-algebra $\mathcal F_N$, this is $\operatorname{Cov}(\mathbb{E}[\xi\mid\mathcal F_N],\eta)\ge0$ for increasing $\xi,\eta$: Harris survives stopping along an exploration (DecisionTree.PrW_mul_PrW_le_Pr2W_treeHK, TreeHarris.treeHarris_real; also the kernel form of Gladkov–Zimin [20 Ch. 5], [21], GladkovZiminKernel.lean);

(K4) the Ahlswede–Daykin four functions theorem [1] (Mathlib’s four_functions_theorem_univ): for a product measure $\sigma$ on $2^{U'}$, $\alpha(s)\beta(t)\le\gamma(s\cup t)\delta(s\cap t)$ for all $s,t$ implies $\sigma[\alpha]\sigma[\beta]\le\sigma[\gamma]\sigma[\delta]$.

Russo’s formula, RSW and the BK inequality (in the library for $d=2$) are not used on this path.

Why Theorem 2.5 holds: worlds, and three steps. Fix a datum and an increasing $f$. Under $\nu$ explore the cluster $C_Y$ and let $U:=V\setminus C_Y$, the world, with law $\pi$; on $\{x\nleftrightarrow Y\}$ it contains $x$. By the Markov property (K2), given $C_Y$ the configuration on $U$ is a fresh percolation on the graph induced on $U$ (pairs meeting $C_Y$ deleted); write $\mathbb{P}_U,\operatorname{Cov}_U$ for it, and set a world functional of $U$ to $0$ when a vertex it names is not in $U$. Let $\kappa^U(u):=\operatorname{Cov}_U(f(\mathcal{C}_x),\mathbf{1}\{u\in C_x\})$ and let $\mathcal W[f]:=\mathbb{E}_\pi[\operatorname{Marg}[\kappa^U]]$ be the world part: the margin computed inside each world, but with the global constants $c_j,\tau$, then averaged. The proof is an induction on the level $\ell$ (skeleton CSH.cshHolds_of_unfold, AdditiveGluing/CSHInduction.lean) in three steps: (T) reduces the margin to the world part; (U) splits the world part exactly into a horizontal term plus one lower-level margin per decoy; (H) shows the horizontal term is nonnegative.

(T) Telescoping. Goal: if $\mathcal W[f']\ge0$ for every increasing $f'\ge0$, then (6) holds for every increasing $f$. Idea: conditioning on the world loses the part of the covariance carried by the world itself; that part is again a covariance of the same shape for a new increasing functional, so one can iterate, and the iteration converges because the world is resampled from scratch with positive probability. Why: given the world, $f(\mathcal{C}_x)$ and $\mathbf{1}\{u\in C_x\}$ are functions of the percolation on $U$, so the law of total covariance under $\nu$ gives $\kappa_f(u)=\mathbb{E}_\pi[\kappa^U(u)]+\operatorname{Cov}_\nu\bigl(g(U),\mathbb{P}_U(u\in C_x)\bigr)$ with $g(U):=\mathbb{E}_Uf(\mathcal{C}_x)$, and two applications of the tower property ($g(U)$ is a function of $C_Y$, $\mathbf{1}\{u\in C_x\}$ of $\mathcal{C}_x$) rewrite the last term as $\operatorname{Cov}_\nu((\mathcal Af)(\mathcal{C}_x),\mathbf{1}\{u\in C_x\})$ with $(\mathcal Af)(\mathcal K):=\mathbb{E}_\nu[g(U)\mid\mathcal{C}_x=\mathcal K]$. The constants $c_j,\tau$ do not depend on $f$, so applying the linear form $\operatorname{Marg}$: the margin of $f$ is $\mathcal W[f]$ plus the margin of $\mathcal Af$. Here $\mathcal A$ is the transition operator of the two-block Gibbs sampler alternately resampling $C_Y$ given $\mathcal{C}_x$ and $\mathcal{C}_x$ given $C_Y$; $\mathcal Af$ is again increasing (a larger $\mathcal{C}_x$ leaves less room for $C_Y$, hence a larger world, and $g$ is increasing in $U$), and $\mathcal A^nf\to$ const since the chain regenerates with probability $\ge\prod(1-w_e)>0$ over the pairs leaving $Y$ (the one use of $w_e<1$); iterating, the margin of $f$ is $\sum_{i<n}\mathcal W[\mathcal A^if]$ plus a term tending to $0$. This is the scheme of [34 proof of Thm. 2.1] with Harris inside a world replaced by $\mathcal W\ge0$. In Lean: CSH.cshMargin_nonneg_of_within (CSH/LemmaT.lean), from BHK2006_multiMarkerCov_nonneg_of_within (Literature/TwoClusterGibbsCovariance.lean).

(U) Unfolding. Goal: an exact formula for $\mathcal W[f]$. Idea: inside a world, “the owner reaches $u$” differs from “$u$ is joined to the marker set $X$” exactly by the events “$u$ hangs on a decoy that misses the owner”; the level form was built so that these differences, decoy by decoy, reassemble into margins of the same hierarchy with that decoy as the new owner. The identity: with $\mathcal E_j:=\{z_j\nleftrightarrow Y_j\}$ and $\rho_j:=\mathbb{P}(\cdot\mid\mathcal E_j)$,

where $\operatorname{Marg}^{(j)}$ is the form of $z_{j+1},\dots,z_\ell$ (same constants) and, for a vertex set $K$,

($\mathcal{C}_x^{-K}$, $C_Y^{-K}$: clusters computed in $G\setminus K$; in the first term only $C_Y^{-K}$ is deleted, not $K$): the mean excess of the owner’s cluster after deleting only the cluster of $Y$ grown without $K$, over the owner’s cluster after deleting $K$. $\Phi\ge0$ because on $\{x\nleftrightarrow Y$ in $G\setminus K\}$ the cluster $\mathcal{C}_x^{-K}$ does not meet $C_Y^{-K}$ and therefore lies inside the cluster of the first term; $\Phi$ is increasing in $K$ because enlarging $K$ shrinks $C_Y^{-K}$ (so the first cluster grows) and shrinks $\mathcal{C}_x^{-K}$ (CSH.phiFun_nonneg, phiFun_mono); at $Y=\emptyset$ it is the $\Phi$ of the worked example. The point: the $j$-th summand is $\mathbb{P}(\mathcal E_j)/\mathbb{P}(x\nleftrightarrow Y)\ge0$ times the margin of the datum (owner $z_j$, avoided set $Y_j$, decoys $z_{j+1},\dots,z_\ell$, same observers) at the functional $\Phi$—a datum of lower level whose constants are literally $c_{j+1},\dots,c_\ell,\tau$—so the decoy terms are nonnegative by induction, and $\mathcal W[f]\ge0$ reduces to $\mathrm{Hpart}\ge0$. At level $\ell=1$ with $Y=\emptyset$ there is one world $U=V$, and (11) is the decomposition of the worked example obtained from (9). Why (11) holds. Fix a world $U$ and work under $\mathbb{P}_U$. Iterating the disjoint decomposition $\{u\leftrightarrow X_i\}=\{u\leftrightarrow X_{i-1}\}\sqcup(\{u\in C_{z_i}\}\cap\{z_i\nleftrightarrow X_{i-1}\})$, $X_i=\{x,z_1,\dots,z_i\}$, along the recursion (5), as in the derivation of (9), gives the pointwise identity $\operatorname{sl}^\ell[\mathbf{1}\{\cdot\in C_x\}](u)=\mathbf{1}\{u\leftrightarrow X\}-\sum_j\mathbf{1}\{z_j\nleftrightarrow X_{j-1}\}\,\operatorname{sl}^{(j)}[\mathbf{1}\{\cdot\in C_{z_j}\}-c_j](u)+\mathrm{const}$, where $\operatorname{sl}^{(j)}$ is the form of $z_{j+1},\dots,z_\ell$ (CSH.slForm_jn); taking $\operatorname{Cov}_U(f(\mathcal{C}_x),\cdot\,)$ (linear, zero on constants) and averaging over $\pi$, the first term yields Hpart. For the $j$-th term, the $\pi$-average of a world covariance $\operatorname{Cov}_U(f(\mathcal{C}_x),\psi)$ is $\mathbb{E}_\nu[(f(\mathcal{C}_x)-g(U))\,\psi^U]$, $\psi^U$ being $\psi$ read in the world of the full configuration (Markov property at $C_Y$, CSH.markov_merge_Y); a decoy swallowed by $C_Y$ is isolated in its world, so its term is constant there and integrates to $0$ against the residual (residual_orthogonal), while a decoy outside $C_Y$ has the same cluster in the world as in $G$ and $\{z_j\nleftrightarrow X_{j-1}$ in $U\}$ becomes $\mathcal E_j$. Conditioning finally on $C_{z_j}=K$ (Markov property at $C_{z_j}$; on $\mathcal E_j$, $K$ misses $x$ and $Y$), the residual times $\mathbf{1}\{x\nleftrightarrow Y\}$ has conditional mean $-\Phi(K)$, the term $g$ producing the first half of (12) (CSH.sum_phiIntegrand_eq) and $f$ the second; centring at $c_j(u')=\mathbb{E}_{\rho_j}\mathbf{1}\{u'\in C_{z_j}\}$ gives the covariance of (11), the factor $\mathbb{P}(\mathcal E_j)/\mathbb{P}(x\nleftrightarrow Y)$ coming from $\nu$ and $\rho_j$ (decoy_world_term). In Lean: CSH.within_unfold, subT_comb_nonneg (CSH/UnfoldMain.lean); decoy_world_term (CSH/UnfoldDecoy.lean).

(H) Horizontal part. Goal: $\mathrm{Hpart}\ge0$. Idea: inside each world the required transfer from $v$ to $o$ holds with the world’s own price $\tau(U)$; the price actually charged is the global $\tau$, and although $\tau(U)-\tau$ has no sign in a given world, on average over worlds the discrepancy helps. The inequalities: with the world’s own price $\tau(U):=\mathbb{P}_U(o\in C_v\mid v\nleftrightarrow X)$ write $\mathrm{Hpart}=\mathbb{E}_\pi[h_o(U)-\tau(U)h_v(U)]+\mathbb{E}_\pi[(\tau(U)-\tau)h_v(U)]$. The first integrand is nonnegative in every world by the set four-point transfer (stated under $\mathbb{P}$, applied under each $\mathbb{P}_U$)

and the second expectation is nonnegative by the two-source inequality

Here $\mathbb{E}_\pi[\psi(U)]=\mathbb{E}[\psi(V\setminus C_Y);x\nleftrightarrow Y]/\mathbb{P}(x\nleftrightarrow Y)$ for every world functional $\psi$, and $\tau=\mathbb{P}(o\in C_v\mid v\nleftrightarrow X\cup Y)$ because $Y_{\ell+1}=X\cup Y$; so (14) divided by $\mathbb{P}(x\nleftrightarrow Y)\,\mathbb{P}(v\nleftrightarrow X\cup Y)$ is precisely $\tau\,\mathbb{E}_\pi[h_v(U)]\le\mathbb{E}_\pi[\tau(U)h_v(U)]$. Why (13) holds: writing $f$ for $f(\mathcal{C}_x)$, $\bar f:=f-\mathbb{E} f$, and using $\{o\leftrightarrow X\cup\{v\}\}=\{o\leftrightarrow X\}\sqcup(\{o\in C_v\}\cap\{v\nleftrightarrow X\})$,

the first covariance on the right is $\ge0$ by (K1) and is dropped; the inequality is (K2)(b) given $\{v\nleftrightarrow X\}$ ($f$ is increasing in $\mathcal{C}_X$, $\mathbf{1}\{o\in C_v\}$ in $\mathcal{C}_v$); the last step is $-\mathbb{E}[\bar f;v\nleftrightarrow X]=\mathbb{E}[\bar f;v\leftrightarrow X]$. For $X=\{x\}$, $Y=\emptyset$, (13) is level zero (7)—the covariance form of Kozma–Nitzan’s two-relay mechanism [29 Thm. 1]. The two-source inequality (14) is where (K3) and (K4) enter. In Lean: CSH.hpart_nonneg (AdditiveGluing/CSHHtwBridge.lean), hpart_nonneg_of_htw (CSHHpart.lean); (14) is CSH.htw_world, from CovTau.p1H_univ (CovTau/A2H.lean).

The two-source inequality. Goal: (14). Idea: it is the diagonal case of an inequality with two independent “source sets” whose clusters are explored, of the type introduced by van den Berg–Kahn and van den Berg–Häggström–Kahn for connection probabilities; the novelty is that one of the four quantities is a covariance, which is not monotone in the configuration, and what replaces monotonicity is a one-source bound obtained from Harris’ inequality stopped along the exploration. The inequality: with worlds indexed by their vertex set $U$ as above, put $\mathrm E_X(U):=\mathbb{P}_U(o\in C_v,v\nleftrightarrow X)$, $\mathrm M_X(U):=\mathbb{P}_U(v\nleftrightarrow X)$ (so $\tau(U)=\mathrm E_X(U)/\mathrm M_X(U)$) and $h:=h_v$; for a source set $N\subseteq U$ and any world functional $\psi$ let $\langle\psi\rangle^U_N:=\mathbb{E}_U[\psi(U\setminus C_N)]$: explore the cluster of $N$ inside $U$ and evaluate $\psi$ on what is left. Then (14) is the diagonal $N=N'=Y$, $U=V$ of

(indeed $\langle\mathrm E_X\rangle^V_Y=\mathbb{P}(o\in C_v,\,v\nleftrightarrow X\cup Y)$ and $\langle\mathrm M_X\rangle^V_Y=\mathbb{P}(v\nleftrightarrow X\cup Y)$ by the Markov property, and $\langle h\rangle^V_Y=\mathbb{E}[h(V\setminus C_Y);x\nleftrightarrow Y]$ since $h$ vanishes on worlds not containing $x$). Why: the input about $h$ is the pair of one-source bounds, valid in every sub-world,

exploring the cluster of a source set and recomputing the covariance in what is left loses on average at least the fraction $\mathbb{P}_U(v\leftrightarrow N\mid v\nleftrightarrow X)$. Proof of (16): total covariance along $\mathcal F_N$; the term $\operatorname{Cov}(\mathbb{E}[f(\mathcal{C}_x)\mid\mathcal F_N],\mathbf{1}\{v\leftrightarrow X\cup N\})$ that remains is $\ge0$ by (K3), and (K2)(b) for the sets $X$, $\{v\}$ supplies the factor; antitonicity of $N\mapsto\langle h\rangle^U_N$ follows from the second bound. Base case of (15), $N\cap N'=\emptyset$: by (16), $\langle h\rangle_{N'}\le\mathbb{P}_U(v\nleftrightarrow N'\mid v\nleftrightarrow X)\,h(U)$, and (K2)(a) for the cluster of $v$ given $\{v\nleftrightarrow X\}$ gives $\langle\mathrm E_X\rangle_N\mathbb{P}_U(v\nleftrightarrow N'\mid v\nleftrightarrow X)\le\tau(U)\langle\mathrm M_X\rangle_{N\cup N'}$; multiply. Induction on $|U|$, the scheme of van den Berg–Kahn [35] and [34 proof of Thm. 1.1]: for $N_0:=N\cap N'\ne\emptyset$, condition on the open star $\mathfrak S\subseteq U':=U\setminus N_0$ of $N_0$ (vertices joined to $N_0$ by an open edge), whose law $\sigma$ is a product measure on $2^{U'}$ and for which $C_N=N_0\cup C'_{(N\setminus N_0)\cup\mathfrak S}$ with $C'$ computed in $U'$; then each bracket in (15) is a $\sigma$-average, and (K4) is applied on $2^{U'}$ to $\alpha(s)=\langle\mathrm E_X\rangle^{U'}_{(N\setminus N_0)\cup s}$, $\beta(s)=\langle h\rangle^{U'}_{(N'\setminus N_0)\cup s}$, $\gamma(s)=\langle\mathrm M_X\rangle^{U'}_{((N\cup N')\setminus N_0)\cup s}$, $\delta(s)=\langle\tau h\rangle^{U'}_{s}$, the pointwise hypothesis being (15) in the smaller world $U'$ together with antitonicity in the source set. In Lean: CovTau.a2H, generic induction CovTau.metaA2_of_star (CovTau/MetaA2.lean), product law of the star CovTau/A2Push.lean, one-source bounds CovTau/StarH.lean, antitonicity CovTau/MetaA2Anti.lean.

Level zero in the formal development (an aside on the Lean route). The formal proof of level $0$ does not go through (T)+(H), although those steps are formalised for every level: the development treats $\ell=0$ separately (CSH.cshMargin_nil_nonneg, from CovTau.markerDominanceAvoid) and invokes (U) only for $\ell\ge1$; (7), denominator-free and for a general avoided set, is proved in Continuity/HullPort/ from a singleton-marker one-source bound of type (16) obtained from (K3) and (K2) (HullPort.CE_holds), by an induction on the avoided set in which the weight $\vartheta$ of one pair at a time is deformed (HullPort.bernstein_step, taQ_nonneg_of_Pv): the quantity to be shown nonnegative has the form $\mathcal Q=\mathcal I_1\mathcal J_2-\mathcal J_1\mathcal I_2$ with $\mathcal I_i,\mathcal J_i$ affine in $\vartheta$, and a Bernstein-type identity expresses $\mathcal Q(\vartheta)$ on $[0,1]$ through $\mathcal Q(0),\mathcal Q(1)$ (the pair deleted or contracted, covered by the induction) and a cross term whose sign is (K2)(a) for the cluster of $v$—without (K4).

Remark 3.1 (why global constants). Because the constants are computed under $\mathbb{P}$, the sub-system generated by $z_j$ in (11) is conditioned on exactly the event defining $c_j$ and the later constants are unchanged, so the decoy terms are lower levels of the same hierarchy; centring at world constants instead would require a two-source inequality with two different covariance functionals, which is not available; the global centring produces exactly (14).

We now have the hierarchy for every owner, avoided set, decoy list and pair of observers. The remaining issue is to turn this statement about one cluster and two observers into a statement about an observer and a whole set of relays.

3.4 From the hierarchy to additive gluing (Step 3)

Goal. Theorem 2.5 $\Rightarrow$ Theorem 2.2. Idea. Order the relays $a\in A$ by how valuable they are (here: by $\mathbb{P}(a\leftrightarrow b)$) and charge the failure of $o$ to reach $b$ to the first relay that $o$ holds; this localised union bound (AG-loc) gives additive gluing immediately, and it is the indicator case of a statement (GEN) about an arbitrary increasing functional $F$ of clusters: on the event that $o$ holds some relay, $F(C_o)$ is on average worth at least the mean worth of the first relay held. (GEN) is proved by removing the most valuable relay; the cost of doing so is controlled by a surplus-transfer inequality (S5) between two observers, and (S5) in turn is proved by the same removal, the removed relays becoming decoys—which is where the hierarchy is consumed, twice per step.

The inequalities. Fix an increasing $F\ge0$ on vertex sets, $m_a:=\mathbb{E} F(C_a)$. For a relay set $R$ list its elements so that $m$ is non-decreasing (a compatible rank); on $\{u\leftrightarrow R\}$ the first relay $\iota(u)$ is the relay of least rank in $C_u$, and the events $P^u_a=\{\iota(u)=a\}=\{u\leftrightarrow a\}\cap\bigcap_{a'\prec a}\{u\nleftrightarrow a'\}$ partition $\{u\leftrightarrow R\}$. The surplus of $u$ over its first relay is

(CSH.surplus); the second form shows independence of the rank, and $\operatorname{Sur}_u(\{x\})=\operatorname{Cov}(F(C_x),\mathbf{1}\{u\in C_x\})$. The links of (8) between CSH and (3) are

(S5) says the surplus seen from $o$ is at least that seen from $v$, discounted by the probability that $o$ is glued to $v$ while $v$ misses the relays. (S5D)$[R;Z;o,v]$ (relay set; decoy list; observers) is $\operatorname{Marg}[u\mapsto\operatorname{Sur}_u(R)]\ge0$ for a list $Z$ of decoys with constants as in (4) ($z_j$ avoiding $R\cup\{z_1,\dots,z_{j-1}\}$, $v$ avoiding $R\cup Z$; CSH.surplusMargin); (S5) is its case $\ell=0$ times $\mathbb{P}(v\nleftrightarrow R)$, and for $R=\{x\}$ it is $\mathrm{CSH}(\emptyset;x;Z;o,v)$ at $\widehat F(\mathcal{C}):=F(V(\mathcal{C})\cup\{x\})$—so with one relay, (S5D) is the hierarchy.

Why $\mathrm{CSH}\Rightarrow$ (S5D) (peeling). Weights in $(0,1)$; induction on $|R|$ for all decoy lists at once. Let $a_s$ be the top relay, $R'=R\setminus\{a_s\}$, $\mathcal D_s=\{a_s\nleftrightarrow R'\}$, $\nu_s=\mathbb{P}(\cdot\mid\mathcal D_s)$, $c_s(u)=\nu_s(u\in C_{a_s})$, $\gamma_s=\operatorname{Cov}(F(C_{a_s}),\mathbf{1}\{a_s\leftrightarrow R'\})$. The bookkeeping fact: the constants of $[R;Z;o,v]$ are those of $[R';(a_s,Z);o,v]$, in which $a_s$ has become the first decoy. Then: (P) $\{u\leftrightarrow R\}=\{u\leftrightarrow R'\}\sqcup(\{u\in C_{a_s}\}\cap\mathcal D_s)$ gives $\operatorname{Sur}_u(R)=\operatorname{Sur}_u(R')+\mathbb{P}(\mathcal D_s)\operatorname{Cov}_{\nu_s}(F(C_{a_s}),\mathbf{1}\{u\in C_{a_s}\})-\gamma_sc_s(u)$ (surplus_erase_add); ($\gamma$) $\gamma_s\le\operatorname{Sur}_{a_s}(R')$, as on $\{a_s\leftrightarrow R'\}$ the first relay of $a_s$ has smaller mean—the only use of compatibility (kappa_le_surplus); (AC) $\operatorname{Marg}[c_s]\ge0$, by $\mathrm{CSH}(R';a_s;Z;o,v)$ at $\Psi_{\mathrm{iso}}(\mathcal{C})=\mathbf{1}\{\mathcal{C}\ne\emptyset\}$, for which $\operatorname{Cov}_{\nu_s}(\Psi_{\mathrm{iso}},\mathbf{1}\{u\in C_{a_s}\})=c_s(u)\nu_s(\mathcal{C}_{a_s}=\emptyset)$ (covD_psiIso); (N) by (10), $\operatorname{Marg}[\operatorname{Sur}(R')]-\operatorname{Sur}_{a_s}(R')\operatorname{Marg}[c_s]=\operatorname{Marg}'[\operatorname{Sur}(R')]$, the form with one relay fewer and one decoy more. The middle term of (P) being $\mathbb{P}(\mathcal D_s)$ times the margin of $\mathrm{CSH}(R';a_s;Z;o,v)[\widehat F]\ge0$,

by induction. Each step uses Theorem 2.5 twice; (S5) for $|R|=s$ consumes levels $0,\dots,s-1$. In Lean: CSH.surplusMargin_nonneg_of_csh (CSH/Peel.lean, PeelTools.lean).

Why (S5)$\Rightarrow$(GEN). By (17), (GEN) says $\operatorname{Sur}_o(A)\ge0$. Weights in $[0,1]$; induction on $|A|$ using only (S5), (K1), (K2)(a). With $a_s,A',\mathcal D_s,\gamma_s$ as above ($A$ in place of $R$) and $F_s=F(C_{a_s})$, (P) gives $\operatorname{Sur}_o(A)=\operatorname{Sur}_o(A')-\Delta$, $\Delta=\mathbb{E}[(m_{a_s}-F_s)\mathbf{1}\{o\in C_{a_s}\}\mathbf{1}_{\mathcal D_s}]$, and by (K2)(a) for the cluster of $a_s$ given $\mathcal D_s$, then ($\gamma$),

while (S5) for $A'$ with $v=a_s$ reads $\mathbb{P}(\mathcal D_s)\operatorname{Sur}_o(A')\ge\mathbb{P}(o\in C_{a_s},\mathcal D_s)\operatorname{Sur}_{a_s}(A')$; subtracting, $\mathbb{P}(\mathcal D_s)\operatorname{Sur}_o(A)\ge0$, which is (GEN) for $A$ if $\mathbb{P}(\mathcal D_s)>0$. If $\mathbb{P}(\mathcal D_s)=0$ (possible with weights in $[0,1]$) then $\Delta=0$ and $\operatorname{Sur}_o(A)=\operatorname{Sur}_o(A')\ge0$ by the induction hypothesis; this is its only use. In Lean: AGloc.gen_firstRank_of_surplusTransfer (AdditiveGluing/GenOfSurplusTransfer.lean; two relays directly in GenPair.lean).

Why (GEN)$\Rightarrow$(AG-loc)$\Rightarrow$(AG). At $F=\mathbf{1}\{b\in\cdot\,\}$, $m_a=\mathbb{P}(a\leftrightarrow b)$ and $\mathbb{E}[F(C_o);o\leftrightarrow A]=\mathbb{P}(o\leftrightarrow A,o\leftrightarrow b)$; as the $P^o_a$ partition $\{o\leftrightarrow A\}$, (GEN) gives $\mathbb{P}(o\leftrightarrow A,o\nleftrightarrow b)\le\sum_a\mathbb{P}(P^o_a)(1-\mathbb{P}(a\leftrightarrow b))$; under $\mathbb{P}(a\nleftrightarrow b)\le t$ this is $\le t\mathbb{P}(o\leftrightarrow A)\le t$, and $\mathbb{P}(o\leftrightarrow A)-\mathbb{P}(o\leftrightarrow b)\le\mathbb{P}(o\leftrightarrow A,o\nleftrightarrow b)$. In Lean: AGloc.agloc_firstRank_of_gen, additiveGluing_of_agloc_firstRank (AdditiveGluing/OfAGloc.lean).

Boundary cases. Peeling gives (S5) for weights in $(0,1)$ and $o\ne v$ outside $R$; $o=v$ and $o\in R$ are elementary (surplus_nonneg_of_mem), and weights in $[0,1]$ (absent and contracted edges) follow by closure: by the min-form in (17) both sides of (S5) are rank-free polynomials in the weights (CSH.surplus_eq_minForm), so (S5) passes from $(0,1)^E$ to $[0,1]^E$, $E$ the set of pairs (weights_le_of_forall_pos_lt_one, AGloc.exists_rank_compat; AdditiveGluing/OfSurplusTransfer.lean, SurplusClosure.lean).

Remark 3.2 (Kozma–Nitzan’s Conjecture 1 for three relays). The library proves the following (CovTau.kn_conj1_three, Percolation/Continuity/CovTau/OfTA.lean): on a finite weighted graph, for vertices $o,b,a_1,a_2,a_3$ with $a_3\ne a_1$, $a_3\ne a_2$ and $\mathbb{P}(a_1\leftrightarrow b)\le\mathbb{P}(a_2\leftrightarrow b)\le\mathbb{P}(a_3\leftrightarrow b)$, and every real $t\le\mathbb{P}(a_1\leftrightarrow b)$, one has $t\cdot\mathbb{P}\bigl(\{o\leftrightarrow a_1\}\cup\{o\leftrightarrow a_2\}\cup\{o\leftrightarrow a_3\}\bigr)\le\mathbb{P}(o\leftrightarrow b)$. Up to relabelling the relays so that $\mathbb{P}(a_i\leftrightarrow b)$ is non-decreasing, this is Conjecture 1 (2) for $|A|=3$. The general Conjecture 1, and Conjectures 2 and 4, are not addressed in this development.

3.5 Assembly: proof of Theorem 2.1 from the pieces

(i) Theorem 2.5 holds: strong induction on the level $\ell$, the step being (T)+(U)+(H) of Section 3.3 with (H) fed by the two-source inequality (14) (CSH.cshHolds $=$ cshHolds_of_unfold with within_nonneg_of_hpart and hpart_nonneg). (ii) By Section 3.4, peeling turns Theorem 2.5 into (S5D), hence (S5), hence (GEN), hence (AG-loc), hence Theorem 2.2 for weights in $(0,1)$, and closure gives all weights (CSH.additiveGluing_of_csh, CSH/AdditiveGluingOfCSH.lean). (iii) By Section 3.2, Theorem 2.2 with $t=\varepsilon/2$ is Corollary 2.3 (CSH.conjecture3_of_csh). (iv) By Section 3.1, Kozma–Nitzan’s Theorem 6 applied to Corollary 2.3 gives $\theta(p_{\mathrm{c}})=0$ on $\mathbb{Z}^d$ for every $d\ge2$ (CSH.percolationContinuity_of_csh via KozmaNitzan2024_thm6_holds); $d=3$ is percolationContinuity_three. (v) Solution.lean transports percolationContinuity_allDimensions along bridge (Iff.rfl: the two PercolationContinuity propositions unfold to the same term), and the comparator checks that the statement proved is that of Challenge.lean. $\square$

4 Guide to the formalization

Size and pins. 251 Lean files, 97,574 lines (87,136 non-blank): about 12,200 lines in 63 files under Percolation/Continuity/ (this work) and 85,000 in 183 files under Percolation/Literature/, plus Percolation.lean, Util/Linter.lean, Challenge.lean, Solution.lean, scripts/Axioms.lean. Toolchain leanprover/lean4:v4.32.0; Mathlib commit 81a5d257c8e4 (its tag v4.32.0), pinned [12, 33]. Table 1 is the module map.

folder / file	contents	key declarations
Challenge.lean, Solution.lean	statement file (Mathlib only); proved twin	BondPercolation.percolation_continuity, percolation_continuity_Z3, bridge
Continuity/MainTheorem, Statements, OfGluing	main theorems; gluing statements	CSH.cshHolds, additiveGluing_holds, kozmaNitzan_conjecture3_holds, percolationContinuity_allDimensions
Continuity/CSH/ (12 files)	Definition 2.4, Theorem 2.5; (T), $\Phi$, (U); peeling	CSHHolds, cshMargin, cshMargin_nonneg_of_within, within_unfold, phiFun_mono, surplusMargin_nonneg_of_csh
Continuity/AdditiveGluing/ (13)	induction skeleton; (H); (S5)$\Rightarrow$(GEN)$\Rightarrow$(AG); weight closure	cshHolds_of_unfold, hpart_nonneg, gen_firstRank_of_surplusTransfer, additiveGluing_of_agloc_firstRank, surplusTransfer_of_nondegenerate
Continuity/CovTau/ (19), HullPort/ (12), LowerTail/ (4)	two-source (15), one-source (16); level-zero chain; tree-Harris for real functions	metaA2_of_star, a2H, p1H_univ, markerDominanceAvoid, taQ_nonneg_of_Pv, treeHarris_real, kn_conj1_three
Literature/Basic, CriticalContinuity, LatticeModels/	the model; product measures; weight continuity	zdGraph, bondPercolation, theta, criticalProb, prodBernoulli, PercolationContinuity
Literature/KozmaNitzan* (16)	[29 §§2–4]: Conj. 3, Thm. 6, Thms. 1, 3, 4, 7, 8, Lemmas 6–12	KozmaNitzan2024_conjecture3, KozmaNitzan2024_thm6_holds, targetLemma, KozmaNitzan2024_slabPercolation_holds
Literature/HalfSpace*, Tall*, Flat*, Slab*, Uniqueness*, DualContours	BGN via [22 §7.3]; DST; uniqueness; contours	BarskyGrimmettNewman1991_holds, DuminilCopinSidoraviciusTassion2016_holds, Grimmett1999_numInfiniteClusters_le_one_holds
Literature/Harris*, Kesten*, RSW*, Russo*, PlanarDuality, SharpnessDCT*	$d=2$	harris_theta_half_holds, kesten_criticalProb_Z2_holds, rsw_half_holds, russo_formula_holds, perc_sharpness_holds
Literature/ConditionalPositiveAssociation*, TwoCluster*, TwoSet*, DecisionTree*, TargetExploration*, GladkovZiminKernel	[34] Thms. 1.1–1.5 and §2.1; [19 Thm. 3.2]; [20 Ch. 5]; Harris	BHK2006_clusterConditionalPositiveAssociation_holds, BHK2006_twoSetConditionalAssociation, BHK2006.harris, PrW_mul_PrW_le_Pr2W_treeHK, ED_ED_le_ED_diag

Re-proved versus new. Everything under Literature/ re-proves published results from Mathlib (docstring tags [cite: Key, locator] resolve in references.bib; a literature result is a def AuthorYear_result : Prop discharged by theorem AuthorYear_result_holds; nothing is assumed). Re-proved in this way are the results in the lower half of Table 1 (Kozma–Nitzan’s Theorems 1, 3, 4, 6, 7, 8 and Lemmas 6–12 among them). Everything under Continuity/ is this work (a [cite:] tag there points to a statement a lemma specialises, not to a source of its proof): new are Theorem 2.5, Theorem 2.2, Corollary 2.3 and the chain between them, including (S5), (GEN), (AG-loc), (14), (15).

Trusted base and checks. All seven main theorems depend only on propext, Classical.choice, Quot.sound (scripts/Axioms.lean); sorry occurs twice, in Challenge.lean by design; no axiom declarations, no unsafe code. lake exe cache get && lake build builds the default targets (about 6 minutes, per AUDIT.md); the CI script runs the Palomar acceptance check—the Lean comparator² with lean4export, the independent nanoda kernel and the landrun sandbox—on comparator.json. formalization.yaml records scope, divergences and review status for the Palomar registry³. The docstrings are machine-written working notes, a map rather than an exposition.

5 Limitations and open directions

Other conjectures of Kozma–Nitzan. Conjecture 1 (2) is proved only for $|A|=3$ (CovTau.kn_conj1_three, stated with its hypotheses in Remark 3.2); the general Conjecture 1, Conjectures 2 and 4, and Questions 5–9 of [29 §5] are not addressed in this development. Rates. Nothing quantitative is proved: no bound on $\theta(p)$ as $p\downarrow p_{\mathrm{c}}$, on the tail of $|C_0|$ at $p_{\mathrm{c}}$, or on $\delta(\varepsilon)$ beyond $\varepsilon/2$. Other models. The lattice theorem is proved only for nearest-neighbour bond percolation on $\mathbb{Z}^d$; site percolation, other lattices and long-range models would need the reduction re-run there; nothing new is proved about slabs. Exposition. A conventional written proof refereed by experts does not yet exist.

Acknowledgements. The reduction that makes this result accessible is due to Gady Kozma and Shahaf Nitzan. The Lean formalization and the first drafts of this document were produced by Claude (Anthropic) working under my direction; I am responsible for the final text and for any errors. I thank Ralph Furman and Levent Alpöge for reading and comments. The formalization stands on Lean 4, on Mathlib and its community, and on the Lean comparator, lean4export, nanoda and the Palomar template.