The Ising model in a box as a wired two-state Potts model

6 fully proved

A. The wired Ising model on a graph

DefinitionIsing bond variable of a two-state coloring#✓fully proved

The Ising bond σ_x σ_y of a two-state coloring, with color 0 as spin +1. See also Ising.bond for Boolean configurations.

noncomputable def isingBond (σ : V → Fin 2) (e : Sym2 V) : ℝ :=
  Sym2.lift ⟨fun x y => isingSpin (σ x) * isingSpin (σ y), fun _ _ => mul_comm _ _⟩ e

Uses 1 · Used by 6

Statement usesIsing spin value of a two-state color

Used byPositive planar percolation at some \(p < 1\) via the Ising model · 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 · Ising weight of a coloring with plus boundary

DefinitionIsing weight of a coloring with plus boundary#✓fully proved

The Ising weight exp (β ∑_e σ_x σ_y) of a two-state coloring with boundary color 0, and 0 otherwise.

noncomputable def isingWiredWeight (β : ℝ) (σ : V → Fin 2) : ℝ :=
  if BoundaryFixed bdry (0 : Fin 2) σ then
    Real.exp (β * ∑ e ∈ G.edgeFinset, isingBond σ e) else 0

Uses 2 · Used by 7

Statement usesColoring fixed to a color on the boundary · Ising bond variable of a two-state coloring

Used byPositive planar percolation at some \(p < 1\) via the Ising model · 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 · Plus-boundary Ising one-point function on a graph · Plus-boundary Ising partition function on a graph

DefinitionPlus-boundary Ising partition function on a graph#✓fully proved

The partition function of the Ising model with + boundary condition on a graph.

noncomputable def isingWiredZ (β : ℝ) : ℝ := ∑ σ : V → Fin 2, isingWiredWeight G bdry β σ

Uses 1 · Used by 6

Statement usesIsing weight of a coloring with plus boundary

Used byPositive planar percolation at some \(p < 1\) via the Ising model · 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 · Plus-boundary Ising one-point function on a graph

DefinitionPlus-boundary Ising one-point function on a graph#✓fully proved

The one-point function ⟨σ_x⟩⁺ of the Ising model with + boundary condition on a graph.

noncomputable def isingWiredOnePoint (β : ℝ) (x : V) : ℝ :=
  (∑ σ : V → Fin 2, isingWiredWeight G bdry β σ * isingSpin (σ x)) / isingWiredZ G bdry β

Uses 3 · Used by 5

Statement usesIsing spin value of a two-state color · Ising weight of a coloring with plus boundary · Plus-boundary Ising partition function on a graph

Used byPositive planar percolation at some \(p < 1\) via the Ising model · 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

B. Lattice configurations as box colorings

DefinitionTwo-state color of a Boolean spin#✓fully proved

The two-state color of a Boolean spin: true ↦ 0, false ↦ 1.

def bToF (b : Bool) : Fin 2 := if b then 0 else 1

Used by 7

Used byPositive planar percolation at some \(p < 1\) via the Ising model · 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 · Box configuration as a coloring of the next larger box · Box configurations as box-graph colorings with boundary color \(0\)

DefinitionBox configuration as a coloring of the next larger box#✓fully proved

A configuration in the box Λ_n as a two-state coloring of Λ_{n+1}, with color 0 (spin +) outside Λ_n.

noncomputable def latToBox (d n : ℕ) (τ : {x // x ∈ box d n} → Bool) :
    boxVerts d (n + 1) → Fin 2 :=
  fun v => if h : (v : Site d) ∈ box d n then bToF (τ ⟨v, h⟩) else 0

Uses 4 · Used by 6

Statement usesVertices of the box \((-n, n)^d\) · Two-state color of a Boolean spin · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byPositive planar percolation at some \(p < 1\) via the Ising model · 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 · Box configurations as box-graph colorings with boundary color \(0\)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.