Spin-flip symmetry and the Peierls long-range-order criterion

5 fully proved

A. The global spin flip

DefinitionGlobal spin flip of a configuration#✓fully proved

The global spin flip σ ↦ -σ of an infinite-volume configuration.

def flipConfig (s : ConfigSpace (Site d)) : ConfigSpace (Site d) := fun y => !(s y)

Uses 2 · Used by 1

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\)

DefinitionSpin flip inside the box#✓fully proved

The spin flip of a configuration inside the box Λ_n.

def flipInterior {n : ℕ} (τ : {x // x ∈ box d n} → Bool) : {x // x ∈ box d n} → Bool :=
  fun x => !(τ x)

Uses 2 · Used by 2

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

Used bySpin flip inside the box as an involutive equivalence · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\)

DefinitionSpin flip inside the box as an involutive equivalence#✓fully proved

The spin flip inside the box as an involutive equivalence.

def flipInteriorEquiv {n : ℕ} :
    ({x // x ∈ box d n} → Bool) ≃ ({x // x ∈ box d n} → Bool) where
  toFun := flipInterior
  invFun := flipInterior
  left_inv := flipInterior_involutive
  right_inv := flipInterior_involutive

Uses 3 · Used by 1

Statement usesSpin flip inside the box · 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\)

C. Magnetization at the origin

DefinitionOrigin of \(\mathbb{Z}^d\)#✓fully proved

The origin of ℤ^d.

def origin (d : ℕ) : Site d := fun _ => 0

Uses 1 · Used by 21

Statement usesSite of the hypercubic lattice

Used byPositive planar percolation at some \(p < 1\) via the Ising model · Sites reachable from the origin after deleting edges · Minus cluster of the origin as a finite set · Connected cluster through the origin in the nearest-neighbour graph · Two-site set \(\{0, p\}\) · Winding hypothesis for outer contours on \(\mathbb{Z}^2\) · Outer contour map: clusters as interiors of boundary circuits · Finite-volume magnetization at the origin · Origin cluster family: finite site sets in the box through the origin · Probability that the origin spin is minus · Configuration with only the origin minus · 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 · Filled minus cluster of the origin as a finite set · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Peierls' theorem

DefinitionFinite-volume magnetization at the origin#✓fully proved

The magnetization ⟨σ_0⟩ at the origin in the finite-volume Ising measure on Λ_n with boundary condition η, bond set B, inverse temperature β and field h.

noncomputable def fvMagOrigin (η : ConfigSpace (Site d)) (n : ℕ)
    (B : Finset (Sym2 (Site d))) (β h : ℝ) : ℝ :=
  ∑ τ : {x // x ∈ box d n} → Bool, fvProb η n B β h τ * spin (glue η τ) (origin d)

Uses 7 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Finite-volume Gibbs probability with a boundary condition · Configuration glued from inside spins and a boundary condition · Origin of \(\mathbb{Z}^d\) · Spin of a configuration at a site · 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' theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.