Skip to content

The Peierls bound on the square lattice

DefinitionFilled-cluster winding hypothesis#✓fully proved

The filled-cluster form of the winding hypothesis, with a face-connected boundary.

def OuterContourFill (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)) ∧
        FaceBoundaryConnected (↑K : Set (Site 2)) T ∧
        j < contourLen (↑K : Set (Site 2)) (bondFinsetTouch 2 n) ∧
        axisVertex 2 j ∈ T
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 · Connectedness of the face-boundary graph on a face set · Site of the hypercubic lattice · Site \((j, 0, \ldots, 0)\) on the first coordinate axis · Box \((-n, n)^d\) in the hypercubic lattice · Face-boundary graph of a set
Used byPlus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionExterior component of the complement of a set#✓fully proved

The component of the complement of S that contains the outside of Λ_n.

noncomputable def outerExteriorComponent (S : Set (Site 2)) (n : ℕ) : Set (Site 2) :=
  {x | (latticeOn Sᶜ).Reachable (beacon 2 n) x}
Uses 3 · Used by 5
Statement usesNearest-neighbour graph restricted to a set · Site of the hypercubic lattice · Base point of the exterior of a box
Used byPlus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Set with its holes filled · Filled minus cluster of the origin as a finite set · Peierls' theorem

DefinitionSet with its holes filled#✓fully proved

The set S with its holes filled: the complement of its exterior component.

noncomputable def spinCompatibleFill (S : Set (Site 2)) (n : ℕ) : Set (Site 2) :=
  (outerExteriorComponent S n)ᶜ
Uses 2 · Used by 4
Statement usesExterior component of the complement of a set · Site of the hypercubic lattice
Used byPlus 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
8 fully proved

B. The filled cluster

DefinitionFilled minus cluster of the origin as a finite set#✓fully proved

The filled minus cluster of the origin, as a finset.

