Onsager's 2D Ising phase transition

AbbreviationSites of the periodic square lattice#✓fully proved

For a positive integer \(L\), the sites of the periodic \(L \times L\) square lattice are the pairs \((i, j)\) with \(i, j \in \mathbb{Z}/L\mathbb{Z}\).

abbrev IsingSite (L : ℕ) [NeZero L] : Type := ZMod L × ZMod L

Used by 4

Used byEnergy of an Ising configuration · Ising partition function · Right neighbour · Upward neighbour

DefinitionNumerical value of a spin#✓fully proved

A spin, recorded as a Boolean, has the real value \(1\) if it is true and \(-1\) if it is false.

def spinValue (b : Bool) : ℝ := if b then 1 else -1

Used by 1

Used byEnergy of an Ising configuration

DefinitionRight neighbour#✓fully proved

For a positive integer \(L\), the right neighbour of a site \((i, j)\) of the periodic \(L \times L\) square lattice is \((i + 1, j)\), with addition in \(\mathbb{Z}/L\mathbb{Z}\).

def rightNeighbour {L : ℕ} [NeZero L] (p : IsingSite L) : IsingSite L :=
  ((p.1 + 1 : ZMod L), p.2)

Uses 1 · Used by 1

Statement usesSites of the periodic square lattice

Used byEnergy of an Ising configuration

DefinitionUpward neighbour#✓fully proved

For a positive integer \(L\), the upward neighbour of a site \((i, j)\) of the periodic \(L \times L\) square lattice is \((i, j + 1)\), with addition in \(\mathbb{Z}/L\mathbb{Z}\).

def upNeighbour {L : ℕ} [NeZero L] (p : IsingSite L) : IsingSite L :=
  (p.1, (p.2 + 1 : ZMod L))

Uses 1 · Used by 1

Statement usesSites of the periodic square lattice

Used byEnergy of an Ising configuration

DefinitionEnergy of an Ising configuration#✓fully proved

For a positive integer \(L\), let \(\sigma\) be a spin configuration on the periodic \(L \times L\) square lattice, assigning to each site \(p\) a spin \(\sigma_p \in \{1, -1\}\). Its energy in the zero-field ferromagnetic Ising model with unit coupling is

\[H_L(\sigma) = -\sum_p \left(\sigma_p \sigma_{p + e_1} + \sigma_p \sigma_{p + e_2}\right),\]

where \(p\) runs over all sites, and \(p + e_1\) and \(p + e_2\) are obtained from \(p\) by adding \(1\) modulo \(L\) to its first and to its second coordinate respectively.

noncomputable def isingEnergy (L : ℕ) [NeZero L] (σ : IsingSite L → Bool) : ℝ :=
  -((∑ p : IsingSite L, spinValue (σ p) * spinValue (σ (rightNeighbour p))) +
      ∑ p : IsingSite L, spinValue (σ p) * spinValue (σ (upNeighbour p)))

Uses 4 · Used by 1

Statement usesSites of the periodic square lattice · Right neighbour · Numerical value of a spin · Upward neighbour

Used byIsing partition function

DefinitionIsing partition function#✓fully proved

For a positive integer \(L\) and real \(\beta\), the partition function of the Ising model on the periodic \(L \times L\) square lattice at inverse temperature \(\beta\) is \(Z_L(\beta) = \sum_\sigma e^{-\beta H_L(\sigma)}\), where \(\sigma\) runs over all spin configurations on the lattice and \(H_L(\sigma)\) is the Ising energy of \(\sigma\).

noncomputable def isingPartitionFunction (L : ℕ) [NeZero L] (β : ℝ) : ℝ :=
  ∑ σ : IsingSite L → Bool, Real.exp (-β * isingEnergy L σ)

Uses 2 · Used by 1

Statement usesSites of the periodic square lattice · Energy of an Ising configuration

Used byFinite-volume Ising free energy density

DefinitionFinite-volume Ising free energy density#✓fully proved

For a positive integer \(L\) and real \(\beta\), the free energy density of the Ising model on the periodic \(L \times L\) square lattice is \(\log Z_L(\beta) / L^2\), where \(Z_L(\beta)\) is the partition function at inverse temperature \(\beta\).

No factor \(-1/\beta\) is included.

noncomputable def finiteIsingFreeEnergy (L : ℕ) [NeZero L] (β : ℝ) : ℝ :=
  Real.log (isingPartitionFunction L β) / (L : ℝ) ^ 2

Uses 1 · Used by 1

Statement usesIsing partition function

Used byIsing free energy density along side lengths \(n + 1\)

DefinitionIsing free energy density along side lengths \(n + 1\)#✓fully proved

For a natural number \(n\) and real \(\beta\), this is the finite-volume free energy density of the Ising model on the periodic \((n + 1) \times (n + 1)\) square lattice at inverse temperature \(\beta\), namely \(\log Z_{n+1}(\beta) / (n + 1)^2\), where \(Z_{n+1}(\beta)\) is the partition function of that lattice at inverse temperature \(\beta\).

noncomputable def finiteIsingFreeEnergySeq (n : ℕ) (β : ℝ) : ℝ :=
  finiteIsingFreeEnergy (n + 1) β

Uses 1 · Used by 1

Statement usesFinite-volume Ising free energy density

Used byOnsager's phase transition for the two-dimensional Ising model

TheoremOnsager's phase transition for the two-dimensional Ising model#●ready to prove

For a positive integer \(L\) and real \(\beta\), let \(Z_L(\beta)\) be the partition function of the zero-field ferromagnetic Ising model on the periodic \(L \times L\) square lattice at inverse temperature \(\beta\). There exist a function \(F : \mathbb{R} \to \mathbb{R}\) and a real number \(\beta_c > 0\) such that, for every real \(\beta\), \(\log Z_{n+1}(\beta) / (n+1)^2\) converges to \(F(\beta)\) as \(n \to \infty\), and \(F\) is not real analytic at \(\beta_c\).

public theorem_wanted ising_2d_phase_transition :
    ∃ (F : ℝ → ℝ) (βc : ℝ),
      0 < βc ∧
        (∀ β : ℝ,
          Tendsto (fun n : ℕ => finiteIsingFreeEnergySeq n β) atTop (𝓝 (F β))) ∧
        ¬ AnalyticAt ℝ F βc

Sources

• L. Onsager, Crystal statistics I, Phys. Rev. 65 (1944). Knill, §158. Problem ising_2d_phase_transition of the lean-eval benchmark.

Uses 1

Statement usesIsing free energy density along side lengths \(n + 1\)

8 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.