The random-cluster critical point on ℤ² is below one, given a Peierls bound

25 fully proved

A. Walks to the exterior of a finite cluster

DefinitionHorizontal lattice walk in \(\mathbb{Z}^2\)#✓fully proved

The horizontal lattice walk of k steps from (a, c) to (a + k, c) in ℤ².

noncomputable def horizWalk (c : ℤ) :
    (k : ℕ) → (a : ℤ) → (hypercubicLattice 2).Walk ![a, c] ![a + (k : ℤ), c]
  | 0, a => by
      simpa using (SimpleGraph.Walk.nil : (hypercubicLattice 2).Walk ![a, c] ![a, c])
  | k + 1, a => by
      have step : (hypercubicLattice 2).Adj ![a, c] ![a + 1, c] := latAdj_right a c
      have rest := horizWalk c k (a + 1)
      have he : (![a + 1 + (k : ℤ), c] : Site 2) = ![a + ((k + 1 : ℕ) : ℤ), c] := by
        funext i; fin_cases i <;> (simp; try ring)
      rw [he] at rest
      exact SimpleGraph.Walk.cons step rest

Uses 2 · Used by 1

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used byFinite cluster in \(\mathbb{Z}^2\) has a reachable point outside it

LemmaFinite subsets of \(\mathbb{Z}^2\) miss far points on each row#✓fully proved

A finite set of ℤ² misses some point (N, c) with N ≥ a₀ on every horizontal line.

lemma exists_far_not_mem (S : Set (Site 2)) (hfin : S.Finite) (c a0 : ℤ) :
    ∃ N : ℤ, a0 ≤ N ∧ (![N, c] : Site 2) ∉ S

Uses 1 · Used by 1

Statement usesSite of the hypercubic lattice

Used byFinite cluster in \(\mathbb{Z}^2\) has a reachable point outside it

LemmaFinite cluster in \(\mathbb{Z}^2\) has a reachable point outside it#✓fully proved

A finite cluster of o has a lattice-reachable point outside it.

lemma exists_walk_exterior {ω : ConfigSpace (Sym2 (Site 2))} (o : Site 2)
    (hfin : (cluster 2 ω o).Finite) :
    ∃ z : Site 2, (hypercubicLattice 2).Reachable o z ∧ z ∉ cluster 2 ω o

Uses 6 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Open cluster of a site · Hypercubic lattice \(\mathbb{Z}^d\)

Proof usesFinite subsets of \(\mathbb{Z}^2\) miss far points on each row · Horizontal lattice walk in \(\mathbb{Z}^2\)

Used byFinite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit · Finite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings

B. Closed circuits around a finite cluster

DefinitionClosed-circuit event of a dual circuit#✓fully proved

The event that every primal edge crossed by the dual circuit c is closed.

def closedCircuitEvent {u : Site 2} (c : (hypercubicLattice 2).Walk u u) :
    Set (ConfigSpace (Sym2 (Site 2))) :=
  {ω | ∀ f g : Site 2, s(f, g) ∈ c.edges → ω (sharedPrimalEdge f g) = false}

Uses 4 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Primal edge shared by adjacent faces

Used byFinite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit · Finite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings · Finite-cluster event is covered by closed-circuit events

LemmaFinite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit#✓fully proved

A finite open cluster of o in ℤ² is surrounded by a lattice cycle whose crossed primal edges are all closed.

lemma exists_closed_latticeCircuit_of_finite_cluster
    {ω : ConfigSpace (Sym2 (Site 2))} (o : Site 2) (hfin : (cluster 2 ω o).Finite) :
    ∃ (u : Site 2) (c : (hypercubicLattice 2).Walk u u), c.IsCycle ∧
      ω ∈ closedCircuitEvent c

Uses 25 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Closed-circuit event of a dual circuit · Site of the hypercubic lattice · Open cluster of a site · Hypercubic lattice \(\mathbb{Z}^d\)

