The Edwards–Sokal coupling

14 fully proved

A. The joint weight

DefinitionEdwards–Sokal edge factor#✓fully proved

The Edwards–Sokal factor of an edge e: 1 - p if e is closed in ω, and p times the indicator that σ agrees at the endpoints if e is open.

def esEdgeFactor {q : ℕ} (p : ℝ) (σ : V → Fin q) (ω : ConfigSpace (Sym2 V)) (e : Sym2 V) : ℝ :=
  if ω e then p * Potts.monoIndicator σ e else 1 - p

Uses 2 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · Monochromatic-edge indicator

Used byIsing two-point function equals the \(q = 2\) connection probability · Edwards–Sokal correlation identity · 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 one-point identity

DefinitionEdwards–Sokal joint weight#✓fully proved

The Edwards–Sokal joint weight of a spin configuration σ and a bond configuration ω: the product of esEdgeFactor over the edges of G.

def esWeight {q : ℕ} (p : ℝ) (σ : V → Fin q) (ω : ConfigSpace (Sym2 V)) : ℝ :=
  ∏ e ∈ G.edgeFinset, esEdgeFactor p σ ω e

Uses 2 · Used by 18

Statement usesConfiguration space of a statistical-mechanics model · Edwards–Sokal edge factor

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 joint probability · Ising two-point function from the Edwards–Sokal coupling · Ising two-point function equals the \(q = 2\) connection probability · Edwards–Sokal correlation identity · Edwards–Sokal weight with fixed boundary color · Edwards–Sokal spin marginal is the Potts measure · Edwards–Sokal bond marginal is the random-cluster measure · Spin marginal of the Edwards–Sokal measure · Bond marginal of the Edwards–Sokal measure · 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 · Edwards–Sokal one-point identity

B. Spin marginal: counting colorings constant on clusters

DefinitionSpin configuration constant on open clusters#✓fully proved

σ is constant on every open edge of ω, i.e. on every open cluster.

def ConstOnOpen {q : ℕ} (ω : ConfigSpace (Sym2 V)) (σ : V → Fin q) : Prop :=
  ∀ x y, (openSub G ω).Adj x y → σ x = σ y

Uses 2 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model · Open subgraph of an edge configuration

Used byCorrespondence for cluster-constant colorings equal at two vertices · Ising two-point function equals the \(q = 2\) connection probability · Edwards–Sokal correlation identity · There are \(q^{k(\omega)}\) colorings constant on the open clusters · Cluster-constant colorings as colorings of clusters · Edwards–Sokal weight summed over spins is the random-cluster weight · Edwards–Sokal one-point identity

DefinitionCluster-constant colorings as colorings of clusters#✓fully proved

Colorings constant on open clusters correspond to colorings of the connected components of the open subgraph.

StatMech.FK.constOnOpenEquiv · 18 lines

