Proofs of the Kozma–Nitzan conjectures

Kozma and Nitzan (arXiv:2401.12397) reduced the statement \(\theta(p_c) = 0\) for Bernoulli bond percolation on \(\mathbb{Z}^d\), \(d \ge 2\), to an inequality on finite graphs, their Conjecture 3, and posed four further conjectures and four questions about connection probabilities in finite graphs: Conjectures 1, 2, 4 and 6 and Questions 5, 7, 8 and 9. Anthropic's Lean 4 / Mathlib proof of \(\theta(p_c) = 0\) for Bernoulli bond percolation on \(\mathbb{Z}^d\) in all dimensions \(d \ge 2\) (written by Claude under the direction of Justin Leder) proves Conjecture 3. It does not claim Conjecture 1, but Conjecture 1 is a relatively easy consequence of an inequality proved there on the way, as explained below.

Here the remaining conjectures and questions of the paper are proved on top of that Lean proof: Conjectures 1, 2, 4 and 6 and Questions 5, 7 and 9, each in a stronger form than stated. Question 8 is false as printed. The proofs are in the summary (PDF); the Lean files are in lean/. Warning: the manuscript has not yet undergone extensive independent proofreading.

Notation

Throughout, \(G\) is a finite graph in which each edge \(e\) is open independently with probability \(p_e \in [0,1]\). For vertices \(x\) and \(y\), \(x \leftrightarrow y\) means that \(x\) and \(y\) are joined by a path of open edges, and \(C_x\) is the set of vertices joined to \(x\), the open cluster of \(x\). For a set \(A\) of vertices, \(o \leftrightarrow A\) means that \(o \leftrightarrow x\) for some \(x \in A\), and \(o \nleftrightarrow A\) is its negation. A comma inside a probability means intersection, \(\mathbb{P}(E, F) = \mathbb{P}(E \cap F)\), and \(\mathbb{E}[X;\, E]\) is the expectation of \(X\) on the event \(E\). Increasing functions \(F\) of vertex sets are those with \(F(K) \le F(L)\) whenever \(K \subseteq L\). Page numbers refer to the paper.

Conjecture 1 from the Lean proof of Conjecture 3

Fix \(A\), \(o\) and \(b\), and order the vertices of \(A\) so that \(\mathbb{P}(x \leftrightarrow b)\) is nondecreasing. The Lean proof of Conjecture 3 contains the inequality \[ \sum_{x \in A} \mathbb{P}\bigl(o \leftrightarrow x \text{ and } o \nleftrightarrow y \text{ for every } y \in A \text{ before } x\bigr)\, \mathbb{P}(x \leftrightarrow b) \;\le\; \mathbb{P}(o \leftrightarrow b). \] The events on the left partition \(\{o \leftrightarrow A\}\), and every factor \(\mathbb{P}(x \leftrightarrow b)\) is at least the minimum over \(A\), so \[ \mathbb{P}(o \leftrightarrow A)\, \min_{x \in A} \mathbb{P}(x \leftrightarrow b) \;\le\; \mathbb{P}(o \leftrightarrow b), \] which is Conjecture 1 (p. 3) for every finite graph and every choice of edge probabilities.

The results

• Conjecture 4 (p. 32). Let \(F\) be an increasing function of vertex sets and let \(a \in A\) minimise \(\mathbb{E}\,F(C_x)\) over \(x \in A\). Then \(\mathbb{E}[F(C_a);\, o \leftrightarrow A] \le \mathbb{E}[F(C_o);\, o \leftrightarrow A]\). In particular \(\min_{x \in A} \mathbb{E}[F(C_x);\, o \leftrightarrow A] \le \mathbb{E}[F(C_o);\, o \leftrightarrow A]\), which is Conjecture 4; the same holds in the paper's formulation with a monotone cluster property \(f(v, \omega)\) in place of \(F(C_v)\).
• Conjecture 2 (p. 3), in the pre-FKG form (3): \(\min_{x \in A} \mathbb{P}(x \leftrightarrow b,\, o \leftrightarrow A) \le \mathbb{P}(o \leftrightarrow b,\, o \leftrightarrow A)\). Hence \(\min_{x \in A} \mathbb{P}(o \leftrightarrow A,\, x \leftrightarrow b) \le \mathbb{P}(o \leftrightarrow b)\), which is display (2).
• Question 7 (p. 36), answered yes. Let \(a \in A\) minimise \(\mathbb{P}(x \leftrightarrow b)\) over \(x \in A\). Then \(\mathbb{P}(o \leftrightarrow A,\, a \leftrightarrow b) \le \mathbb{P}(o \leftrightarrow b,\, o \leftrightarrow A)\), which is display (41).
• Conjecture 1 (p. 3), as above, and Conjecture 3 (p. 15) from it: for every \(\varepsilon > 0\) there is \(\delta > 0\) such that if \(\mathbb{P}(o \leftrightarrow A) > 1 - \delta\) and \(\mathbb{P}(x \leftrightarrow b) > 1 - \delta\) for every \(x \in A\), then \(\mathbb{P}(o \leftrightarrow b) > 1 - \varepsilon\).
• Question 5 (p. 32), answered yes. There are numbers \(c_a \ge 0\), \(a \in A\), with \(\sum_{a \in A} c_a = 1\), depending on \(G\), \(A\) and \(o\) but not on \(b\), such that \(\sum_{a \in A} c_a\, \mathbb{P}(o \leftrightarrow A,\, a \leftrightarrow b) \le \mathbb{P}(o \leftrightarrow b)\) for every vertex \(b\), which is display (38).
• Conjecture 6 (p. 34). Let \(e = \{v, w\}\) be an edge of \(G\), let \(a \in A\) minimise \(\mathbb{P}_G(x \leftrightarrow b)\) over \(x \in A\), and let \(G/e\) be the graph with the edge \(e\) shortened, that is, with the probability that \(e\) is open set to \(1\). Then \(\mathbb{P}_{G/e}(v \leftrightarrow b,\, v \leftrightarrow A) \ge \mathbb{P}_{G/e}(a \leftrightarrow b,\, v \leftrightarrow A)\), and therefore \(\mathbb{P}_{G/e}(v \leftrightarrow b) \ge \mathbb{P}_{G/e}(v \leftrightarrow A)\, \mathbb{P}_{G/e}(a \leftrightarrow b)\), which is display (40). The paper assumes in addition its display (39); that assumption is not needed, and it is in any case a consequence of Conjecture 1.
• Question 9 (p. 36), answered yes. Let \(H\) be \(G\) with every edge at \(o\) removed and let \(a \in A\) minimise \(\mathbb{P}_H(x \leftrightarrow b)\) over \(x \in A\). Then \(\mathbb{P}(o \leftrightarrow A,\, a \leftrightarrow b) \le \mathbb{P}(o \leftrightarrow b,\, o \leftrightarrow A)\) in \(G\).
• Question 8 (p. 36), which takes a vertex \(a \in A\) minimising \(\mathbb{P}(x \leftrightarrow b,\, o \nleftrightarrow A)\), is false as printed.