Proof usesFinite cluster in \(\mathbb{Z}^2\) has a reachable point outside it · Connection by an open path · Every edge of a finite even-degree graph lies on a cycle · Open lattice edge of a bond configuration · Nearest neighbours in \(\mathbb{Z}^d\) · Boundary edge of a set · Boundary indicator of an edge · Nearest neighbours of a lattice site · Neighbour of a site in a coordinate direction · Four unit faces at a lattice site · Edge boundary of a set of sites · Boundary degree of a unit face · Face-boundary graph of a set · Lower left corner of the unit face at \((a, b)\) · Upper left corner of the unit face at \((a, b)\) · Lower right corner of the unit face at \((a, b)\) · Upper right corner of the unit face at \((a, b)\) · Open subgraph of a bond configuration · Primal edge shared by adjacent faces · Shift of a site along a coordinate

Used byFinite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings · Finite-cluster event is covered by closed-circuit events

LemmaFinite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings#✓fully proved

The closed circuit of exists_closed_latticeCircuit_of_finite_cluster, together with a point that the cluster boundary separates from o and an odd crossing number for every walk to it.

lemma exists_enclosing_closed_latticeCircuit_of_finite_cluster
    {ω : ConfigSpace (Sym2 (Site 2))} (o : Site 2) (hfin : (cluster 2 ω o).Finite) :
    ∃ z : Site 2,
      (∃ (u : Site 2) (c : (hypercubicLattice 2).Walk u u), c.IsCycle ∧ ω ∈ closedCircuitEvent c)
        ∧ ¬ (latticeMinusBarrier (cluster 2 ω o)).Reachable o z
        ∧ ∀ γ : (hypercubicLattice 2).Walk o z, ¬ Even (crossCount (cluster 2 ω o) γ)

Uses 27

Statement usesConfiguration space of a statistical-mechanics model · Closed-circuit event of a dual circuit · Site of the hypercubic lattice · Open cluster of a site · Number of boundary crossings of a walk · Hypercubic lattice \(\mathbb{Z}^d\) · Square lattice with the boundary edges of a set removed

Proof usesFinite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit · Finite cluster in \(\mathbb{Z}^2\) has a reachable point outside it · Connection by an open path · Every edge of a finite even-degree graph lies on a cycle · Nearest neighbours in \(\mathbb{Z}^d\) · Boundary edge of a set · Boundary indicator of an edge · Nearest neighbours of a lattice site · Neighbour of a site in a coordinate direction · Four unit faces at a lattice site · Edge boundary of a set of sites · Boundary degree of a unit face · Face-boundary graph of a set · Lower left corner of the unit face at \((a, b)\) · Upper left corner of the unit face at \((a, b)\) · Lower right corner of the unit face at \((a, b)\) · Upper right corner of the unit face at \((a, b)\) · Open subgraph of a bond configuration · Primal edge shared by adjacent faces · Shift of a site along a coordinate

LemmaFinite-cluster event is covered by closed-circuit events#✓fully proved

The event that the cluster of o is finite is covered by the closed-circuit events.

lemma finiteCluster_subset_iUnion_closedCircuit (o : Site 2) :
    {ω : ConfigSpace (Sym2 (Site 2)) | (cluster 2 ω o).Finite}
      ⊆ ⋃ (u : Site 2) (c : (hypercubicLattice 2).Walk u u) (_ : c.IsCycle),
          closedCircuitEvent c

Uses 6

Statement usesConfiguration space of a statistical-mechanics model · Closed-circuit event of a dual circuit · Site of the hypercubic lattice · Open cluster of a site · Hypercubic lattice \(\mathbb{Z}^d\)

Proof usesFinite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit

LemmaNon-percolation means the origin's cluster is finite#✓fully proved

No percolation from the origin means the cluster of the origin is finite.

lemma compl_percolationEvent_eq_finiteCluster :
    (percolationEvent 2)ᶜ
      = {ω : ConfigSpace (Sym2 (Site 2)) | (cluster 2 ω (origin 2)).Finite}

Uses 5

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Open cluster of a site · Origin of the hypercubic lattice · Percolation event for the origin

C. The Peierls series

DefinitionPeierls series \(\sum_\ell \ell\,(2d)^\ell (1-p)^\ell\)#✓fully proved

The Peierls series Σ_ℓ ℓ (2d)^ℓ (1 - p)^ℓ bounding the probability of a finite cluster.

noncomputable def fkPcUpperBound (d : ℕ) (p : ℝ) : ℝ :=
  ∑' ℓ : ℕ, (ℓ : ℝ) * (2 * d : ℝ) ^ ℓ * (1 - p) ^ ℓ

Used by 8

