Uniqueness of the infinite cluster

DefinitionConfiguration with all edges at a site closed#✓fully proved

The configuration obtained from ω by closing every edge incident to x.

noncomputable def removeSite (x : Site d) (ω : ConfigSpace (Sym2 (Site d))) :
    ConfigSpace (Sym2 (Site d)) :=
  fun e => if x ∈ e then false else ω e

Uses 2 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice

Used byTrifurcation point, without requiring infinite branches

DefinitionTrifurcation point, without requiring infinite branches#✓fully proved

x is connected to three distinct sites with infinite ω-clusters that are pairwise disconnected after removing x. Unlike the classical definition, the three branches at x are not required to be infinite.

def IsTrifurcation (d : ℕ) (ω : ConfigSpace (Sym2 (Site d))) (x : Site d) : Prop :=
  ∃ a₁ a₂ a₃ : Site d,
    (a₁ ≠ a₂ ∧ a₁ ≠ a₃ ∧ a₂ ≠ a₃) ∧
    (Connected d ω x a₁ ∧ Connected d ω x a₂ ∧ Connected d ω x a₃) ∧
    ((cluster d ω a₁).Infinite ∧ (cluster d ω a₂).Infinite ∧ (cluster d ω a₃).Infinite) ∧
    (¬ Connected d (removeSite x ω) a₁ a₂ ∧
      ¬ Connected d (removeSite x ω) a₁ a₃ ∧
      ¬ Connected d (removeSite x ω) a₂ a₃)

Uses 5 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Connection by an open path · Site of the hypercubic lattice · Open cluster of a site · Configuration with all edges at a site closed

Used byNumber of trifurcation points in a box

DefinitionSites of a box as a finite set#✓fully proved

The sites of the box Λ_n as a finset.

noncomputable def boxFinsetBK (d n : ℕ) : Finset (Site d) := (box_finite d n).toFinset

Uses 2 · Used by 1

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byNumber of trifurcation points in a box

DefinitionNumber of trifurcation points in a box#✓fully proved

The number of trifurcation points of ω in the box Λ_n.

noncomputable def Tcount (d : ℕ) (ω : ConfigSpace (Sym2 (Site d))) (n : ℕ) : ℕ :=
  ((boxFinsetBK d n).filter (fun x => IsTrifurcation d ω x)).card

Uses 4

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Trifurcation point, without requiring infinite branches · Sites of a box as a finite set

TheoremBurton–Keane theorem#●ready to prove

Burton–Keane theorem for Bernoulli bond percolation. For every dimension d and every p ∈ [0, 1], almost surely under the Bernoulli(p) bond percolation measure on ℤ^d there is at most one infinite open cluster.

public theorem_wanted burton_keane_bernoulli :
    ∀ (d : ℕ) (p : ℝ≥0) (hp : p ≤ 1),
      ∀ᵐ ω ∂(bernoulliProductMeasure (E := Sym2 (Lattice.Site d)) p hp),
        numInfiniteClusters d ω ≤ 1

Sources

• R. M. Burton, M. Keane, Density and uniqueness in percolation, Comm. Math. Phys. 121 (1989), 501–505.

Uses 4

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Number of infinite open clusters · Bernoulli product measure on configuration space

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.