Ising two-point function via the Edwards–Sokal coupling

7 fully proved

A. Spins, connection events, and connection probabilities

DefinitionIsing spin value of a two-state color#✓fully proved

The Ising spin value of a two-state color: 0 ↦ -1, 1 ↦ 1.

def isingSpin : Fin 2 → ℝ := fun a => if a = 0 then 1 else -1

Used by 11

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 from the Edwards–Sokal coupling · Ising two-point function equals the \(q = 2\) connection probability · Ising bond variable of a two-state coloring · Plus-boundary Ising one-point function on a graph · Wired Edwards–Sokal one-point function · Edwards–Sokal one-point identity

DefinitionOpen connection between two vertices#✓fully proved

x and y are joined by a path of open edges of ω in G (x ↔ y).

def Connected (ω : ConfigSpace (Sym2 V)) (x y : V) : Prop :=
  (openSub G ω).Reachable x y

Uses 2 · Used by 19

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

Used byConnection to the boundary depends only on graph edges · Random-cluster connection probability · Ising two-point function equals the \(q = 2\) connection probability · Edwards–Sokal correlation identity · Potts two-point agreement at least \(1/q\) for \(q \ge 2\), \(\beta J > 0\) · Open connection of a vertex to the boundary · Edwards–Sokal one-point identity · Wired random-cluster probability of connecting to the boundary · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Boundary connection inside \(\Lambda_n\) reaches outside \(\Lambda_{n-1}\) · One-step decrease of the events \(0 \leftrightarrow \partial\Lambda_n\) · Open path from the origin out of \(\Lambda_n\) gives \(0 \leftrightarrow \partial\Lambda_n\) inside \(\Lambda_n\) · Paths to \(\partial\Lambda_{n+1}\) pass through \(\partial\Lambda_n\) · Origin-to-boundary connection is an increasing event · Boundary-connection event of \(\Lambda_n\) on \(\Lambda_m\) is increasing · Cylinder form of the \(\Lambda_n\) boundary connection is measurable · Infinite-volume limit of the wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\) · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+1}\) at most in \(\Lambda_n\)

DefinitionRandom-cluster connection probability#✓fully proved

The random-cluster connection probability φ_{G,p,q}(x ↔ y).

noncomputable def connProb (p q : ℝ) (x y : V) : ℝ :=
  ∑ ω ∈ Finset.univ.filter (fun ω : ConfigSpace (Sym2 V) => Connected G ω x y),
    fkProb G p q ω

Uses 4 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Open connection between two vertices · Probability of an ambient FK configuration · Open subgraph of an edge configuration

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

B. Counting colorings that agree at two points

DefinitionFunctions equal at two points as functions omitting one point#✓fully proved

For a ≠ b, functions C → Fin q with f a = f b correspond to functions on C \ {b}.

StatMech.FK.eqFunEquiv · 19 lines

noncomputable def eqFunEquiv {C : Type*} [Fintype C] [DecidableEq C] (q : ℕ) (a b : C)
    (hab : a ≠ b) :
    {f : C → Fin q // f a = f b} ≃ ({c : C // c ≠ b} → Fin q) where
  toFun f := fun c => f.1 c.1
  invFun g := ⟨fun c => if h : c = b then g ⟨a, hab⟩ else g ⟨c, h⟩, by
    change (if h : a = b then g ⟨a, hab⟩ else g ⟨a, h⟩)
        = if h : b = b then g ⟨a, hab⟩ else g ⟨b, h⟩
    rw [dite_eq_right hab, dite_eq_left rfl]⟩
  left_inv f := by
    apply Subtype.ext
    funext c
    simp only
    by_cases h : c = b
    · rw [dite_eq_left h, h]; exact f.2
    · rw [dite_eq_right h]
  right_inv g := by
    funext c
    simp only
    rw [dite_eq_right c.2]

Used by 2

Used byIsing two-point function equals the \(q = 2\) connection probability · Edwards–Sokal correlation identity

DefinitionCorrespondence for cluster-constant colorings equal at two vertices#✓fully proved

Colorings constant on open clusters with σ x = σ y correspond to colorings of the clusters that agree on the clusters of x and y.

noncomputable def constEqEquiv {q : ℕ} (ω : ConfigSpace (Sym2 V)) (x y : V) :
    {σ : V → Fin q // ConstOnOpen G ω σ ∧ σ x = σ y} ≃
      {τ : (openSub G ω).ConnectedComponent → Fin q //
        τ ((openSub G ω).connectedComponentMk x)
          = τ ((openSub G ω).connectedComponentMk y)} := by
  refine (Equiv.subtypeSubtypeEquivSubtypeInter _ _).symm.trans ?_
  exact ((constOnOpenEquiv G ω).subtypeEquiv (fun _ => Iff.rfl)).symm

Uses 4 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Spin configuration constant on open clusters · Cluster-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 correlation identity

C. The two-point function

DefinitionIsing two-point function from the Edwards–Sokal coupling#✓fully proved

The Ising two-point function ⟨σ_x σ_y⟩ at bond parameter p, computed as the Edwards–Sokal spin marginal.

noncomputable def esTwoPoint (p : ℝ) (x y : V) : ℝ :=
  (∑ ω : ConfigSpace (Sym2 V), ∑ σ : V → Fin 2,
      esWeight G p σ ω * (isingSpin (σ x) * isingSpin (σ y))) / esZ G 2 p

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Edwards–Sokal joint weight · Edwards–Sokal partition function · Ising spin value of a two-state color

Used byIsing two-point function equals the \(q = 2\) connection probability

LemmaIsing two-point function equals the \(q = 2\) connection probability#✓fully proved

The Ising two-point function equals the random-cluster connection probability with q = 2: ⟨σ_x σ_y⟩ = φ_{p,2}(x ↔ y) (Edwards–Sokal 1988; Grimmett, The Random-Cluster Model, 2006, Theorem 1.16).

lemma esTwoPoint_eq_connProb (p : ℝ) (x y : V) :
    esTwoPoint G p x y = connProb G p 2 x y

Uses 20

Statement usesRandom-cluster connection probability · Ising two-point function from the Edwards–Sokal coupling

Proof usesConfiguration space of a statistical-mechanics model · Open connection between two vertices · Spin configuration constant on open clusters · There are \(q^{k(\omega)}\) colorings constant on the 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 · Edwards–Sokal joint weight · Edwards–Sokal weight summed over spins is the random-cluster weight · Edwards–Sokal partition function · Probability of an ambient FK configuration · Unnormalized random-cluster weight · Ambient FK normalizer · Ising spin value of a two-state color · Number of open clusters · Open subgraph of an edge configuration · Monochromatic-edge indicator

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.