Used byPeierls series is below 1 on an interval \((p_0, 1)\) · Peierls bound hypothesis for the wired measure on \(\mathbb{Z}^2\) · \(p_c(q) < 1\) on \(\mathbb{Z}^2\) for \(q \ge 1\) under a Peierls bound · Closed form \(x/(1-x)^2\) of the Peierls series for \(|x| < 1\) · Nonnegativity of the Peierls series for \(p \le 1\) · Peierls series tends to \(0\) as \(p \to 1\) · Peierls series for \(d = 2\) equals the Bernoulli Peierls series · Percolation from a Peierls bound with series below 1

DefinitionRatio \(2d(1-p)\) of the Peierls series#✓fully proved

The ratio 2d (1 - p) of the Peierls series.

noncomputable def fkPcRatio (d : ℕ) (p : ℝ) : ℝ := (2 * d : ℝ) * (1 - p)

Used by 5

Used byDefining formula for the Peierls ratio · Peierls ratio \(2d(1-p)\) tends to \(0\) as \(p \to 1\) · Peierls summand as \(\ell x^\ell\) with \(x = 2d(1-p)\) · Closed form \(x/(1-x)^2\) of the Peierls series for \(|x| < 1\) · Peierls series tends to \(0\) as \(p \to 1\)

LemmaDefining formula for the Peierls ratio#✓fully proved

Unfolding fkPcRatio.

@[simp] lemma fkPcRatio_def (d : ℕ) (p : ℝ) : fkPcRatio d p = (2 * d : ℝ) * (1 - p)

Uses 1 · Used by 1

Statement usesRatio \(2d(1-p)\) of the Peierls series

Used byPeierls summand as \(\ell x^\ell\) with \(x = 2d(1-p)\)

LemmaPeierls summand as \(\ell x^\ell\) with \(x = 2d(1-p)\)#✓fully proved

The Peierls summand in terms of fkPcRatio.

lemma fkPcSummand_eq (d : ℕ) (p : ℝ) (ℓ : ℕ) :
    (ℓ : ℝ) * (2 * d : ℝ) ^ ℓ * (1 - p) ^ ℓ = (ℓ : ℝ) * (fkPcRatio d p) ^ ℓ

Uses 2 · Used by 1

Statement usesRatio \(2d(1-p)\) of the Peierls series

Proof usesDefining formula for the Peierls ratio

Used byClosed form \(x/(1-x)^2\) of the Peierls series for \(|x| < 1\)

LemmaClosed form \(x/(1-x)^2\) of the Peierls series for \(|x| < 1\)#✓fully proved

Closed form x / (1 - x)² of the Peierls series for |x| < 1, where x = 2d (1 - p).

lemma fkPcUpperBound_eq_closedForm (d : ℕ) (p : ℝ) (hx : ‖fkPcRatio d p‖ < 1) :
    fkPcUpperBound d p = (fkPcRatio d p) / (1 - fkPcRatio d p) ^ 2

Uses 3 · Used by 1

Statement usesRatio \(2d(1-p)\) of the Peierls series · Peierls series \(\sum_\ell \ell\,(2d)^\ell (1-p)^\ell\)

Proof usesPeierls summand as \(\ell x^\ell\) with \(x = 2d(1-p)\)

Used byPeierls series tends to \(0\) as \(p \to 1\)

LemmaPeierls ratio \(2d(1-p)\) tends to \(0\) as \(p \to 1\)#✓fully proved

2d (1 - p) → 0 as p → 1.

lemma fkPcRatio_tendsto_one (d : ℕ) :
    Tendsto (fun p : ℝ => fkPcRatio d p) (nhds 1) (nhds 0)

Uses 1 · Used by 1

Statement usesRatio \(2d(1-p)\) of the Peierls series

Used byPeierls series tends to \(0\) as \(p \to 1\)

Lemma\(x/(1-x)^2 \to 0\) as \(x \to 0\)#✓fully proved

x / (1 - x)² → 0 as x → 0.

lemma fkPcClosedForm_tendsto_zero :
    Tendsto (fun x : ℝ => x / (1 - x) ^ 2) (nhds 0) (nhds 0)

Used by 1

Used byPeierls series tends to \(0\) as \(p \to 1\)

LemmaPeierls series tends to \(0\) as \(p \to 1\)#✓fully proved

The Peierls series tends to 0 as p → 1.