In the paper, Conjectures 2 and 4 are proved when \(A\) has two vertices (Theorems 1 and 7), when \(A\) has three vertices under extra hypotheses (Theorems 2, 3 and 11), when \(o\) is isolated in \(G \setminus A\) or joined only to \(A\) and to one further vertex (Theorems 4 and 5), and for the functions \(f = \mathbf{1}\{|C| \ge k\}\) with \(k \le 4\) on every graph (Theorem 9).

The method

The proofs run the argument of the Lean proof of Conjecture 3 with two changes. First, the clusters of the vertices of \(A\) are conditioned on missing a given set \(Y\) of vertices: if the vertices of \(A\) are ordered so that \(\mathbb{E}[F(C_x) \mid x \nleftrightarrow Y]\) is nondecreasing, then \[ \sum_{x \in A} \mathbb{P}\bigl(o \nleftrightarrow Y,\; o \leftrightarrow x,\; o \nleftrightarrow y \text{ for every } y \in A \text{ before } x\bigr)\, \mathbb{E}[F(C_x) \mid x \nleftrightarrow Y] \;\le\; \mathbb{E}[F(C_o);\; o \nleftrightarrow Y,\; o \leftrightarrow A]. \] Second, \(F(K)\) is replaced by \(F(K)\) minus the expectation of \(F\) at the cluster of \(a\) in the graph with every edge at a vertex of \(K\) removed; this new function is increasing in \(K\). Taking \(Y = \{a\}\) for the vertex \(a \in A\) minimising \(\mathbb{E}\,F(C_x)\) makes every conditional expectation on the left nonnegative, and the inequality becomes Conjecture 4 with the minimiser specified. The other conjectures and questions follow from that statement. For Conjecture 6 and Question 9 the cluster of \(o\) is replaced by the union of the clusters of a set of vertices: the union of the clusters of \(v\) and \(w\) does not depend on whether the edge \(\{v, w\}\) is open, and the cluster of \(o\) is the union of the clusters of \(o\) and of its open neighbours in the graph with the edges at \(o\) removed.

Implications

• The paper's chain of implications, Conjecture 4 to (3) to Conjecture 2 to Conjecture 1 to Conjecture 3 to \(\theta(p_c) = 0\), holds with every link proved, the last one in Anthropic's Lean proof.
• The vertex of \(A\) minimising \(\mathbb{P}(x \leftrightarrow b)\) is itself a valid choice in the pre-FKG comparison (Question 7), for every graph and every size of \(A\); so is the minimiser computed in the graph with the edges at \(o\) removed (Question 9).
• Conjecture 6 holds without its hypothesis (39), so the paper's Lemma 13 applies without it.
• The conditional comparison theorem for increasing functions of clusters remains valid with \(C_R=\bigcup_{r\in R}C_r\), for any finite set \(R\), in place of the single cluster \(C_o\); it also needs no sign condition on \(F\).

Files

How to check

lake exe cache get && lake build      # build Anthropic's Lean proof, as in its README
mkdir -p .lake/build/lib/lean/KN         # copy the .lean files to KN/, then:
for m in AvoidedDefs AvoidedPeelTools AvoidedClosure AvoidedGen AvoidedPeel AvoidedTransfer Projection Statements Conjectures ClusterProperty Statements6 Conjecture6Reduction PairSource GuardedDefs GuardedBasic GuardedKernel GuardedDecoy GuardedTwoCluster PairGuardedCSH PairSurplus PairSurplusClosure PairFixedMin Conjecture6Proof Question5Dual Question5 Question8Defs Question8Cases Question8Counterexample Question8Equivalence Question8Interior Question8Sufficient SourceGeneralCSH SourceSurplus SourceProjection Statements9 Question9Reduction Question9; do
  lake env lean -o .lake/build/lib/lean/KN/$m.olean -i .lake/build/lib/lean/KN/$m.ilean KN/$m.lean || break
done

Expected: the #print axioms lines of VERIFICATION.log, each [propext, Classical.choice, Quot.sound]. The sources of Anthropic's Lean proof can be checked first with shasum -a 256 -c conjecture-1/SOURCES.sha256 from its root.

All of this was done autonomously by ChatGPT 5.6 Sol and Claude Fable 5.1, with minimal human intervention. Released under the Apache License 2.0, the licence of Anthropic's Lean proof.