The critical point of the planar random-cluster model equals the self-dual point

Lemma\(p_c(q)\) equals the self-dual point if percolation starts there, \(q \ge 1\)#✓fully proved

If θ(r, q) = 0 for r < p_sd(q) and θ(r, q) > 0 for r > p_sd(q), then p_c(q) = p_sd(q).

lemma fkPc_eq_selfDualPoint {q : ℝ} (hq : 1 ≤ q)
    (hNoPercBelow : ∀ (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1),
      r < selfDualPoint q → fkTheta 2 hr0 hr1 (zero_lt_one.trans_le hq) (q := q) = 0)
    (hPercAbove : ∀ (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1),
      selfDualPoint q < r → 0 < fkTheta 2 hr0 hr1 (zero_lt_one.trans_le hq) (q := q)) :
    fkPc 2 q = selfDualPoint q

Uses 8 · Used by 1

Statement usesSelf-dual point \(p_{sd}(q) = \sqrt q/(1 + \sqrt q)\) · Critical parameter \(p_c(q)\) of the random-cluster model · Wired random-cluster percolation probability \(\theta(p, q)\)

Proof usesPositivity of the random-cluster critical point · Non-percolating parameters of the wired random-cluster measure · Subcritical set is bounded above by one · Nonempty subcritical set on \(\mathbb{Z}^2\) for \(q \ge 1\) · Positive percolation probability rules out subcriticality

Used byBeffara–Duminil-Copin theorem, conditional form

TheoremBeffara–Duminil-Copin theorem, conditional form#✓fully proved

For q ≥ 1, if the wired random-cluster measure on ℤ² does not percolate for p < √q / (1 + √q) (hNoPercBelow) and percolates for p > √q / (1 + √q) (hPercAbove), then p_c(q) = √q / (1 + √q).

The two hypotheses are the content of the Beffara–Duminil-Copin theorem; this statement only identifies the supremum defining p_c(q) once they hold. They are true for every q ≥ 1, so the statement is not vacuous. (V. Beffara and H. Duminil-Copin, The self-dual point of the two-dimensional random-cluster model is critical for q ≥ 1, Probab. Theory Related Fields 153, 2012.)

theorem beffaraDC_critical_point {q : ℝ} (hq : 1 ≤ q)
    (hNoPercBelow : ∀ (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1),
      r < Real.sqrt q / (1 + Real.sqrt q) →
        fkTheta 2 hr0 hr1 (zero_lt_one.trans_le hq) (q := q) = 0)
    (hPercAbove : ∀ (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1),
      Real.sqrt q / (1 + Real.sqrt q) < r →
        0 < fkTheta 2 hr0 hr1 (zero_lt_one.trans_le hq) (q := q)) :
    fkPc 2 q = Real.sqrt q / (1 + Real.sqrt q)

Uses 4

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

Proof uses\(p_c(q)\) equals the self-dual point if percolation starts there, \(q \ge 1\) · Self-dual point \(p_{sd}(q) = \sqrt q/(1 + \sqrt q)\)

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.