lemma fkPcUpperBound_tendsto_one (d : ℕ) :
    Tendsto (fun p : ℝ => fkPcUpperBound d p) (nhds 1) (nhds 0)

Uses 5 · Used by 1

Statement usesPeierls series \(\sum_\ell \ell\,(2d)^\ell (1-p)^\ell\)

Proof uses\(x/(1-x)^2 \to 0\) as \(x \to 0\) · Ratio \(2d(1-p)\) of the Peierls series · Peierls ratio \(2d(1-p)\) tends to \(0\) as \(p \to 1\) · Closed form \(x/(1-x)^2\) of the Peierls series for \(|x| < 1\)

Used byPeierls series is below 1 on an interval \((p_0, 1)\)

LemmaPeierls series is below 1 on an interval \((p_0, 1)\)#✓fully proved

The Peierls series is below 1 on an interval (p₀, 1].

lemma exists_p_lt_one_fkPcUpperBound_lt_one (d : ℕ) :
    ∃ p₀ : ℝ, p₀ < 1 ∧ ∀ p : ℝ, p₀ < p → p ≤ 1 → fkPcUpperBound d p < 1

Uses 2 · Used by 1

Statement usesPeierls series \(\sum_\ell \ell\,(2d)^\ell (1-p)^\ell\)

Proof usesPeierls series tends to \(0\) as \(p \to 1\)

Used by\(p_c(q) < 1\) on \(\mathbb{Z}^2\) for \(q \ge 1\) under a Peierls bound

LemmaNonnegativity of the Peierls series for \(p \le 1\)#✓fully proved

The Peierls series is nonnegative for p ≤ 1.

lemma fkPcUpperBound_nonneg (d : ℕ) {p : ℝ} (hp : p ≤ 1) : 0 ≤ fkPcUpperBound d p

Uses 1

Statement usesPeierls series \(\sum_\ell \ell\,(2d)^\ell (1-p)^\ell\)

D. The critical point is below one

DefinitionPeierls bound hypothesis for the wired measure on \(\mathbb{Z}^2\)#✓fully proved

The Peierls bound for the wired random-cluster measure on ℤ² at (p, q): 1 - θ¹(p, q) ≤ Σ_ℓ ℓ 4^ℓ (1 - p)^ℓ.

def FkNonPercolationBound (q : ℝ) {p : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) : Prop :=
  1 - fkTheta 2 hp hp1 hq (q := q) ≤ fkPcUpperBound 2 p

Uses 2 · Used by 3

Statement usesPeierls series \(\sum_\ell \ell\,(2d)^\ell (1-p)^\ell\) · Wired random-cluster percolation probability \(\theta(p, q)\)

Used by\(p_c(q) < 1\) on \(\mathbb{Z}^2\) for \(q \ge 1\) under a Peierls bound · \(0 < p_c(q) < 1\) on \(\mathbb{Z}^2\) for \(q \ge 1\) under a Peierls bound · Percolation from a Peierls bound with series below 1

LemmaPercolation from a Peierls bound with series below 1#✓fully proved

The Peierls bound with a series below 1 gives percolation: 0 < θ¹(p, q).

lemma fkTheta_pos_of_nonPercolationBound {q : ℝ} {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hq : 0 < q) (hBound : FkNonPercolationBound q hp hp1 hq)
    (hsum : fkPcUpperBound 2 p < 1) :
    0 < fkTheta 2 hp hp1 hq (q := q)

Uses 3 · Used by 1

Statement usesPeierls bound hypothesis for the wired measure on \(\mathbb{Z}^2\) · Peierls series \(\sum_\ell \ell\,(2d)^\ell (1-p)^\ell\) · Wired random-cluster percolation probability \(\theta(p, q)\)

Used by\(p_c(q) < 1\) on \(\mathbb{Z}^2\) for \(q \ge 1\) under a Peierls bound

LemmaNonempty subcritical set on \(\mathbb{Z}^2\) for \(q \ge 1\)#✓fully proved

For q ≥ 1 the subcritical set on ℤ² is nonempty (it contains 1/8).

lemma fkSubcriticalSet_nonempty {q : ℝ} (hq : 1 ≤ q) : (fkSubcriticalSet 2 q).Nonempty

Uses 3 · Used by 2

Statement usesNon-percolating parameters of the wired random-cluster measure

