Compatible colorings in the Edwards–Sokal coupling

5 fully proved

A. Compatible colorings

DefinitionCompatibility of a coloring with a bond configuration#✓fully proved

A coloring σ is compatible with the bond configuration ω if every open edge of G joins vertices of the same color. See also FK.ConstOnOpen (compatible_iff_constOnOpen).

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

Uses 1 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model

Used byEdwards–Sokal one-point identity

DefinitionMonochromatic edge indicator#✓fully proved

Whether an edge is monochromatic under the coloring σ.

def monoBool {q : ℕ} (σ : V → Fin q) : Sym2 V → Bool :=
  Sym2.lift ⟨fun x y => decide (σ x = σ y), by
    intro a b
    simp only [decide_eq_decide]
    exact ⟨Eq.symm, Eq.symm⟩⟩

Used by 1

Used byEdges with differently colored endpoints

DefinitionEdges with differently colored endpoints#✓fully proved

The edges of G whose endpoints have different colors.

def disagreeEdges {q : ℕ} (σ : V → Fin q) : Finset (Sym2 V) :=
  G.edgeFinset.filter (fun e => ¬ monoBool σ e)

Uses 1

Statement usesMonochromatic edge indicator

B. Colorings of the open clusters

DefinitionVertex coloring induced by a coloring of open clusters#✓fully proved

The coloring of the vertices obtained from a coloring τ of the open clusters of ω.

def coloring {q : ℕ} (ω : ConfigSpace (Sym2 V))
    (τ : (openSub G ω).ConnectedComponent → Fin q) : V → Fin q :=
  fun v => τ ((openSub G ω).connectedComponentMk v)

Uses 2

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

C. The joint Edwards–Sokal probability

DefinitionEdwards–Sokal joint probability#✓fully proved

The joint Edwards–Sokal probability of the coloring σ and the bond configuration ω.

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

Uses 3

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

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.