The wired Edwards–Sokal one-point function

5 fully proved

A. Counting pinned colorings

DefinitionWired colorings as cluster colorings with a pinned boundary cluster#✓fully proved

Colorings constant on wired clusters with boundary color b correspond to colorings of the clusters of wiredSub with the boundary cluster colored b.

StatMech.IsingFK.wiredColourEquiv · 15 lines

noncomputable def wiredColourEquiv {q : ℕ} (b : Fin q) (ω : ConfigSpace (Sym2 V))
    (v₀ : V) (hv₀ : bdry v₀) :
    {σ : V → Fin q // ConstOnWired G bdry ω σ ∧ BoundaryFixed bdry b σ}
      ≃ {τ : (wiredSub G bdry ω).ConnectedComponent → Fin q //
            τ ((wiredSub G bdry ω).connectedComponentMk v₀) = b} := by
  refine (Equiv.subtypeSubtypeEquivSubtypeInter _ _).symm.trans ?_
  refine ((constOnWiredEquiv G bdry ω).subtypeEquiv ?_).symm
  intro τ
  change (τ ((wiredSub G bdry ω).connectedComponentMk v₀) = b
        ↔ BoundaryFixed bdry b ((constOnWiredEquiv G bdry ω) τ).1)
  constructor
  · intro h x hx
    change τ ((wiredSub G bdry ω).connectedComponentMk x) = b
    rw [wiredSub_componentMk_eq_of_bdry G bdry hx hv₀]; exact h
  · intro h; have := h v₀ hv₀; simpa [constOnWiredEquiv] using this

Uses 8 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Open subgraph of an edge configuration · Coloring fixed to a color on the boundary · Coloring constant on the wired graph · Colorings constant on wired clusters as cluster colorings · Open-edge graph with a boundary clique · Complete graph on the boundary vertices · Boundary wiring relation

Used byEdwards–Sokal one-point identity

B. Connection to the boundary

DefinitionOpen connection of a vertex to the boundary#✓fully proved

The vertex x is joined by an open path of ω to a boundary vertex.

def ConnToBdry (ω : ConfigSpace (Sym2 V)) (x : V) : Prop :=
  ∃ y, bdry y ∧ Connected G ω x y

Uses 2 · Used by 23

Statement usesConfiguration space of a statistical-mechanics model · Open connection between two vertices

Used byConnection to the boundary depends only on graph edges · Monotonicity in \(p\) of the Bernoulli percolation probability · Wired \(q = 2\) origin-to-boundary probability at most Bernoulli · 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 · Wired box-boundary connection probability is monotone in \(p\) at \(q = 2\) · Edwards–Sokal one-point identity · Wired random-cluster probability of connecting to the boundary · Event that the box origin connects to the box 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\) · Origin-to-\(\partial\Lambda_n\) event as an event on \(\Lambda_{n+1}\) · A connection to outside the box passes through the box boundary · Boundary connection of \(\Lambda_n\) is a \(\Lambda_m\) cylinder event · Open path from the origin out of \(\Lambda_n\) gives \(0 \leftrightarrow \partial\Lambda_n\) inside \(\Lambda_n\) · Boundary-connection event of \(\Lambda_n\) as an event on \(\Lambda_m\) · Paths to \(\partial\Lambda_{n+1}\) pass through \(\partial\Lambda_n\) · Leaving \(\Lambda_n\) implies connecting to \(\partial\Lambda_n\) · Origin-to-boundary connection is an increasing event · Boundary-connection event of \(\Lambda_n\) on \(\Lambda_m\) is increasing · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+1}\) at most in \(\Lambda_n\)

D. The one-point function

DefinitionWired Edwards–Sokal one-point function#✓fully proved

The one-point function ⟨σ_x⟩ of the wired Edwards–Sokal measure with boundary color b and q = 2.

noncomputable def esWiredOnePoint (b : Fin 2) (p : ℝ) (x : V) : ℝ :=
  (∑ ω : ConfigSpace (Sym2 V), ∑ σ : V → Fin 2,
      esWeightWired G bdry b p σ ω * isingSpin (σ x)) / esZWired G bdry 2 b p

Uses 4 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · Ising spin value of a two-state color · Edwards–Sokal weight with fixed boundary color · Total wired Edwards–Sokal 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 · Edwards–Sokal one-point identity

DefinitionWired random-cluster probability of connecting to the boundary#✓fully proved

The probability φ^w(x ↔ ∂) that x is connected to the boundary under the wired random-cluster measure with q = 2.

noncomputable def wiredConnToBdryProb (p : ℝ) (x : V) : ℝ :=
  ∑ ω ∈ Finset.univ.filter (fun ω : ConfigSpace (Sym2 V) => ConnToBdry G bdry ω x),
    bcProb G (boundaryCliqueGraph bdry) p (2 : ℝ) ω

Uses 7 · Used by 8

Statement usesConfiguration space of a statistical-mechanics model · Open connection between two vertices · Random-cluster probability with a boundary wiring · Open subgraph of an edge configuration · Open connection of a vertex to the boundary · Complete graph on the boundary vertices · Boundary wiring relation

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 · Wired probability that the origin reaches the box boundary · Edwards–Sokal one-point identity · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do

TheoremEdwards–Sokal one-point identity#✓fully proved

With + boundary condition, the Ising magnetization at x equals the probability that x is connected to the boundary in the wired FK measure with q = 2 (Edwards and Sokal, Phys. Rev. D 38 (1988); Grimmett, The Random-Cluster Model, Theorem 1.16).

theorem esWiredOnePoint_eq_wiredConnToBdryProb (p : ℝ) (x : V) (v₀ : V) (hv₀ : bdry v₀) :
    esWiredOnePoint G bdry (0 : Fin 2) p x = wiredConnToBdryProb G bdry p x

Uses 27 · Used by 5

Statement usesWired Edwards–Sokal one-point function · Wired random-cluster probability of connecting to the boundary

Proof usesConfiguration space of a statistical-mechanics model · Open connection between two vertices · Spin configuration constant on open clusters · Random-cluster probability with a boundary wiring · Random-cluster weight with a boundary wiring · Partition function with a boundary wiring · Bernoulli edge product · Edwards–Sokal edge factor · Edwards–Sokal joint weight · Ising spin value of a two-state color · Number of clusters under a boundary wiring · Open subgraph of an edge configuration · Coloring fixed to a color on the boundary · Compatibility of a coloring with a bond configuration · Open connection of a vertex to the boundary · Coloring constant on the wired graph · Colorings constant on wired clusters as cluster colorings · Edwards–Sokal weight with fixed boundary color · Total wired Edwards–Sokal weight · Functions pinned at a point as functions on its complement · Wired colorings as cluster colorings with a pinned boundary cluster · Open-edge graph with a boundary clique · Complete graph on the boundary vertices · Boundary wiring relation · 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

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.