Contours of minus clusters

15 fully proved

A. Flipping a set

DefinitionConfiguration with the spins in a set flipped#✓fully proved

The configuration with the spins in K flipped.

noncomputable def flipOnSet (K : Set (Site d)) (σ : ConfigSpace (Site d)) :
    ConfigSpace (Site d) :=
  fun x => if x ∈ K then !(σ x) else σ x

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. Contours

DefinitionBond crossing the boundary of a set#✓fully proved

The bond e has exactly one endpoint in K.

noncomputable def crosses (K : Set (Site d)) (e : Sym2 (Site d)) : Prop :=
  Sym2.lift ⟨fun x y => (x ∈ K ↔ y ∉ K), by
    intro x y; simp only [eq_iff_iff]
    by_cases hx : x ∈ K <;> by_cases hy : y ∈ K <;> tauto⟩ e

Uses 1 · Used by 5

Statement usesSite of the hypercubic lattice

Used byContour of a set: bonds crossing its boundary · 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

DefinitionContour of a set: bonds crossing its boundary#✓fully proved

The bonds of B crossing the boundary of K (the contour of K).

noncomputable def crossEdges (K : Set (Site d)) (B : Finset (Sym2 (Site d))) :
    Finset (Sym2 (Site d)) :=
  B.filter (crosses K)

Uses 2 · Used by 10

Statement usesBond crossing the boundary of a set · Site of the hypercubic lattice

Used byAnchored closed-walk decoding of cluster contours in \(\mathbb{Z}^2\) · Contour event of a set: opposite spins across every crossing bond · Contour length of a set · Connected face-boundary graphs at the axis for all realised contours · Tight axis circuit data: contour edges in one axis-face component · Contours of length \(\ell\) realised by connected clusters in a box · 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

DefinitionContour length of a set#✓fully proved

The number of bonds of B crossing the boundary of K.

noncomputable def contourLen (K : Set (Site d)) (B : Finset (Sym2 (Site d))) : ℕ :=
  (crossEdges K B).card

Uses 2 · Used by 18

Statement usesContour of a set: bonds crossing its boundary · 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 cluster-family contour sum · Peierls series bound on the connected-cluster contour sum · Connected face-boundary graphs at the axis for all connected clusters · Connected face-boundary graphs at the axis for all realised contours · Tight axis circuit data: contour edges in one axis-face component · Hole-free clusters with contour length \(\ell\) · Hole-free connected cluster through the origin · Winding hypothesis for outer contours on \(\mathbb{Z}^2\) · Contours of length \(\ell\) realised by connected clusters in a box · Outer contour map: clusters as interiors of boundary circuits · Peierls series bound on the origin-cluster contour sum · 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

DefinitionBond variable of a crossing bond#✓fully proved

The bond variable of a crossing bond.

noncomputable def crossEdgeBond (K : Set (Site d)) (σ : ConfigSpace (Site d))
    (e : Sym2 (Site d)) : ℝ :=
  Sym2.lift ⟨fun x y => if (x ∈ K ↔ y ∉ K) then bond σ s(x, y) else 0, by
    intro x y; simp only
    rw [bond_mk, bond_mk, mul_comm (spin σ x)]
    by_cases h : (x ∈ K ↔ y ∉ K)
    · rw [ite_eq_left h, ite_eq_left (by tauto)]
    · rw [ite_eq_right h, ite_eq_right (by tauto)]⟩ e

Uses 4 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Bond variable of an unordered pair · Spin of a configuration at a site · Site of the hypercubic lattice

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

C. Contour events and their probability

DefinitionContour event of a set: opposite spins across every crossing bond#✓fully proved

Every bond of B crossing the boundary of K joins a minus spin inside to a plus spin outside.

def ContourEvent (K : Set (Site d)) (B : Finset (Sym2 (Site d))) (σ : ConfigSpace (Site d)) :
    Prop :=
  ∀ e ∈ crossEdges K B, bond σ e = -1

Uses 4 · Used by 8

Statement usesConfiguration space of a statistical-mechanics model · Bond variable of an unordered pair · Contour of a set: bonds crossing its boundary · Site of the hypercubic lattice

Used byProbability of the contour event of a set · Winding hypothesis for outer contours on \(\mathbb{Z}^2\) · Outer contour map: clusters as interiors of boundary circuits · 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

DefinitionInside configuration with the spins in a set flipped#✓fully proved

The inside configuration with the spins in K flipped.