Proof usesWired random-cluster percolation probability \(\theta(p, q)\) · No wired percolation for \(2dp < 1\) and \(q \ge 1\)

Used by\(p_c(q)\) equals the self-dual point if percolation starts there, \(q \ge 1\) · \(p_c(q) < 1\) on \(\mathbb{Z}^2\) for \(q \ge 1\) under a Peierls bound

LemmaPositive percolation probability rules out subcriticality#✓fully proved

A parameter with positive percolation probability is not subcritical.

lemma not_mem_fkSubcriticalSet_of_fkTheta_pos {q : ℝ} {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hq : 0 < q) (hθ : 0 < fkTheta 2 hp hp1 hq (q := q)) : p ∉ fkSubcriticalSet 2 q

Uses 2 · Used by 2

Statement usesNon-percolating parameters of the wired random-cluster measure · Wired random-cluster percolation probability \(\theta(p, q)\)

Used by\(p_c(q)\) equals the self-dual point if percolation starts there, \(q \ge 1\) · \(p_c(q) < 1\) on \(\mathbb{Z}^2\) for \(q \ge 1\) under a Peierls bound

Lemma\(p_c(q) < 1\) on \(\mathbb{Z}^2\) for \(q \ge 1\) under a Peierls bound#✓fully proved

For q ≥ 1, the random-cluster critical point on ℤ² satisfies p_c(q) < 1, assuming the Peierls bound FkNonPercolationBound for all p in some interval (p₀, 1).

lemma fkPc_lt_one {q : ℝ} (hq : 1 ≤ q)
    (hGeom : ∃ p₀ : ℝ, p₀ < 1 ∧
      ∀ (p : ℝ) (hp : 0 < p) (hp1 : p < 1), p₀ < p →
        FkNonPercolationBound q hp hp1 (zero_lt_one.trans_le hq)) :
    fkPc 2 q < 1

Uses 9 · Used by 1

Statement usesPeierls bound hypothesis for the wired measure on \(\mathbb{Z}^2\) · Critical parameter \(p_c(q)\) of the random-cluster model

Proof usesPeierls series is below 1 on an interval \((p_0, 1)\) · Peierls series \(\sum_\ell \ell\,(2d)^\ell (1-p)^\ell\) · Non-percolating parameters of the wired random-cluster measure · Nonempty subcritical set on \(\mathbb{Z}^2\) for \(q \ge 1\) · Wired random-cluster percolation probability \(\theta(p, q)\) · Percolation from a Peierls bound with series below 1 · Positive percolation probability rules out subcriticality

Used by\(0 < p_c(q) < 1\) on \(\mathbb{Z}^2\) for \(q \ge 1\) under a Peierls bound

Lemma\(0 < p_c(q) < 1\) on \(\mathbb{Z}^2\) for \(q \ge 1\) under a Peierls bound#✓fully proved

For q ≥ 1, 0 < p_c(q) < 1 on ℤ², assuming the Peierls bound as in fkPc_lt_one.

lemma fkPc_pos_and_lt_one {q : ℝ} (hq : 1 ≤ q)
    (hGeom : ∃ p₀ : ℝ, p₀ < 1 ∧
      ∀ (p : ℝ) (hp : 0 < p) (hp1 : p < 1), p₀ < p →
        FkNonPercolationBound q hp hp1 (zero_lt_one.trans_le hq)) :
    0 < fkPc 2 q ∧ fkPc 2 q < 1

Uses 4

Statement usesPeierls bound hypothesis for the wired measure on \(\mathbb{Z}^2\) · Critical parameter \(p_c(q)\) of the random-cluster model

Proof uses\(p_c(q) < 1\) on \(\mathbb{Z}^2\) for \(q \ge 1\) under a Peierls bound · Positive random-cluster critical point for \(d \ge 2\), \(q \ge 1\)

LemmaPeierls series for \(d = 2\) equals the Bernoulli Peierls series#✓fully proved

The Peierls series for d = 2 is the Bernoulli Peierls series StatMech.Percolation.pcUpperBound.

lemma fkPcUpperBound_two_eq_pcUpperBound (p : ℝ) :
    fkPcUpperBound 2 p = Percolation.pcUpperBound p

Uses 2

Statement usesPeierls series \(\sum_\ell \ell\,(2d)^\ell (1-p)^\ell\) · Peierls series bounding closed dual circuits

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.