Peierls argument for the Ising model

• A connected cluster is determined by its edge boundary
• Spin-flip symmetry and the Peierls long-range-order criterion
• Connected dual contours of the singleton and rectangular clusters
• Euler circuits and single dual circuits for planar contours
• The Peierls argument: contour sums and the long-range-order criterion
• Contours of minus clusters
• Counting connected contours
• Injectivity of contours and the reduction to counting contour sets
• Contours of clusters in a box and closed-walk encodings
• Clusters as open clusters of indicator configurations, and anchored boundary walks
• Dual circuits anchored on a coordinate axis
• Dual circuits through one component of the contour
• Dual circuits decode to contours in two dimensions
• The contour of a hole-free planar set is a single cycle
• Hole-free clusters and the Peierls bound on the square lattice
• The contour-count bound over all clusters fails
• Outer contours on the square lattice
• The Peierls bound on the square lattice

DefinitionClosed-walk encoding of realised contours of length \(\ell\)#✓fully proved

Every realised contour of length ℓ in Λ_n is decoded from a closed lattice walk of length ℓ based at one of at most ℓ anchor sites.

def RealisedContourWalkEncoding (d n ℓ : ℕ) : Prop :=
  ∃ anchors : Finset (Site d), anchors.card ≤ ℓ ∧
    ∃ (enc : Finset (Sym2 (Site d)) → Σ v : Site d, (hypercubicLattice d).Walk v v)
      (decode : (Σ v : Site d, (hypercubicLattice d).Walk v v) → Finset (Sym2 (Site d))),
      ∀ F ∈ realisedContours d n ℓ,
        (enc F).1 ∈ anchors ∧ (enc F).2.length = ℓ ∧ decode (enc F) = F

Uses 3

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Contours of length \(\ell\) realised by connected clusters in a box

DefinitionPeierls count of connected clusters by contour length#✓fully proved

For every ℓ, at most ℓ (2d)^ℓ connected clusters through the origin in Λ_n have contour length ℓ.

def ConnectedContourCount (d n : ℕ) : Prop :=
  ∀ ℓ : ℕ,
    (((connClusterFamily (d := d) n).filter
        (fun (K : Finset (Site d)) => contourLen (↑K) (bondFinsetTouch d n) = ℓ)).card : ℝ)
      ≤ (ℓ : ℝ) * (2 * d : ℝ) ^ ℓ

Uses 4

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

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.