The q-state Potts model on a finite graph

6 fully proved

A. Monochromatic edges

DefinitionMonochromatic-edge indicator#✓fully proved

The indicator of a monochromatic edge: 𝟙[σ x = σ y] on the unordered pair s(x, y).

def monoIndicator {q : ℕ} (σ : V → Fin q) : Sym2 V → ℝ :=
  Sym2.lift ⟨fun x y => if σ x = σ y then (1 : ℝ) else 0, by
    intro a b
    dsimp only
    by_cases h : σ a = σ b
    · rw [ite_eq_left h, ite_eq_left h.symm]
    · rw [ite_eq_right h, ite_eq_right (Ne.symm h)]⟩

Used by 13

Used byPositive planar percolation at some \(p < 1\) via the Ising model · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-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 · Ising two-point function equals the \(q = 2\) connection probability · Edwards–Sokal correlation identity · Edwards–Sokal factor of an arbitrary coordinate and state · Edwards–Sokal edge factor · Edwards–Sokal weight summed over spins is the random-cluster weight · Edwards–Sokal bond sum is a multiple of the Potts weight · Agreement count of a spin configuration · Edwards–Sokal one-point identity

DefinitionAgreement count of a spin configuration#✓fully proved

The agreement count: the number of edges of G whose endpoints carry the same spin.

def agreement {q : ℕ} (σ : V → Fin q) : ℝ :=
  ∑ e ∈ G.edgeFinset, monoIndicator σ e

Uses 1 · Used by 8

Statement usesMonochromatic-edge indicator

Used byPositive planar percolation at some \(p < 1\) via the Ising model · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-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 · Edwards–Sokal bond sum is a multiple of the Potts weight · Potts Gibbs measure as a probability mass function · Potts Boltzmann weight

B. Weights and the partition function

DefinitionPotts Boltzmann weight#✓fully proved

The Potts Boltzmann weight exp (β J · agreement G σ).

noncomputable def pottsWeight {q : ℕ} (β J : ℝ) (σ : V → Fin q) : ℝ :=
  Real.exp (β * J * agreement G σ)

Uses 1 · Used by 12

Statement usesAgreement count of a spin configuration

Used byPositive planar percolation at some \(p < 1\) via the Ising model · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-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 · Edwards–Sokal correlation identity · Potts weight with fixed boundary color · Edwards–Sokal spin marginal is the Potts measure · Edwards–Sokal bond sum is a multiple of the Potts weight · Potts Gibbs measure as a probability mass function · Potts probability of a spin configuration · Potts partition function

DefinitionPotts partition function#✓fully proved

The Potts partition function Z = ∑_σ exp (β J · agreement G σ).

noncomputable def pottsZ (q : ℕ) (β J : ℝ) : ℝ :=
  ∑ σ : V → Fin q, pottsWeight G β J σ

Uses 1 · Used by 4

Statement usesPotts Boltzmann weight

Used byEdwards–Sokal correlation identity · Edwards–Sokal spin marginal is the Potts measure · Potts Gibbs measure as a probability mass function · Potts probability of a spin configuration

C. The Potts Gibbs measure

DefinitionPotts probability of a spin configuration#✓fully proved

The Potts probability of the spin configuration σ.

noncomputable def pottsProb (q : ℕ) (β J : ℝ) (σ : V → Fin q) : ℝ :=
  pottsWeight G β J σ / pottsZ G q β J

Uses 2 · Used by 4

Statement usesPotts Boltzmann weight · Potts partition function

Used byEdwards–Sokal correlation identity · Potts two-point agreement probability · Edwards–Sokal spin marginal is the Potts measure · Potts Gibbs measure as a probability mass function

DefinitionPotts Gibbs measure as a probability mass function#✓fully proved

The Potts Gibbs measure on V → Fin q as a probability mass function.

noncomputable def pottsPMF (q : ℕ) [NeZero q] (β J : ℝ) : PMF (V → Fin q) :=
  PMF.ofFintype (fun σ => ENNReal.ofReal (pottsProb G q β J σ)) <| by
    rw [← ENNReal.ofReal_sum_of_nonneg fun σ _ => pottsProb_nonneg G q β J σ,
      pottsProb_sum_eq_one]
    simp

Uses 4

Statement usesAgreement count of a spin configuration · Potts probability of a spin configuration · Potts Boltzmann weight · Potts partition function

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.