The Ising model as the two-state Potts model

3 fully proved

A. Ising configurations as two-state Potts colorings

DefinitionIsing configuration of a two-state Potts coloring#✓fully proved

The Ising configuration of a two-state Potts coloring, via Fin 2 ≃ Bool.

noncomputable def toIsing (σ : V → Fin 2) : ConfigSpace V := fun x => finTwoEquiv (σ x)

Uses 1

Statement usesConfiguration space of a statistical-mechanics model

C. The FK edge parameter

DefinitionIsing inverse temperature of an FK edge parameter#✓fully proved

The Ising inverse temperature -(1/2) log (1 - p) corresponding to the FK edge parameter p. See also pToBeta for general q (pToBeta_two_eq_betaOfP).

noncomputable def betaOfP (p : ℝ) : ℝ := -(1 / 2) * Real.log (1 - p)

Used by 1

Used byInverse-temperature map of the Potts model at \(q = 2\) is the Ising map

DefinitionFK edge parameter of an Ising inverse temperature#✓fully proved

The FK edge parameter p = 1 - e^{-2β} of the Ising model at inverse temperature β. See also betaToP for general q (betaToP_two_eq_pOfBeta).

noncomputable def pOfBeta (β : ℝ) : ℝ := 1 - Real.exp (-2 * β)

Used by 6

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 · FK edge-parameter map of the Potts model at \(q = 2\) is the Ising map

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.