Clusters as open clusters of indicator configurations, and anchored boundary walks

3 fully proved

A. Indicator configurations of clusters

DefinitionBond configuration open on the edges inside a set#✓fully proved

The bond configuration that is open exactly on the edges with both endpoints in K.

noncomputable def indicatorConfig (K : Finset (Site d)) : ConfigSpace (Sym2 (Site d)) :=
  fun e => Sym2.lift ⟨fun x y => decide (x ∈ K ∧ y ∈ K), by
    intro x y; simp only [decide_eq_decide]; tauto⟩ e

Uses 2 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice

Used byPlus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

B. Anchored boundary walks in two dimensions

DefinitionAnchor row of \(\ell\) sites in \(\mathbb{Z}^2\)#✓fully proved

The anchor row {(j, 0) : j < ℓ} in ℤ².

noncomputable def ccb_anchorRow (ℓ : ℕ) : Finset (Site 2) :=
  (Finset.range ℓ).image (fun j : ℕ => (![ (j : ℤ), 0] : Site 2))

Uses 1 · Used by 1

Statement usesSite of the hypercubic lattice

Used byAnchored closed-walk decoding of cluster contours in \(\mathbb{Z}^2\)

DefinitionAnchored closed-walk decoding of cluster contours in \(\mathbb{Z}^2\)#✓fully proved

In ℤ², every connected cluster in Λ_n with contour length ℓ has its contour decoded from a closed walk of length ℓ based in the anchor row.

def ccb_AnchoredBoundaryWalkExists (n ℓ : ℕ) : Prop :=
  ∃ D : (Σ v : Site 2, (hypercubicLattice 2).Walk v v) → Finset (Sym2 (Site 2)),
    ∀ K ∈ ccb_contourFiber 2 n ℓ,
      ∃ v ∈ ccb_anchorRow ℓ, ∃ w : (hypercubicLattice 2).Walk v v,
        w.length = ℓ ∧ D ⟨v, w⟩ = crossEdges (↑K) (bondFinsetTouch 2 n)

Uses 6

Statement usesBonds touching the box · Contour of a set: bonds crossing its boundary · Site of the hypercubic lattice · Anchor row of \(\ell\) sites in \(\mathbb{Z}^2\) · Connected clusters in a box with contour length \(\ell\) · Hypercubic lattice \(\mathbb{Z}^d\)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.