First-order transitions of the random-cluster model

9 fully proved

A. The free percolation probability

DefinitionFree percolation probability#✓fully proved

The free percolation probability θ⁰(p, q): the free infinite-volume measure of the event that the origin lies in an infinite open cluster.

noncomputable def fkThetaFree (d : ℕ) {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) : ℝ :=
  ((freeInfiniteVolume d hp hp1 hq : ProbabilityMeasure (ConfigSpace (Sym2 (Site d)))) :
      Measure (ConfigSpace (Sym2 (Site d)))).real (percolationEvent d)

Uses 4 · Used by 10

Statement usesConfiguration space of a statistical-mechanics model · Free infinite-volume random-cluster measure · Site of the hypercubic lattice · Percolation event for the origin

Used byFirst-order transition from \(\theta^0 = 0\) and \(\theta^1 > 0\) · Free percolation probability is at most one · \(\theta^0 \ne \theta^1\) at a first-order transition · Nonnegativity of the free percolation probability · Free and wired measures differ at a first-order transition · First-order transition of the random-cluster model · Free and wired measures differ at self-dual \(p\) for \(q > 4\) if first order · Free and wired measures differ at \(\sqrt{q}/(1+\sqrt{q})\) for \(q > 4\) if first order · Free percolation from domination and free–wired agreement at \(p'\) · Free percolation above \(p_c\) from monotonicity and countable agreement

LemmaNonnegativity of the free percolation probability#✓fully proved

θ⁰(p, q) ≥ 0.

lemma fkThetaFree_nonneg (d : ℕ) {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) :
    0 ≤ fkThetaFree d hp hp1 hq (q := q)

Uses 5

Statement usesFree percolation probability

Proof usesConfiguration space of a statistical-mechanics model · Free infinite-volume random-cluster measure · Site of the hypercubic lattice · Percolation event for the origin

LemmaFree percolation probability is at most one#✓fully proved

θ⁰(p, q) ≤ 1.

lemma fkThetaFree_le_one (d : ℕ) {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) :
    fkThetaFree d hp hp1 hq (q := q) ≤ 1

Uses 5

Statement usesFree percolation probability

Proof usesConfiguration space of a statistical-mechanics model · Free infinite-volume random-cluster measure · Site of the hypercubic lattice · Percolation event for the origin

B. First-order transitions

DefinitionFirst-order transition of the random-cluster model#✓fully proved

A first-order transition at (p, q): the free measure does not percolate, θ⁰(p, q) = 0, while the wired one does, θ¹(p, q) > 0.

def IsFirstOrderTransition (d : ℕ) {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q) : Prop :=
  fkThetaFree d hp hp1 hq (q := q) = 0 ∧ 0 < fkTheta d hp hp1 hq (q := q)

Uses 2 · Used by 5

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

Used byFirst-order transition from \(\theta^0 = 0\) and \(\theta^1 > 0\) · \(\theta^0 \ne \theta^1\) at a first-order transition · Free and wired measures differ at a first-order transition · Free and wired measures differ at self-dual \(p\) for \(q > 4\) if first order · Free and wired measures differ at \(\sqrt{q}/(1+\sqrt{q})\) for \(q > 4\) if first order

LemmaFirst-order transition from \(\theta^0 = 0\) and \(\theta^1 > 0\)#✓fully proved

Introduction rule for IsFirstOrderTransition.

lemma firstOrderTransition_of_contour (d : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (hFree : fkThetaFree d hp hp1 hq (q := q) = 0)
    (hWired : 0 < fkTheta d hp hp1 hq (q := q)) :
    IsFirstOrderTransition d hp hp1 hq

Uses 3 · Used by 1

Statement usesFirst-order transition of the random-cluster model · Wired random-cluster percolation probability \(\theta(p, q)\) · Free percolation probability

Used byFree and wired measures differ at self-dual \(p\) for \(q > 4\) if first order

Lemma\(\theta^0 \ne \theta^1\) at a first-order transition#✓fully proved

At a first-order transition, θ⁰(p, q) ≠ θ¹(p, q).

lemma fkThetaFree_ne_fkTheta_of_firstOrder (d : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (h : IsFirstOrderTransition d hp hp1 hq) :
    fkThetaFree d hp hp1 hq (q := q) ≠ fkTheta d hp hp1 hq (q := q)

Uses 3 · Used by 1

Statement usesFirst-order transition of the random-cluster model · Wired random-cluster percolation probability \(\theta(p, q)\) · Free percolation probability

Used byFree and wired measures differ at a first-order transition

LemmaFree and wired measures differ at a first-order transition#✓fully proved

At a first-order transition, the free and wired infinite-volume measures differ.

lemma freeInfiniteVolume_ne_wiredInfiniteVolume_of_firstOrder (d : ℕ) {p q : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (h : IsFirstOrderTransition d hp hp1 hq) :
    freeInfiniteVolume d hp hp1 hq ≠ wiredInfiniteVolume d hp hp1 hq

Uses 9 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · First-order transition of the random-cluster model · Free infinite-volume random-cluster measure · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice

Proof usesWired random-cluster percolation probability \(\theta(p, q)\) · Free percolation probability · \(\theta^0 \ne \theta^1\) at a first-order transition · Percolation event for the origin

Used byFree and wired measures differ at self-dual \(p\) for \(q > 4\) if first order

LemmaFree and wired measures differ at self-dual \(p\) for \(q > 4\) if first order#✓fully proved

At a point p ∈ (0, 1) given as the self-dual point on ℤ², the hypotheses θ⁰ = 0 and θ¹ > 0 give a first-order transition with distinct free and wired measures. The first-order property for q > 4 (Duminil-Copin et al., 2021) is assumed, not proved; 4 < q is only used to get q > 0.

lemma order_transition_q_large {q : ℝ} (hq : 4 < q)
    (hpos : 0 < BeffaraDC.selfDualPoint q)
    (hlt : BeffaraDC.selfDualPoint q < 1)
    (hFree : fkThetaFree 2 hpos hlt (by linarith : (0 : ℝ) < q) (q := q) = 0)
    (hWired : 0 < fkTheta 2 hpos hlt (by linarith : (0 : ℝ) < q) (q := q)) :
    IsFirstOrderTransition 2 hpos hlt (by linarith : (0 : ℝ) < q)
      ∧ freeInfiniteVolume 2 hpos hlt (by linarith : (0 : ℝ) < q)
          ≠ wiredInfiniteVolume 2 hpos hlt (by linarith : (0 : ℝ) < q)

Uses 10 · Used by 1

Statement usesSelf-dual point \(p_{sd}(q) = \sqrt q/(1 + \sqrt q)\) · Configuration space of a statistical-mechanics model · First-order transition of the random-cluster model · Wired random-cluster percolation probability \(\theta(p, q)\) · Free percolation probability · Free infinite-volume random-cluster measure · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice

Proof usesFirst-order transition from \(\theta^0 = 0\) and \(\theta^1 > 0\) · Free and wired measures differ at a first-order transition

Used byFree and wired measures differ at \(\sqrt{q}/(1+\sqrt{q})\) for \(q > 4\) if first order

LemmaFree and wired measures differ at \(\sqrt{q}/(1+\sqrt{q})\) for \(q > 4\) if first order#✓fully proved

order_transition_q_large at the self-dual point p_sd(q) = √q / (1 + √q) of ℤ², with θ⁰(p_sd, q) = 0 and θ¹(p_sd, q) > 0 assumed.

StatMech.FK.order_transition_q_large_selfDual · 16 lines

lemma order_transition_q_large_selfDual {q : ℝ} (hq : 4 < q)
    (hFree : fkThetaFree 2 (BeffaraDC.selfDualPoint_mem_Ioo (by linarith : (0 : ℝ) < q)).1
        (BeffaraDC.selfDualPoint_mem_Ioo (by linarith : (0 : ℝ) < q)).2
        (by linarith : (0 : ℝ) < q) (q := q) = 0)
    (hWired : 0 < fkTheta 2 (BeffaraDC.selfDualPoint_mem_Ioo (by linarith : (0 : ℝ) < q)).1
        (BeffaraDC.selfDualPoint_mem_Ioo (by linarith : (0 : ℝ) < q)).2
        (by linarith : (0 : ℝ) < q) (q := q)) :
    IsFirstOrderTransition 2 (BeffaraDC.selfDualPoint_mem_Ioo (by linarith : (0 : ℝ) < q)).1
        (BeffaraDC.selfDualPoint_mem_Ioo (by linarith : (0 : ℝ) < q)).2
        (by linarith : (0 : ℝ) < q)
      ∧ freeInfiniteVolume 2 (BeffaraDC.selfDualPoint_mem_Ioo (by linarith : (0 : ℝ) < q)).1
          (BeffaraDC.selfDualPoint_mem_Ioo (by linarith : (0 : ℝ) < q)).2
          (by linarith : (0 : ℝ) < q)
        ≠ wiredInfiniteVolume 2 (BeffaraDC.selfDualPoint_mem_Ioo (by linarith : (0 : ℝ) < q)).1
            (BeffaraDC.selfDualPoint_mem_Ioo (by linarith : (0 : ℝ) < q)).2
            (by linarith : (0 : ℝ) < q)

Uses 9

Statement usesSelf-dual point \(p_{sd}(q) = \sqrt q/(1 + \sqrt q)\) · Configuration space of a statistical-mechanics model · First-order transition of the random-cluster model · Wired random-cluster percolation probability \(\theta(p, q)\) · Free percolation probability · Free infinite-volume random-cluster measure · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice

Proof usesFree and wired measures differ at self-dual \(p\) for \(q > 4\) if first order

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.