Hole-free clusters and the Peierls bound on the square lattice

4 fully proved

A. The winding hypothesis

DefinitionWinding hypothesis for outer contours on \(\mathbb{Z}^2\)#✓fully proved

Every plus-boundary configuration on Λ_n with the origin minus has a connected contour event through the origin whose boundary meets the positive axis within the contour length.

def OuterContourWinding (n : ℕ) : Prop :=
  ∀ τ : {x // x ∈ box 2 n} → Bool, glue (plusField 2) τ (origin 2) = false →
    ∃ K : Finset (Site 2), (↑K : Set (Site 2)) ⊆ box 2 n ∧ IsConnectedCluster K ∧
      ContourEvent (↑K : Set (Site 2)) (bondFinsetTouch 2 n) (glue (plusField 2) τ) ∧
      ∃ (T : Finset (Site 2)) (j : ℕ),
        (faceBoundaryGraph (↑K : Set (Site 2))).support ⊆ (T : Set (Site 2)) ∧
        j < contourLen (↑K : Set (Site 2)) (bondFinsetTouch 2 n) ∧
        axisVertex 2 j ∈ T ∧
        (∀ e ∈ (faceBoundaryGraph (↑K : Set (Site 2))).edgeSet,
          e ∈ (componentGraph (↑K : Set (Site 2)) (axisVertex 2 j)).edgeSet)

Uses 12 · Used by 3

Statement usesContour event of a set: opposite spins across every crossing bond · Connected cluster through the origin in the nearest-neighbour graph · Bonds touching the box · Contour length of a set · Configuration glued from inside spins and a boundary condition · Origin of \(\mathbb{Z}^d\) · All-plus configuration · Site of the hypercubic lattice · Site \((j, 0, \ldots, 0)\) on the first coordinate axis · Box \((-n, n)^d\) in the hypercubic lattice · Component of a face in the face-boundary graph · Face-boundary graph of a set

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

B. Hole-free clusters

DefinitionHole-free connected cluster through the origin#✓fully proved

K is a connected cluster in Λ_n through the origin without holes.

def IsHoleFreeBoxCluster (n : ℕ) (K : Finset (Site 2)) : Prop :=
  IsConnectedCluster K ∧
    ∃ (T : Finset (Site 2)) (j : ℕ),
      (faceBoundaryGraph (↑K : Set (Site 2))).support ⊆ (T : Set (Site 2)) ∧
      j < contourLen (↑K : Set (Site 2)) (bondFinsetTouch 2 n) ∧
      axisVertex 2 j ∈ T ∧
      (∀ e ∈ (faceBoundaryGraph (↑K : Set (Site 2))).edgeSet,
        e ∈ (componentGraph (↑K : Set (Site 2)) (axisVertex 2 j)).edgeSet)

Uses 7 · Used by 4

Statement usesConnected cluster through the origin in the nearest-neighbour graph · Bonds touching the box · Contour length of a set · Site of the hypercubic lattice · Site \((j, 0, \ldots, 0)\) on the first coordinate axis · Component of a face in the face-boundary graph · Face-boundary graph of a set

Used byHole-free clusters in the box through the origin · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionHole-free clusters in the box through the origin#✓fully proved

The hole-free clusters in Λ_n through the origin.

noncomputable def holeFreeClusterFamily (n : ℕ) : Finset (Finset (Site 2)) :=
  (clusterFamily (d := 2) n).filter (fun K => IsHoleFreeBoxCluster n K)

Uses 3 · Used by 4

Statement usesHole-free connected cluster through the origin · Cluster family: all subsets of the box · Site of the hypercubic lattice

Used byHole-free clusters with contour length \(\ell\) · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

C. Counting by contour length

DefinitionHole-free clusters with contour length \(\ell\)#✓fully proved

The hole-free clusters in Λ_n through the origin with contour length ℓ.

noncomputable def holeFreeAtLen (n ℓ : ℕ) : Finset (Finset (Site 2)) :=
  (holeFreeClusterFamily n).filter
    (fun K => contourLen (↑K : Set (Site 2)) (bondFinsetTouch 2 n) = ℓ)

Uses 4 · Used by 3

Statement usesBonds touching the box · Contour length of a set · Hole-free clusters in the box through the origin · Site of the hypercubic lattice

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

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.