Counting connected contours

5 fully proved

A. Failure of the origin bound

DefinitionTwo-site set \(\{0, p\}\)#✓fully proved

The two-site set {0, p}.

noncomputable def pcc_pairCluster (p : Site d) : Finset (Site d) := {origin d, p}

Uses 2

Statement usesOrigin of \(\mathbb{Z}^d\) · Site of the hypercubic lattice

B. Connected clusters

DefinitionNearest-neighbour graph restricted to a set#✓fully proved

The nearest-neighbour graph restricted to K.

noncomputable def latticeOn (K : Set (Site d)) : SimpleGraph (Site d) where
  Adj x y := (hypercubicLattice d).Adj x y ∧ x ∈ K ∧ y ∈ K
  symm := ⟨fun _ _ ⟨h1, h2, h3⟩ => ⟨h1.symm, h3, h2⟩⟩
  loopless := ⟨fun _ h => (hypercubicLattice d).irrefl h.1⟩

Uses 2 · Used by 7

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used byConnected cluster through the origin in the nearest-neighbour graph · Origin-only minus configuration satisfies the filled-cluster data · Exterior component of the complement of a set · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Filled minus cluster of the origin as a finite set · Peierls' theorem

DefinitionConnected cluster through the origin in the nearest-neighbour graph#✓fully proved

K is connected in the nearest-neighbour graph.

def IsConnectedCluster (K : Finset (Site d)) : Prop :=
  origin d ∈ K ∧ ∀ x ∈ K, (latticeOn (↑K : Set (Site d))).Reachable (origin d) x

Uses 3 · Used by 8

Statement usesNearest-neighbour graph restricted to a set · Origin of \(\mathbb{Z}^d\) · Site of the hypercubic lattice

Used byConnected clusters in the box containing the origin · Hole-free connected cluster through the origin · Winding hypothesis for outer contours on \(\mathbb{Z}^2\) · Filled-cluster winding hypothesis · Origin-only minus configuration satisfies the filled-cluster data · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionConnected clusters in the box containing the origin#✓fully proved

The connected finite sets of sites in Λ_n containing the origin.

noncomputable def connClusterFamily (n : ℕ) : Finset (Finset (Site d)) :=
  (clusterFamily (d := d) n).filter (fun K => IsConnectedCluster K)

Uses 3 · Used by 8

Statement usesConnected cluster through the origin in the nearest-neighbour graph · Cluster family: all subsets of the box · Site of the hypercubic lattice

Used byPeierls count of connected clusters by contour length · Connected clusters in a box with contour length \(\ell\) · Peierls series bound on the connected-cluster contour sum · Connected face-boundary graphs at the axis for all connected clusters · Contours of length \(\ell\) realised by connected clusters in a box · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionPeierls series bound on the connected-cluster contour sum#✓fully proved

The sum of e^{-2β |∂K|} over connected clusters is at most the Peierls series.

def ConnectedContourCountBound (d n : ℕ) (β : ℝ) : Prop :=
  ∑ K ∈ connClusterFamily (d := d) n,
      Real.exp (-(2 * β) * (contourLen (↑K) (bondFinsetTouch d n) : ℝ))
    ≤ peierlsBound d β

Uses 5

Statement usesBonds touching the box · Connected clusters in the box containing the origin · Contour length of a set · Peierls series · Site of the hypercubic lattice

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.