Skip to content

The Edwards–Sokal coupling with wired boundary conditions

12 fully proved

A. The Potts model with boundary color b

DefinitionColoring fixed to a color on the boundary#✓fully proved

The coloring σ equals b on every boundary vertex.

def BoundaryFixed {q : ℕ} (b : Fin q) (σ : V → Fin q) : Prop := ∀ x, bdry x → σ x = b
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 · Edwards–Sokal weight with fixed boundary color · Potts weight with fixed boundary color · Ising weight of a coloring with plus boundary · Box configurations as box-graph colorings with boundary color \(0\) · Edwards–Sokal one-point identity · Wired colorings as cluster colorings with a pinned boundary cluster

DefinitionPotts weight with fixed boundary color#✓fully proved

The Potts weight restricted to colorings with boundary color b.

noncomputable def pottsWeightWired {q : ℕ} (b : Fin q) (β J : ℝ) (σ : V → Fin q) : ℝ :=
  if BoundaryFixed bdry b σ then Potts.pottsWeight G β J σ else 0
Uses 2 · Used by 7
Statement usesColoring fixed to a color on the boundary · Potts Boltzmann weight
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 · Potts Gibbs probability with fixed boundary color · Potts partition function with fixed boundary color

DefinitionPotts partition function with fixed boundary color#✓fully proved

The partition function of the Potts model with boundary color b.

noncomputable def pottsZWired (q : ℕ) (b : Fin q) (β J : ℝ) : ℝ :=
  ∑ σ : V → Fin q, pottsWeightWired G bdry b β J σ
Uses 1 · Used by 6
Statement usesPotts weight with fixed boundary color
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 · Potts Gibbs probability with fixed boundary color

DefinitionPotts Gibbs probability with fixed boundary color#✓fully proved

The Gibbs probability of the Potts model with boundary color b.

noncomputable def pottsProbWired (q : ℕ) (b : Fin q) (β J : ℝ) (σ : V → Fin q) : ℝ :=
  pottsWeightWired G bdry b β J σ / pottsZWired G bdry q b β J
Uses 2
Statement usesPotts weight with fixed boundary color · Potts partition function with fixed boundary color

B. The wired Edwards–Sokal weight and its spin marginal

DefinitionEdwards–Sokal weight with fixed boundary color#✓fully proved

The Edwards–Sokal weight restricted to colorings with boundary color b.

noncomputable def esWeightWired {q : ℕ} (b : Fin q) (p : ℝ) (σ : V → Fin q)
    (ω : ConfigSpace (Sym2 V)) : ℝ :=
  if BoundaryFixed bdry b σ then esWeight G p σ ω else 0
Uses 3 · Used by 10
Statement usesConfiguration space of a statistical-mechanics model · Edwards–Sokal joint weight · Coloring fixed to a color on the boundary
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 · Spin marginal of the wired Edwards–Sokal measure · Bond marginal of the wired Edwards–Sokal measure · Total wired Edwards–Sokal weight · Wired Edwards–Sokal one-point function · Edwards–Sokal one-point identity

DefinitionTotal wired Edwards–Sokal weight#✓fully proved

The total wired Edwards–Sokal weight.

noncomputable def esZWired (q : ℕ) (b : Fin q) (p : ℝ) : ℝ :=
  ∑ ω : ConfigSpace (Sym2 V), ∑ σ : V → Fin q, esWeightWired G bdry b p σ ω
Uses 2 · Used by 9
Statement usesConfiguration space of a statistical-mechanics model · Edwards–Sokal weight with fixed boundary color
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 · Spin marginal of the wired Edwards–Sokal measure · Bond marginal of the wired Edwards–Sokal measure · Wired Edwards–Sokal one-point function · Edwards–Sokal one-point identity

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

The spin marginal of the wired Edwards–Sokal measure.

noncomputable def esWiredFirstMarginal (q : ℕ) (b : Fin q) (p : ℝ) (σ : V → Fin q) : ℝ :=
  (∑ ω : ConfigSpace (Sym2 V), esWeightWired G bdry b p σ ω) / esZWired G bdry q b p