noncomputable def flipInteriorOn {n : ℕ} (K : Set (Site d))
    (τ : {x // x ∈ box d n} → Bool) : {x // x ∈ box d n} → Bool :=
  fun x => if (x : Site d) ∈ K then !(τ x) else τ x

Uses 2 · Used by 4

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byFlipping spins in a set as an involutive equivalence · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionFlipping spins in a set as an involutive equivalence#✓fully proved

Flipping the spins in K as an involutive equivalence of inside configurations.

noncomputable def flipInteriorOnEquiv {n : ℕ} (K : Set (Site d)) :
    ({x // x ∈ box d n} → Bool) ≃ ({x // x ∈ box d n} → Bool) where
  toFun := flipInteriorOn K
  invFun := flipInteriorOn K
  left_inv := flipInteriorOn_involutive K
  right_inv := flipInteriorOn_involutive K

Uses 3 · Used by 3

Statement usesInside configuration with the spins in a set flipped · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

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

DefinitionProbability of the contour event of a set#✓fully proved

The probability of the contour event of K under the box measure.

noncomputable def probContour (K : Set (Site d)) (η : ConfigSpace (Site d)) (n : ℕ)
    (B : Finset (Sym2 (Site d))) (β : ℝ) : ℝ :=
  ∑ τ : {x // x ∈ box d n} → Bool,
    (if ContourEvent K B (glue η τ) then fvProb η n B β 0 τ else 0)

Uses 6 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Contour event of a set: opposite spins across every crossing bond · Finite-volume Gibbs probability with a boundary condition · Configuration glued from inside spins and a boundary condition · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byBoltzmann weight of a closed walk in the circuit sum · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

D. Minus clusters

DefinitionSet of minus sites#✓fully proved

The set of minus sites.

def minusSet (σ : ConfigSpace (Site d)) : Set (Site d) := {x | σ x = false}

Uses 2 · Used by 7

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

Used byMinus cluster of the origin as a finite set · Nearest-neighbour graph on the minus sites · Origin-only minus configuration satisfies the filled-cluster data · 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

DefinitionNearest-neighbour graph on the minus sites#✓fully proved

The nearest-neighbour graph on the minus sites.

def minusGraph (σ : ConfigSpace (Site d)) : SimpleGraph (Site d) where
  Adj x y := (hypercubicLattice d).Adj x y ∧ x ∈ minusSet σ ∧ y ∈ minusSet σ
  symm := ⟨fun _ _ ⟨h1, h2, h3⟩ => ⟨h1.symm, h3, h2⟩⟩
  loopless := ⟨fun _ h => (hypercubicLattice d).irrefl h.1⟩

Uses 4 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model · Set of minus sites · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used byMinus cluster of a site · Minus cluster of the origin as a finite set · Origin-only minus configuration satisfies the filled-cluster data · 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

DefinitionMinus cluster of a site#✓fully proved

The minus cluster of o: the sites joined to o by a path of minus sites.

def minusCluster (σ : ConfigSpace (Site d)) (o : Site d) : Set (Site d) :=
  {x | (minusGraph σ).Reachable o x}

Uses 3 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on the minus sites · Site of the hypercubic lattice

Used byMinus cluster of the origin as a finite set · Origin-only minus configuration satisfies the filled-cluster data · 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

E. Cluster families and the Peierls sum

DefinitionCluster family: all subsets of the box#✓fully proved

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

noncomputable def clusterFamily (n : ℕ) : Finset (Finset (Site d)) :=
  (boxFinset d n).powerset

Uses 2 · Used by 7

Statement usesBox \((-n, n)^d\) as a finite set of sites · Site of the hypercubic lattice

Used byPeierls series bound on the cluster-family contour sum · Connected clusters in the box containing the origin · Hole-free clusters in the box through the origin · Origin cluster family: finite site sets in the box through the origin · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

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

The minus cluster of the origin in a plus-boundary box configuration, as a finset.

noncomputable def minusClusterFinset {n : ℕ} (τ : {x // x ∈ box d n} → Bool)
    (ho : glue (plusField d) τ (origin d) = false) : Finset (Site d) :=
  (minusCluster_glue_plus_finite τ ho).toFinset

Uses 10

Statement usesConfiguration space of a statistical-mechanics model · Configuration glued from inside spins and a boundary condition · Minus cluster of a site · Nearest-neighbour graph on the minus sites · Set of minus sites · Origin of \(\mathbb{Z}^d\) · All-plus configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

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

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

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

Uses 5

Statement usesBonds touching the box · Cluster family: all subsets of the box · 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.