No percolation below the q = 2 random-cluster critical point

4 fully proved

A. Monotonicity of the percolation probability in p

LemmaWired box-boundary connection probability is monotone in \(p\) at \(q = 2\)#✓fully proved

For q = 2, the wired infinite-volume probability that the origin is connected to the boundary of the box of radius n is monotone in p.

lemma tzp_fkTheta_iv_monotone_boxBdry (n : ℕ) {p₁ p₂ : ℝ}
    (hp₁ : 0 < p₁) (hp₁' : p₁ < 1) (hp₂ : 0 < p₂) (hp₂' : p₂ < 1) (hle : p₁ ≤ p₂) :
    (wiredInfiniteVolume d hp₁ hp₁' (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxBdryConnEvent d n)
      ≤ (wiredInfiniteVolume d hp₂ hp₂' (by norm_num : (0 : ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real (boxBdryConnEvent d n)

Uses 26 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Event that the box origin connects to the box boundary · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice

Proof usesRandom-cluster probability with a boundary wiring · Boundary clique gives the wired random-cluster measure · Boundary-graph FK measure increases in \(p\) for \(q \ge 1\) · Vertex boundary of a box · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Monotonicity of restriction between boxes · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Wired infinite-volume measure as limit on increasing cylinder events · Origin-to-boundary connection is an increasing event · Wired random-cluster measure on a box · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired random-cluster probability of a configuration · Increasing event · Open connection of a vertex to the boundary · Origin as a vertex of the box graph · Complete graph on the boundary vertices · Box \((-n, n)^d\) in the hypercubic lattice · Boundary wiring relation

Used byMonotonicity of \(\theta^1(p, 2)\) in \(p\)

LemmaMonotonicity of \(\theta^1(p, 2)\) in \(p\)#✓fully proved

For q = 2, the wired percolation probability θ¹(p, 2) is monotone in p.

lemma tzp_fkTheta_monotone_in_p {p₁ p₂ : ℝ}
    (hp₁ : 0 < p₁) (hp₁' : p₁ < 1) (hp₂ : 0 < p₂) (hp₂' : p₂ < 1) (hle : p₁ ≤ p₂) :
    fkTheta d hp₁ hp₁' (by norm_num : (0 : ℝ) < 2) (q := 2)
      ≤ fkTheta d hp₂ hp₂' (by norm_num : (0 : ℝ) < 2) (q := 2)

Uses 7 · Used by 4

Statement usesWired random-cluster percolation probability \(\theta(p, q)\)

Proof usesConfiguration space of a statistical-mechanics model · Event that the box origin connects to the box boundary · Wired box-boundary connection probability is monotone in \(p\) at \(q = 2\) · Wired infinite-volume random-cluster measure · Wired infinite-volume boundary connection tends to \(\theta^1(p, q)\) · Site of the hypercubic lattice

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · No percolation below the critical point at \(q = 2\)

B. No percolation below the critical point

LemmaNo percolation below the critical point at \(q = 2\)#✓fully proved

For q = 2, there is no percolation below the critical point: θ¹(p, 2) = 0 for p < p_c(2, d).

lemma tzp_fkTheta_eq_zero_of_lt_pc {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hpc : p < FK.fkPc d 2) :
    FK.fkTheta d hp hp1 (by norm_num : (0 : ℝ) < 2) (q := 2) = 0

Uses 8 · Used by 4

Statement usesCritical parameter \(p_c(q)\) of the random-cluster model · Wired random-cluster percolation probability \(\theta(p, q)\)

Proof usesConfiguration space of a statistical-mechanics model · Non-percolating parameters of the wired random-cluster measure · Monotonicity of \(\theta^1(p, 2)\) in \(p\) · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice · Percolation event for the origin

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · No percolation for \(p \le p_c\) at \(q = 2\), given \(\theta^1(p_c, 2) = 0\)

LemmaNo percolation for \(p \le p_c\) at \(q = 2\), given \(\theta^1(p_c, 2) = 0\)#✓fully proved

For q = 2, if θ¹(p_c, 2) = 0, then θ¹(p, 2) = 0 for every p ≤ p_c(2, d).

lemma tzp_fkTheta_eq_zero_of_le_pc_of_pc
    (hθpc : ∀ (hp : 0 < FK.fkPc d 2) (hp1 : FK.fkPc d 2 < 1),
      FK.fkTheta d hp hp1 (by norm_num : (0 : ℝ) < 2) (q := 2) = 0) :
    ∀ (p : ℝ) (hp : 0 < p) (hp1 : p < 1), p ≤ FK.fkPc d 2 →
      FK.fkTheta d hp hp1 (by norm_num : (0 : ℝ) < 2) (q := 2) = 0

Uses 3

Statement usesCritical parameter \(p_c(q)\) of the random-cluster model · Wired random-cluster percolation probability \(\theta(p, q)\)

Proof usesNo percolation below the critical point at \(q = 2\)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.