Onsager's solution of the two-dimensional Ising model

DefinitionKac-Ward symbol determinant at t = tanh β#✓fully proved

The Kac-Ward symbol determinant (1 + t²)² - 2t(1 - t²)(cos k₁ + cos k₂) at t = tanh β.

noncomputable def ons_symbolDispersion (β k₁ k₂ : ℝ) : ℝ :=
  (1 + Real.tanh β ^ 2) ^ 2 -
    2 * Real.tanh β * (1 - Real.tanh β ^ 2) * (Real.cos k₁ + Real.cos k₂)

Used by 5

Used bySector determinant with boundary phases · Onsager's formula from the spin Kac-Ward identities · Spin Kac-Ward identities from the decorated-torus formal identity · Spin Kac-Ward identities from the edge-weighted root identity · Onsager's formula

• Continuity of Onsager's pressure at the critical point
• The critical point of the square-lattice Ising model
• High-temperature expansion of the Ising partition function
• From the spin Kac-Ward identities to Onsager's formula
• The square-lattice torus
• Onsager's free energy and the torus pressure
• Onsager's solution of the two-dimensional Ising model
• Onsager's 2D Ising phase transition

DefinitionFinite-volume pressure#✓fully proved

The finite-volume pressure log Z_G(β) / |V| (the negative of β times the free energy per site).

noncomputable def ons_pressureFinite (β : ℝ) : ℝ :=
  Real.log (ons_Z G β) / (Fintype.card V : ℝ)

Uses 1 · Used by 5

Statement usesZero-field Ising partition function with unit couplings

Used byTorus pressure sequence of the zero-field Ising model · Finite-volume pressure decomposition for \(\beta \ge 0\) · Onsager's formula from the spin Kac-Ward identities · Pressure decomposition on the \(L \times L\) torus for \(\beta \ge 0\) · Onsager's formula

DefinitionTorus pressure sequence of the zero-field Ising model#✓fully proved

The pressure log Z_L(β) / L² of the zero-field Ising model on the L × L torus, as a sequence in L (set to 0 for L ≤ 2, where the torus graph is not defined).

noncomputable def ons_torusPressureSeq (beta : ℝ) (L : ℕ) : ℝ :=
  if h : 2 < L then
    letI : Fact (2 < L) := ⟨h⟩
    ons_pressureFinite (onsTorusGraph L) beta
  else 0

Uses 3 · Used by 3

Statement usesNearest-neighbor adjacency on the discrete torus · The \(L \times L\) square-lattice torus graph · Finite-volume pressure

Used byOnsager's formula · Onsager's formula from the spin Kac-Ward identities · Onsager's formula

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.