Uses 3
Statement usesConfiguration space of a statistical-mechanics model · Edwards–Sokal weight with fixed boundary color · Total wired Edwards–Sokal weight

C. Colorings constant on wired clusters

DefinitionOpen-edge graph with a boundary clique#✓fully proved

The graph of open edges of ω together with a clique on the boundary vertices.

noncomputable def wiredSub (ω : ConfigSpace (Sym2 V)) : SimpleGraph V :=
  openSub G ω ⊔ boundaryCliqueGraph bdry
Uses 3 · Used by 4
Statement usesConfiguration space of a statistical-mechanics model · Open subgraph of an edge configuration · Complete graph on the boundary vertices
Used byColoring constant on the wired graph · Colorings constant on wired clusters as cluster colorings · Edwards–Sokal one-point identity · Wired colorings as cluster colorings with a pinned boundary cluster

DefinitionColoring constant on the wired graph#✓fully proved

The coloring σ is constant along the edges of wiredSub.

def ConstOnWired {q : ℕ} (ω : ConfigSpace (Sym2 V)) (σ : V → Fin q) : Prop :=
  ∀ x y, (wiredSub G bdry ω).Adj x y → σ x = σ y
Uses 2 · Used by 3
Statement usesConfiguration space of a statistical-mechanics model · Open-edge graph with a boundary clique
Used byColorings constant on wired clusters as cluster colorings · Edwards–Sokal one-point identity · Wired colorings as cluster colorings with a pinned boundary cluster

DefinitionColorings constant on wired clusters as cluster colorings#✓fully proved

Colorings constant on the clusters of wiredSub correspond to colorings of those clusters.

StatMech.IsingFK.constOnWiredEquiv · 19 lines 
noncomputable def constOnWiredEquiv {q : ℕ} (ω : ConfigSpace (Sym2 V)) :
    ((wiredSub G bdry ω).ConnectedComponent → Fin q)
      ≃ {σ : V → Fin q // ConstOnWired G bdry ω σ} where
  toFun τ := ⟨fun v => τ ((wiredSub G bdry ω).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 constOnWired_reachable G bdry ω σ.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 · Coloring constant on the wired graph · Open-edge graph with a boundary clique
Used byEdwards–Sokal one-point identity · Wired colorings as cluster colorings with a pinned boundary cluster

DefinitionFunctions pinned at a point as functions on its complement#✓fully proved

Functions to Fin q taking the value b at c₀ correspond to functions on the complement of c₀. See also Equiv.piSplitAt.

def pinnedFunEquiv {α : Type*} [DecidableEq α] {q : ℕ} (c₀ : α) (b : Fin q) :
    {τ : α → Fin q // τ c₀ = b} ≃ ({c : α // c ≠ c₀} → Fin q) where
  toFun τ := fun c => τ.1 c.1
  invFun g := ⟨fun a => if h : a = c₀ then b else g ⟨a, h⟩, by simp⟩
  left_inv := by
    rintro ⟨τ, hτ⟩
    apply Subtype.ext; funext a
    by_cases h : a = c₀
    · simp [h, hτ]
    · simp [h]
  right_inv := by
    intro g; funext c
    obtain ⟨a, ha⟩ := c
    simp [ha]
Used by 1
Used byEdwards–Sokal one-point identity

D. The bond marginal

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

The bond marginal of the wired Edwards–Sokal measure.

noncomputable def esWiredSecondMarginal (q : ℕ) (b : Fin q) (p : ℝ)
    (ω : ConfigSpace (Sym2 V)) : ℝ :=
  (∑ σ : V → Fin q, esWeightWired G bdry b p σ ω) / esZWired G bdry q b p
Uses 3
Statement usesConfiguration space of a statistical-mechanics model · Edwards–Sokal weight with fixed boundary color · Total wired Edwards–Sokal weight

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.