noncomputable def constOnOpenEquiv {q : ℕ} (ω : ConfigSpace (Sym2 V)) :
    ((openSub G ω).ConnectedComponent → Fin q) ≃ {σ : V → Fin q // ConstOnOpen G ω σ} where
  toFun τ := ⟨fun v => τ ((openSub G ω).connectedComponentMk v), by
    intro x y hxy
    simp only
    congr 1
    exact SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj hxy⟩
  invFun σ := SimpleGraph.ConnectedComponent.lift σ.1 (by
    intro v w p _
    exact constOnOpen_reachable G ω σ.1 σ.2 p.reachable)
  left_inv τ := by
    funext c
    induction c using SimpleGraph.ConnectedComponent.ind with
    | _ v => rfl
  right_inv σ := by
    apply Subtype.ext
    funext v
    rfl

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Spin configuration constant on open clusters · Open subgraph of an edge configuration

Used byCorrespondence for cluster-constant colorings equal at two vertices · There are \(q^{k(\omega)}\) colorings constant on the open clusters

LemmaThere are \(q^{k(\omega)}\) colorings constant on the open clusters#✓fully proved

There are q ^ k(ω) colorings constant on the open clusters, where k(ω) is the number of clusters.

lemma card_constOnOpen {q : ℕ} (ω : ConfigSpace (Sym2 V)) :
    Nat.card {σ : V → Fin q // ConstOnOpen G ω σ} = q ^ numClusters G ω

Uses 5 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Spin configuration constant on open clusters · Number of open clusters

Proof usesCluster-constant colorings as colorings of clusters · Open subgraph of an edge configuration

Used byIsing two-point function equals the \(q = 2\) connection probability · Edwards–Sokal weight summed over spins is the random-cluster weight

LemmaEdwards–Sokal weight summed over spins is the random-cluster weight#✓fully proved

Spin marginal of the Edwards–Sokal weight: summing over spins gives the random-cluster weight p^{o(ω)} (1 - p)^{c(ω)} q^{k(ω)}.

lemma esWeight_sum {q : ℕ} (p : ℝ) (ω : ConfigSpace (Sym2 V)) :
    (∑ σ : V → Fin q, esWeight G p σ ω) = fkWeight G p (q : ℝ) ω

Uses 10 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Edwards–Sokal joint weight · Unnormalized random-cluster weight

Proof usesSpin configuration constant on open clusters · There are \(q^{k(\omega)}\) colorings constant on the open clusters · Bernoulli edge product · Edwards–Sokal edge factor · Number of open clusters · Open subgraph of an edge configuration · Monochromatic-edge indicator

Used byIsing two-point function equals the \(q = 2\) connection probability · Edwards–Sokal correlation identity · Edwards–Sokal bond marginal is the random-cluster measure

C. Bond marginal: the Potts weight

DefinitionEdwards–Sokal factor of an arbitrary coordinate and state#✓fully proved

The Edwards–Sokal factor of an edge e written for an arbitrary pair (e, b) with b the state of e; edges outside G get factor 1.

def esCoeff {q : ℕ} (p : ℝ) (σ : V → Fin q) (e : Sym2 V) (b : Bool) : ℝ :=
  if e ∈ G.edgeFinset then (if b then p * Potts.monoIndicator σ e else 1 - p) else 1

Uses 1 · Used by 1

Statement usesMonochromatic-edge indicator

Used byEdwards–Sokal bond sum is a multiple of the Potts weight

DefinitionNormalizing constant relating the bond sum to the Potts weight#✓fully proved

The normalizing constant e^{-βJ |E(G)|} relating the bond marginal to the Potts weight.

noncomputable def esFirstConst (β J : ℝ) : ℝ :=
  2 ^ (Fintype.card (Sym2 V) - G.edgeFinset.card)
    * Real.exp (-(β * J)) ^ G.edgeFinset.card

Used by 8

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 · Edwards–Sokal spin marginal is the Potts measure · Edwards–Sokal bond sum is a multiple of the Potts weight

LemmaEdwards–Sokal bond sum is a multiple of the Potts weight#✓fully proved

Bond marginal of the Edwards–Sokal weight: with p = 1 - e^{-βJ}, summing over bond configurations gives e^{-βJ |E|} times the Potts weight of σ.

lemma esWeight_sum_eq_pottsWeight {q : ℕ} (β J : ℝ) (σ : V → Fin q) :
    (∑ ω : ConfigSpace (Sym2 V), esWeight G (1 - Real.exp (-(β * J))) σ ω)
      = esFirstConst G β J * Potts.pottsWeight G β J σ

Uses 8 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model · Normalizing constant relating the bond sum to the Potts weight · Edwards–Sokal joint weight · Potts Boltzmann weight

Proof usesEdwards–Sokal factor of an arbitrary coordinate and state · Edwards–Sokal edge factor · Agreement count of a spin configuration · Monochromatic-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 correlation identity · Edwards–Sokal spin marginal is the Potts measure

D. Partition functions and marginals

DefinitionEdwards–Sokal partition function#✓fully proved

The Edwards–Sokal partition function: the total joint weight.

noncomputable def esZ (q : ℕ) (p : ℝ) : ℝ :=
  ∑ ω : ConfigSpace (Sym2 V), ∑ σ : V → Fin q, esWeight G p σ ω

Uses 2 · Used by 8

Statement usesConfiguration space of a statistical-mechanics model · Edwards–Sokal joint weight

Used byEdwards–Sokal joint probability · Ising two-point function from the Edwards–Sokal coupling · Ising two-point function equals the \(q = 2\) connection probability · Edwards–Sokal correlation identity · Edwards–Sokal spin marginal is the Potts measure · Edwards–Sokal bond marginal is the random-cluster measure · Spin marginal of the Edwards–Sokal measure · Bond marginal of the Edwards–Sokal measure

DefinitionBond marginal of the Edwards–Sokal measure#✓fully proved

The bond marginal of the normalized Edwards–Sokal measure.

noncomputable def esSecondMarginal (q : ℕ) (p : ℝ) (ω : ConfigSpace (Sym2 V)) : ℝ :=
  (∑ σ : V → Fin q, esWeight G p σ ω) / esZ G q p

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Edwards–Sokal joint weight · Edwards–Sokal partition function

Used byEdwards–Sokal bond marginal is the random-cluster measure

DefinitionSpin marginal of the Edwards–Sokal measure#✓fully proved

The spin marginal of the normalized Edwards–Sokal measure.

noncomputable def esFirstMarginal (q : ℕ) (p : ℝ) (σ : V → Fin q) : ℝ :=
  (∑ ω : ConfigSpace (Sym2 V), esWeight G p σ ω) / esZ G q p

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Edwards–Sokal joint weight · Edwards–Sokal partition function

Used byEdwards–Sokal correlation identity · Edwards–Sokal spin marginal is the Potts measure

LemmaEdwards–Sokal bond marginal is the random-cluster measure#✓fully proved

The bond marginal of the Edwards–Sokal measure is the random-cluster measure with parameters (1 - e^{-βJ}, q).

lemma edwardsSokal_secondMarginal (q : ℕ) (β J : ℝ) (ω : ConfigSpace (Sym2 V)) :
    esSecondMarginal G q (1 - Real.exp (-(β * J))) ω
      = fkProb G (1 - Real.exp (-(β * J))) (q : ℝ) ω

Uses 8

Statement usesConfiguration space of a statistical-mechanics model · Bond marginal of the Edwards–Sokal measure · Probability of an ambient FK configuration

Proof usesEdwards–Sokal joint weight · Edwards–Sokal weight summed over spins is the random-cluster weight · Edwards–Sokal partition function · Unnormalized random-cluster weight · Ambient FK normalizer

LemmaEdwards–Sokal spin marginal is the Potts measure#✓fully proved

The spin marginal of the Edwards–Sokal measure is the q-state Potts measure at inverse temperature β and coupling J.

lemma edwardsSokal_firstMarginal (q : ℕ) [NeZero q] (β J : ℝ) (σ : V → Fin q) :
    esFirstMarginal G q (1 - Real.exp (-(β * J))) σ = Potts.pottsProb G q β J σ

Uses 9

Statement usesSpin marginal of the Edwards–Sokal measure · Potts probability of a spin configuration

Proof usesConfiguration space of a statistical-mechanics model · Normalizing constant relating the bond sum to the Potts weight · Edwards–Sokal joint weight · Edwards–Sokal bond sum is a multiple of the Potts weight · Edwards–Sokal partition function · Potts Boltzmann weight · Potts partition function

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.