noncomputable def spinCompatibleFillFinset {n : ℕ}
    (τ : {x // x ∈ box 2 n} → Bool)
    (ho : glue (plusField 2) τ (origin 2) = false) : Finset (Site 2) :=
  (spinCompatibleFill_finite τ ho).toFinset
Uses 16 · Used by 3
Statement usesConfiguration space of a statistical-mechanics model · Configuration glued from inside spins and a boundary condition · Nearest-neighbour graph restricted to a set · Minus cluster of a site · Nearest-neighbour graph on the minus sites · Set of minus sites · Origin of \(\mathbb{Z}^d\) · Exterior component of the complement of a set · All-plus configuration · Set with its holes filled · Site of the hypercubic lattice · Base point of the exterior of a box · Box \((-n, n)^d\) in the hypercubic lattice · Exterior of a box in \(\mathbb{Z}^d\) · Hypercubic lattice \(\mathbb{Z}^d\) · Setting a set of coordinates of a lattice site
Used byPlus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

D. The Peierls bound

TheoremPlus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\)#✓fully proved

Plus and minus box measures on ℤ² differ for all β beyond some β₀. See peierls_probOriginMinus_le_uniform for the informative uniform bound; the inequality of measures itself holds for every β > 0.

theorem peierls_long_range_order_spinCompatibleFill :
    ∃ β₀ : ℝ, ∀ (n : ℕ) (β : ℝ), β₀ ≤ β →
      plusMeasure 2 n β 0 ≠ minusMeasure 2 n β 0
Uses 117
Statement usesConfiguration space of a statistical-mechanics model · Minus-boundary Ising measure in a box · Plus-boundary Ising measure in a box · Site of the hypercubic lattice
Proof usesContour event of a set: opposite spins across every crossing bond · Connected cluster through the origin in the nearest-neighbour graph · Hole-free connected cluster through the origin · Filled-cluster winding hypothesis · Winding hypothesis for outer contours on \(\mathbb{Z}^2\) · Bond variable of an unordered pair · Bonds touching the box · Ordered nearest-neighbour pairs touching the box · Box \((-n, n)^d\) as a finite set of sites · Cluster family: all subsets of the box · Connected clusters in the box containing the origin · Contour length of a set · Bond variable of a crossing bond · Contour of a set: bonds crossing its boundary · Bond crossing the boundary of a set · Global spin flip of a configuration · Spin flip inside the box · Spin flip inside the box as an involutive equivalence · Inside configuration with the spins in a set flipped · Flipping spins in a set as an involutive equivalence · Configuration with the spins in a set flipped · Box energy with a boundary condition · Finite-volume magnetization at the origin · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Finite-volume Gibbs probability with a boundary condition · Finite-volume Boltzmann weight with a boundary condition · Finite-volume partition function with a boundary condition · Configuration glued from inside spins and a boundary condition · Hole-free clusters with contour length \(\ell\) · Hole-free clusters in the box through the origin · Nearest-neighbour graph restricted to a set · Minus cluster of a site · All-minus configuration · Nearest-neighbour graph on the minus sites · Set of minus sites · Origin of \(\mathbb{Z}^d\) · Exterior component of the complement of a set · Peierls series · Ratio \(2d e^{-2\beta}\) of the Peierls series · All-plus configuration · Probability of the contour event of a set · Probability that the origin spin is minus · Spin of a configuration at a site · Set with its holes filled · Filled minus cluster of the origin as a finite set · Twice the Peierls series · Connection by an open path · Euler's theorem for a graph supported on a finite connected set · Connectedness of the face-boundary graph on a face set · Nearest neighbours in \(\mathbb{Z}^d\) · Planar lattice subgraph of the square lattice · Site on the positive horizontal axis · Site \((j, 0, \ldots, 0)\) on the first coordinate axis · Boundary edge of a set · Boundary indicator of an edge · Base point of the exterior of a box · Edge boundary of a set of sites · Box \((-n, n)^d\) in the hypercubic lattice · Nearest neighbours of a lattice site · Neighbour of a site in a coordinate direction · Edgeless graph has one component per vertex · Removing one element lowers cardinality by one · Open cluster of a site · Component of a face in the face-boundary graph · Faces of a set reachable from a face in the face-boundary graph · Four unit faces at a lattice site · Primal edges crossed by a closed dual walk · Edge boundary of a set of sites · Edge with exactly one endpoint in a set · Face below the exit edge · Face above the exit edge · Exit index of a finite origin cluster · Axis site lies outside the origin cluster · Exterior of a box in \(\mathbb{Z}^d\) · Boundary degree of a unit face · Face-boundary graph of a set · Lower left corner of the unit face at \((a, b)\) · Upper left corner of the unit face at \((a, b)\) · Lower right corner of the unit face at \((a, b)\) · Upper right corner of the unit face at \((a, b)\) · Every finite set of sites lies in a box · Two faces flanking a primal edge · Two faces flanking an unordered pair of sites · Hypercubic lattice \(\mathbb{Z}^d\) · Square lattice is connected · Image of a planar lattice subgraph in the square lattice · Bond configuration open on the edges inside a set · Bounded faces of a finite lattice graph are counted by its cycle rank · Outer face region of a planar lattice subgraph · \(\ell^1\) distance on \(\mathbb{Z}^d\) · Square lattice with the boundary edges of a set removed · Hypercubic lattice with the edge boundary removed · Site on the negative horizontal axis · Face below the left exit edge · Face above the left exit edge · Left exit index of a finite cluster · Left exit condition at an axis site · Cycle rank of a finite graph · Open subgraph of a bond configuration · Radius of a box containing a planar lattice subgraph · Support of the face-boundary graph of a finite set · Shift isomorphism: lattice minus barrier edges to face region graph · Face-boundary graph of a finite set as a planar subgraph · Setting a set of coordinates of a lattice site · Primal edge shared by adjacent faces · Shift of a site along a coordinate · Primal edge crossed by a dual edge · Primal edge crossed by an unordered pair of faces · Face-region graph of a square-lattice subgraph · Faithful discrete Jordan statement for the face count · Number of bounded faces of a lattice subgraph · Anchor sites for dual circuits · Origin of the hypercubic lattice

TheoremPeierls bound#✓fully proved

Peierls bound on ℤ², uniform in the box: there is β₀ such that for β ≥ β₀ the probability that the origin is minus under the plus-boundary box measure on Λ_n is at most twoPeierlsBound 2 β, which is less than 1 / 2 and independent of n.

theorem peierls_probOriginMinus_le_uniform :
    ∃ β₀ : ℝ, ∀ β : ℝ, β₀ ≤ β → twoPeierlsBound 2 β < 1 / 2 ∧
      ∀ n : ℕ, probOriginMinus (plusField 2) n (bondFinsetTouch 2 n) β 0 ≤ twoPeierlsBound 2 β
Uses 109
Statement usesBonds touching the box · All-plus configuration · Probability that the origin spin is minus · Twice the Peierls series
Proof usesConfiguration space of a statistical-mechanics model · Contour event of a set: opposite spins across every crossing bond · Connected cluster through the origin in the nearest-neighbour graph · Hole-free connected cluster through the origin · Filled-cluster winding hypothesis · Winding hypothesis for outer contours on \(\mathbb{Z}^2\) · Bond variable of an unordered pair · Ordered nearest-neighbour pairs touching the box · Box \((-n, n)^d\) as a finite set of sites · Cluster family: all subsets of the box · Connected clusters in the box containing the origin · Contour length of a set · Bond variable of a crossing bond · Contour of a set: bonds crossing its boundary · Bond crossing the boundary of a set · Inside configuration with the spins in a set flipped · Flipping spins in a set as an involutive equivalence · Configuration with the spins in a set flipped · Box energy with a boundary condition · Finite-volume Gibbs probability with a boundary condition · Finite-volume Boltzmann weight with a boundary condition · Finite-volume partition function with a boundary condition · Configuration glued from inside spins and a boundary condition · Hole-free clusters with contour length \(\ell\) · Hole-free clusters in the box through the origin · Nearest-neighbour graph restricted to a set · Minus cluster of a site · Nearest-neighbour graph on the minus sites · Set of minus sites · Origin of \(\mathbb{Z}^d\) · Exterior component of the complement of a set · Peierls series · Ratio \(2d e^{-2\beta}\) of the Peierls series · Probability of the contour event of a set · Spin of a configuration at a site · Set with its holes filled · Filled minus cluster of the origin as a finite set · Connection by an open path · Euler's theorem for a graph supported on a finite connected set · Connectedness of the face-boundary graph on a face set · Nearest neighbours in \(\mathbb{Z}^d\) · Planar lattice subgraph of the square lattice · Site of the hypercubic lattice · Site on the positive horizontal axis · Site \((j, 0, \ldots, 0)\) on the first coordinate axis · Boundary edge of a set · Boundary indicator of an edge · Base point of the exterior of a box · Edge boundary of a set of sites · Box \((-n, n)^d\) in the hypercubic lattice · Nearest neighbours of a lattice site · Neighbour of a site in a coordinate direction · Edgeless graph has one component per vertex · Removing one element lowers cardinality by one · Open cluster of a site · Component of a face in the face-boundary graph · Faces of a set reachable from a face in the face-boundary graph · Four unit faces at a lattice site · Primal edges crossed by a closed dual walk · Edge boundary of a set of sites · Edge with exactly one endpoint in a set · Face below the exit edge · Face above the exit edge · Exit index of a finite origin cluster · Axis site lies outside the origin cluster · Exterior of a box in \(\mathbb{Z}^d\) · Boundary degree of a unit face · Face-boundary graph of a set · Lower left corner of the unit face at \((a, b)\) · Upper left corner of the unit face at \((a, b)\) · Lower right corner of the unit face at \((a, b)\) · Upper right corner of the unit face at \((a, b)\) · Every finite set of sites lies in a box · Two faces flanking a primal edge · Two faces flanking an unordered pair of sites · Hypercubic lattice \(\mathbb{Z}^d\) · Square lattice is connected · Image of a planar lattice subgraph in the square lattice · Bond configuration open on the edges inside a set · Bounded faces of a finite lattice graph are counted by its cycle rank · Outer face region of a planar lattice subgraph · \(\ell^1\) distance on \(\mathbb{Z}^d\) · Square lattice with the boundary edges of a set removed · Hypercubic lattice with the edge boundary removed · Site on the negative horizontal axis · Face below the left exit edge · Face above the left exit edge · Left exit index of a finite cluster · Left exit condition at an axis site · Cycle rank of a finite graph · Open subgraph of a bond configuration · Radius of a box containing a planar lattice subgraph · Support of the face-boundary graph of a finite set · Shift isomorphism: lattice minus barrier edges to face region graph · Face-boundary graph of a finite set as a planar subgraph · Setting a set of coordinates of a lattice site · Primal edge shared by adjacent faces · Shift of a site along a coordinate · Primal edge crossed by a dual edge · Primal edge crossed by an unordered pair of faces · Face-region graph of a square-lattice subgraph · Faithful discrete Jordan statement for the face count · Number of bounded faces of a lattice subgraph · Anchor sites for dual circuits · Origin of the hypercubic lattice

E. A nonvacuity check

DefinitionConfiguration with only the origin minus#✓fully proved

The configuration on Λ_n with only the origin minus.

noncomputable def isoOriginCompletion (n : ℕ) : {x // x ∈ box 2 n} → Bool :=
  fun x => decide ((x : Site 2) ≠ origin 2)
Uses 3 · Used by 1
Statement usesOrigin of \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice
Used byOrigin-only minus configuration satisfies the filled-cluster data

LemmaOrigin-only minus configuration satisfies the filled-cluster data#✓fully proved

A nonvacuity check: the configuration with only the origin minus satisfies the data of OuterContourFill.

lemma outerContourFill_nonvacuous (n : ℕ) :
    ∃ τ : {x // x ∈ box 2 n} → Bool, glue (plusField 2) τ (origin 2) = false ∧
      (↑({origin 2} : Finset (Site 2)) : Set (Site 2)) ⊆ box 2 n ∧
      IsConnectedCluster ({origin 2} : Finset (Site 2)) ∧
      ContourEvent (↑({origin 2} : Finset (Site 2)) : Set (Site 2)) (bondFinsetTouch 2 n)
        (glue (plusField 2) τ) ∧
      ∃ (T : Finset (Site 2)) (j : ℕ),
        (faceBoundaryGraph (↑({origin 2} : Finset (Site 2)) : Set (Site 2))).support
          ⊆ (T : Set (Site 2)) ∧
        FaceBoundaryConnected (↑({origin 2} : Finset (Site 2)) : Set (Site 2)) T ∧
        j < contourLen (↑({origin 2} : Finset (Site 2)) : Set (Site 2)) (bondFinsetTouch 2 n) ∧
        axisVertex 2 j ∈ T
Uses 40
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 · Connectedness of the face-boundary graph on a face set · Site of the hypercubic lattice · Site \((j, 0, \ldots, 0)\) on the first coordinate axis · Box \((-n, n)^d\) in the hypercubic lattice · Face-boundary graph of a set
Proof usesConfiguration space of a statistical-mechanics model · Bond variable of an unordered pair · Ordered nearest-neighbour pairs touching the box · Box \((-n, n)^d\) as a finite set of sites · Contour of a set: bonds crossing its boundary · Bond crossing the boundary of a set · Configuration with only the origin minus · Nearest-neighbour graph restricted to a set · Minus cluster of a site · Nearest-neighbour graph on the minus sites · Set of minus sites · Site \(j e_c\) on the \(c\)-th coordinate axis · Spin of a configuration at a site · Nearest neighbours in \(\mathbb{Z}^d\) · Boundary edge of a set · Boundary indicator of an edge · Nearest neighbours of a lattice site · Neighbour of a site in a coordinate direction · Four unit faces at a lattice site · Boundary degree of a unit face · Lower left corner of the unit face at \((a, b)\) · Upper left corner of the unit face at \((a, b)\) · Lower right corner of the unit face at \((a, b)\) · Upper right corner of the unit face at \((a, b)\) · Hypercubic lattice \(\mathbb{Z}^d\) · Primal edge shared by adjacent faces · Shift of a site along a coordinate · Four faces meeting the origin

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.