Potts correlations and random-cluster connectivity

DefinitionPotts two-point agreement probability#✓fully proved

The Potts two-point agreement probability μ_{G,β,J,q}(σ_x = σ_y).

noncomputable def pottsAgreeProb (q : ℕ) (β J : ℝ) (x y : V) : ℝ :=
  ∑ σ ∈ Finset.univ.filter (fun σ : V → Fin q => σ x = σ y), Potts.pottsProb G q β J σ

Uses 1 · Used by 3

Statement usesPotts probability of a spin configuration

Used byEdwards–Sokal correlation identity · Edwards–Sokal correlation identity in \((q-1)/q\) form · Potts two-point agreement at least \(1/q\) for \(q \ge 2\), \(\beta J > 0\)

TheoremEdwards–Sokal correlation identity#✓fully proved

For the q-state Potts model on a finite graph with p = 1 - e^{-βJ} ∈ (0, 1), μ_{β,J,q}(σ_x = σ_y) - 1/q = (1 - 1/q) φ_{p,q}(x ↔ y). The hypothesis hp1 holds for every real βJ and hq follows from [NeZero q]; the only restriction is hp, i.e. βJ > 0 (ferromagnetic). (Edwards–Sokal, Phys. Rev. D 38, 1988; Grimmett, The Random-Cluster Model, 2006, Theorem 1.16.)

theorem edwards_sokal_correlation (q : ℕ) [NeZero q] (β J : ℝ) (x y : V)
    (hp : 0 < 1 - Real.exp (-(β * J))) (hp1 : 1 - Real.exp (-(β * J)) < 1)
    (hq : 0 < (q : ℝ)) :
    pottsAgreeProb G q β J x y - 1 / q
      = (1 - 1 / q) * connProb G (1 - Real.exp (-(β * J))) q x y

Uses 24 · Used by 2

Statement usesRandom-cluster connection probability · Potts two-point agreement probability

Proof usesConfiguration space of a statistical-mechanics model · Open connection between two vertices · Spin configuration constant on open clusters · Correspondence for cluster-constant colorings equal at two vertices · Bernoulli edge product · Functions equal at two points as functions omitting one point · Edwards–Sokal edge factor · Normalizing constant relating the bond sum to the Potts weight · Spin marginal of the Edwards–Sokal measure · Edwards–Sokal joint weight · Edwards–Sokal weight summed over spins is the random-cluster weight · Edwards–Sokal bond sum is a multiple of the Potts weight · Edwards–Sokal partition function · Probability of an ambient FK configuration · Unnormalized random-cluster weight · Ambient FK normalizer · Number of open clusters · Open subgraph of an edge configuration · Monochromatic-edge indicator · Potts probability of a spin configuration · Potts Boltzmann weight · Potts partition function

Used byEdwards–Sokal correlation identity in \((q-1)/q\) form · Potts two-point agreement at least \(1/q\) for \(q \ge 2\), \(\beta J > 0\)

LemmaEdwards–Sokal correlation identity in \((q-1)/q\) form#✓fully proved

The Edwards–Sokal correlation identity with the prefactor written as (q - 1)/q.

lemma edwards_sokal_correlation' (q : ℕ) [NeZero q] (β J : ℝ) (x y : V)
    (hp : 0 < 1 - Real.exp (-(β * J))) (hp1 : 1 - Real.exp (-(β * J)) < 1)
    (hq : 0 < (q : ℝ)) :
    pottsAgreeProb G q β J x y - 1 / q
      = ((q : ℝ) - 1) / q * connProb G (1 - Real.exp (-(β * J))) q x y

Uses 3

Statement usesRandom-cluster connection probability · Potts two-point agreement probability

Proof usesEdwards–Sokal correlation identity

LemmaPotts two-point agreement at least \(1/q\) for \(q \ge 2\), \(\beta J > 0\)#✓fully proved

For q ≥ 2 and βJ > 0, two Potts spins agree with probability at least 1/q.

lemma pottsAgreeProb_ge (q : ℕ) [NeZero q] (β J : ℝ) (x y : V)
    (hp : 0 < 1 - Real.exp (-(β * J))) (hp1 : 1 - Real.exp (-(β * J)) < 1)
    (hq : 2 ≤ q) :
    1 / q ≤ pottsAgreeProb G q β J x y

Uses 11

Statement usesPotts two-point agreement probability

Proof usesConfiguration space of a statistical-mechanics model · Open connection between two vertices · Random-cluster connection probability · Bernoulli edge product · Edwards–Sokal correlation identity · Probability of an ambient FK configuration · Unnormalized random-cluster weight · Ambient FK normalizer · Number of open clusters · Open subgraph of an edge configuration

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.