# yaml-language-server: $schema=https://raw.githubusercontent.com/mathlib-initiative/formalization.yaml/main/schema/formalization.schema.json # formalization.yaml v0.4 -- Palomar registry metadata for this repository. version: "v0.4" project: name: "Percolation — θ(p_c) = 0 for Bernoulli bond percolation on ℤ^d in all dimensions d ≥ 2" # project folder `percolation/`; directory `percolation/` of anthropics/formal-math; Lake package PercolationContinuity, library Percolation # The concise public registry abstract (Palomar shows exactly this text). description: >- We prove θ(p_c) = 0 for nearest-neighbour Bernoulli bond percolation on ℤ^d for every dimension d ≥ 2: at the critical parameter the open cluster of the origin is almost surely finite (`Percolation.Continuity.CSH.percolationContinuity_allDimensions : ∀ d, 2 ≤ d → PercolationContinuity d`, in Lean 4 / Mathlib; comparator-checked over Mathlib-only definitions as `BondPercolation.percolation_continuity` and, for d = 3, `BondPercolation.percolation_continuity_Z3`). In particular this covers ℤ³, where it yields the classical corollary that p ↦ θ(p) is continuous on [0,1]; the formal statement is the vanishing of θ at p_c, and the classical equivalence with continuity on [0,1] is not itself part of the formal statement. The result was previously known for d = 2 (Harris, Kesten) and for d ≥ 11 (lace expansion); the cases 3 ≤ d ≤ 10 were open. The route is Kozma–Nitzan's reduction (arXiv:2401.12397): they conjectured gluing inequalities for percolation on arbitrary finite weighted graphs and proved (their Theorem 6) that the weakest of them, Conjecture 3, implies θ(p_c) = 0 on ℤ^d for all d ≥ 2. This development proves Conjecture 3 (`Percolation.Continuity.CSH.kozmaNitzan_conjecture3_holds`) through a stronger additive gluing inequality (`Percolation.Continuity.CSH.additiveGluing_holds`): if P(a ↔ b) ≥ 1 − t for every a ∈ A, then P(o ↔ b) ≥ P(o ↔ A) − t. Additive gluing is derived from a new conditioned slack hierarchy (`Percolation.Continuity.CSH.cshHolds`): 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, whose level-zero unconditioned case is the Harris inequality. Kozma–Nitzan's Theorem 6 and every classical input (Harris, van den Berg–Häggström–Kahn, the four functions theorem, Gladkov's decision-tree Harris–Kleitman inequality, the Barsky–Grimmett–Newman half-space theorem, Kesten's p_c(ℤ²) = 1/2) are re-proved in the library from Mathlib, so the statement has no hypothesis other than 2 ≤ d. Kozma–Nitzan's Conjectures 1, 2 and 4 are neither proved nor stated; nothing new is claimed about slabs, site percolation or other lattices. All main theorems depend only on propext, Classical.choice and Quot.sound; there is no sorry outside the two deliberate placeholders of the statement file Challenge.lean and no added axiom. The work has not yet been refereed by anyone independent of the author; correctness rests on the mechanical checks recorded in AUDIT.md, and readers should check that Challenge.lean states the intended theorem. # Required nonempty list of name strings (human authors). authors: - "Justin Leder" license: "Apache-2.0" responsible_maintainers: - "Justin Leder" # GitHub: jleder3 # `repository` is omitted: this directory contains the substantive proof development (it is not a # thin Comparator wrapper around another formalization). classification: arxiv: [math.PR, math.CO] msc2020: ["60K35", "82B43"] sources: - title: "theta(p_c) = 0 for nearest-neighbour Bernoulli bond percolation on Z^d for every d >= 2, via a proof of the Kozma-Nitzan gluing inequalities (the conditioned slack hierarchy)" type: original-proof relationship: other note: >- First presented by this formalization (2026). An informal proof sketch (summary.pdf, LaTeX source summary.tex) accompanies the formalization; there is no refereed paper or arXiv identifier yet. author_endorsement: n/a - title: "A reduction of the theta(p_c)=0 problem to a conjectured inequality" authors: ["Gady Kozma", "Shahaf Nitzan"] id: "arXiv:2401.12397v1" type: paper year: 2024 relationship: background note: >- Source of the statement of the near-one gluing inequality (their Conjecture 3) and of the reduction Theorem 6 (Conjecture 3 implies theta(p_c) = 0 on Z^d, d >= 2). The library PROVES Conjecture 3 (new, via the additive gluing inequality) and re-proves Theorem 6 and the paper's own Theorems 1, 3, 4, 7, 8 in Lean following Sections 2-4; nothing from the paper is assumed. author_endorsement: not-contacted - title: "Some conditional correlation inequalities for percolation and related processes" authors: ["J. van den Berg", "O. Haggstrom", "J. Kahn"] id: "doi:10.1002/rsa.20102" type: paper year: 2006 relationship: background note: "Conditional association inequalities (Thms 1.3-1.5) used as inputs of the hierarchy; re-proved in the library." - title: "Percolation inequalities and decision trees" authors: ["Nikita Gladkov"] id: "arXiv:2408.08457v2" type: paper year: 2024 relationship: background note: "Decision-tree Harris-Kleitman inequality (Thm 3.2) used as an input of the hierarchy; re-proved in the library." - title: "Inequalities for connectivity events in Bernoulli percolation (Ph.D. thesis, UCLA)" authors: ["Nikita Gladkov"] id: "https://escholarship.org/uc/item/4h82d4n1" type: thesis year: 2025 relationship: background note: "Chapter 5 (Harris-Kleitman type inequalities, with A. Zimin): the kernel lemmas Thm 5.2.1, Cor 5.2.2, Thm 5.2.3 are re-proved in Percolation/Literature/GladkovZiminKernel.lean as inputs of the hierarchy." - title: "Absence of infinite cluster for critical Bernoulli percolation on slabs" authors: ["Hugo Duminil-Copin", "Vladas Sidoravicius", "Vincent Tassion"] id: "arXiv:1401.7130" type: paper year: 2016 relationship: background note: "Slab theorem (Thm 1: no infinite cluster on a slab of Z^3 at the slab's own critical point) re-proved in the library as a literature input (DuminilCopinSidoraviciusTassion2016_holds); nothing new about slabs is claimed." - title: "Percolation in half-spaces: equality of critical densities and continuity of the percolation probability" authors: ["David J. Barsky", "Geoffrey R. Grimmett", "Charles M. Newman"] id: "doi:10.1007/BF01321136" type: paper year: 1991 relationship: background note: "Half-space theorem (no percolation in a half-space at its critical point) invoked by the Kozma-Nitzan reduction; re-proved in the library." - title: "A lower bound for the critical probability in a certain percolation process" authors: ["T. E. Harris"] id: "doi:10.1017/S0305004100034241" type: paper year: 1960 relationship: background note: "theta(1/2) = 0 on Z^2 and the Harris(-FKG) inequality; re-proved in the library (d = 2 case)." - title: "The critical probability of bond percolation on the square lattice equals 1/2" authors: ["Harry Kesten"] id: "doi:10.1007/BF01197577" type: paper year: 1980 relationship: background note: "p_c(Z^2) = 1/2; re-proved in the library (d = 2 case)." - title: "Percolation (2nd edition)" authors: ["Geoffrey Grimmett"] id: "doi:10.1007/978-3-662-03981-6" type: book year: 1999 relationship: background note: "Definitions of the model, theta and p_c (Sections 1.3-1.4) followed by Challenge.lean; statement of the open problem (pp. 14, 202-203)." - title: "Mean-field behavior for nearest-neighbor percolation in d > 10" authors: ["Robert Fitzner", "Remco van der Hofstad"] id: "doi:10.1214/17-EJP56" type: paper year: 2017 relationship: background note: "Prior state of the art: theta(p_c) = 0 for d >= 11 by the lace expansion (Hara-Slade 1990 for d >= 19). Not used in the proof." - title: "Sixty years of percolation" authors: ["Hugo Duminil-Copin"] id: "doi:10.1142/9789813272880_0162" type: paper year: 2018 relationship: background note: "ICM survey; Conjecture 1 there is the statement proved here for d >= 3. Not used in the proof." related_formalizations: [] status: scope: >- Formalized and compared: theta(p_c) = 0 for nearest-neighbour Bernoulli BOND percolation on Z^d, for every d >= 2 (BondPercolation.percolation_continuity) and for d = 3 (BondPercolation.percolation_continuity_Z3), with p_c defined as an infimum (see fidelity). Also proved in the library but NOT among the compared declarations: Kozma-Nitzan's Conjecture 3 and the additive gluing inequality on finite weighted graphs, the conditioned slack hierarchy, Kozma-Nitzan's Theorem 6, the Barsky-Grimmett-Newman half-space theorem, Kesten's p_c(Z^2) = 1/2. Nothing new is claimed about site percolation, other lattices or slabs (the Duminil-Copin- Sidoravicius-Tassion slab theorem is formalized, as a literature input), continuity of theta as a function on [0,1] (equivalent by standard facts that are not part of the compared statement), or quantitative bounds on theta near p_c. Kozma-Nitzan's Conjecture 3 is obtained through the stronger ADDITIVE gluing inequality; their Conjectures 1 (multiplicative form), 2 and 4 are not addressed. Nothing is conditional: no extra hypotheses, no axioms beyond the three standard ones. sorry_count: 0 # the library, Solution.lean; Challenge.lean carries the 2 placeholder proofs of the trusted statement file by design sorry_in_definitions: 0 axioms: [propext, Classical.choice, Quot.sound] main_results: - declaration: "BondPercolation.percolation_continuity" file: "Solution.lean" sorry_count: 0 axioms: [propext, Classical.choice, Quot.sound] comparator_config: "comparator.json" - declaration: "BondPercolation.percolation_continuity_Z3" file: "Solution.lean" sorry_count: 0 axioms: [propext, Classical.choice, Quot.sound] comparator_config: "comparator.json" - declaration: "Percolation.Continuity.CSH.percolationContinuity_allDimensions" file: "Percolation/Continuity/MainTheorem.lean" sorry_count: 0 axioms: [propext, Classical.choice, Quot.sound] - declaration: "Percolation.Continuity.CSH.kozmaNitzan_conjecture3_holds" file: "Percolation/Continuity/MainTheorem.lean" sorry_count: 0 axioms: [propext, Classical.choice, Quot.sound] automation: methods: - method: autonomous models: ["Claude"] framework: "n/a" tool_setup: >- The Lean development (definitions, statements and proofs, including Challenge.lean and Solution.lean) was produced by large-language-model agents (Anthropic's Claude) iterating against the Lean compiler and the pinned Mathlib, under human direction; no human wrote or edited Lean source. The statement file Challenge.lean, the README and this metadata file were read by the responsible author before submission. Everything is machine-checked by the Lean kernel; the compared theorems additionally by the Palomar Comparator with the independent nanoda kernel (see AUDIT.md). cost: wall_time: "about one week (August 2026)" spend_usd: "not tracked" hardware: "cloud CPU machines for Lean elaboration; API inference" prompting_notes: "The responsible author posed the problem, set the acceptance standard (kernel-checked proof with the standard axioms, plus adversarial review of the statements) and directed priorities." spend_usd: "not tracked" notes: >- Discovery, informal proof and Lean formalization were all produced by the AI system operating autonomously. Human role (Justin Leder): problem selection, direction, reading of the statement file and metadata, and responsibility for this submission. fidelity: divergences: >- (1) p_c is defined as inf({p in [0,1] : theta_0(p) > 0} U {1}) rather than the textbook sup{p : theta(p) = 0}; the two agree because theta is non-decreasing (standard; the U {1} only fixes the degenerate case theta == 0, where it gives p_c = 1 instead of the real-number junk value inf(empty) = 0). (2) "Percolation" is the event that the open cluster of the origin is an infinite set of vertices (Grimmett's {|C| = infinity}); theta is its probability as a real number (Measure.real). (3) The nearest-neighbour graph on Z^d is encoded as Mathlib's Hasse diagram of the coordinatewise order on Fin d -> Z, which is exactly the graph with edges x ~ x +/- e_i. (4) Bond configurations are arbitrary subsets of Sym2(Z^d); under the measure, pairs that are not lattice edges are almost surely closed. (5) Only d >= 2 is claimed (for d = 1 the statement is false: p_c = 1 and theta(1) = 1). (6) Kozma-Nitzan is an arXiv preprint (v1); its Theorem 6 is re-proved in Lean here, so the result does not depend on the preprint's correctness. No other divergences known. review: status: "self-assessed" # not yet reviewed by anyone independent of the author; no human peer review reviewers: - "none independent of the author (AI review and mechanical checks only, August 2026)" notes: >- Not independently peer-reviewed. Performed before submission, by AI systems plus mechanical replays: line-by-line faithfulness check of the literature statements re-proved along the proof chain against the cited sources; scan of the sources for sorry/axiom/unsafe/native_decide/implemented_by (none); #print axioms = {propext, Classical.choice, Quot.sound} for the main theorems and both compared theorems; clean rebuilds (Lean leanprover/lean4:v4.32.0); independent-kernel replay with nanoda via the comparator. NOT performed: any review by a human mathematician or by anyone independent of the author; readers should independently check that Challenge.lean states the intended theorem. See README.md "Provenance and review status" and AUDIT.md. alignment: namespace: "BondPercolation" statements: - source: "Grimmett 1999, Sections 1.3-1.4: bond percolation measure P_p, open cluster C(x), theta(p) = P_p(|C| = infinity) (1.9), p_c (1.11)" lean: "BondPercolation.bondPercolation, BondPercolation.openCluster, BondPercolation.theta, BondPercolation.criticalProb" module: "Challenge" status: "definitions, verbatim copies of the library's Percolation.Literature.*" note: "p_c as an infimum with the U {1} convention; see fidelity (1)." - source: "Duminil-Copin ICM 2018 Conjecture 1 / Grimmett 1999 pp. 14, 202-203: theta(p_c) = 0 on Z^d, d >= 3 (d = 2 known)" lean: "BondPercolation.percolation_continuity" module: "Solution" status: "proved for all d >= 2" note: "Transported by definitional unfolding (Iff.rfl) from Percolation.Continuity.CSH.percolationContinuity_allDimensions (247-module library `Percolation`)." - source: "same, d = 3" lean: "BondPercolation.percolation_continuity_Z3" module: "Solution" status: "proved" note: "Special case d = 3 of the previous entry." acknowledgements: "Lean 4 and Mathlib (leanprover-community); leanprover/comparator, lean4export and nanoda for independent checking; the Palomar template."