The critical point of the square-lattice Ising model

4 fully proved

A. The Onsager integrand

DefinitionOnsager integrand of the square-lattice Ising model#✓fully proved

The Onsager integrand cosh² 2β - sinh 2β (cos k₁ + cos k₂) at inverse temperature β and momentum (k₁, k₂).

noncomputable def ons_gInt (β k₁ k₂ : ℝ) : ℝ :=
  Real.cosh (2*β)^2 - Real.sinh (2*β) * (Real.cos k₁ + Real.cos k₂)

Used by 4

Used byOnsager's free-energy double integral · Onsager's formula from the spin Kac-Ward identities · Continuity of Onsager's pressure at the critical point · Onsager's formula

DefinitionCritical inverse temperature ½ log(1 + √2) of the square lattice#✓fully proved

The critical inverse temperature β_c = ½ log (1 + √2) of the square-lattice Ising model with unit couplings.

noncomputable def ons_betaC : ℝ := (1/2) * Real.log (1 + Real.sqrt 2)

Used by 7

Used by\(\beta_c\) is the unique positive root of \(\sinh 2\beta = 1\) · Kramers-Wannier critical point · Onsager's formula from the spin Kac-Ward identities · Continuity of Onsager's pressure at the critical point · Kramers-Wannier critical point · β_c is the unique positive solution of sinh 2β = 1 · Onsager's formula

B. The critical inverse temperature

TheoremKramers-Wannier critical point#✓fully proved

sinh 2β_c = 1 (H. A. Kramers and G. H. Wannier, Statistics of the two-dimensional ferromagnet. Part I, 1941).

theorem ons_betaC_sinh : Real.sinh (2 * ons_betaC) = 1

Uses 1 · Used by 5

Statement usesCritical inverse temperature ½ log(1 + √2) of the square lattice

Used byKramers-Wannier critical point · Onsager's formula from the spin Kac-Ward identities · Continuity of Onsager's pressure at the critical point · β_c is the unique positive solution of sinh 2β = 1 · Onsager's formula

Lemmaβ_c is the unique positive solution of sinh 2β = 1#✓fully proved

β_c is the unique positive inverse temperature with sinh 2β = 1, the self-dual point of the Kramers-Wannier duality.

lemma ons_betaC_unique (β : ℝ) (_hβ : 0 < β) :
    Real.sinh (2*β) = 1 ↔ β = ons_betaC

Uses 2 · Used by 3

Statement usesCritical inverse temperature ½ log(1 + √2) of the square lattice

Proof usesKramers-Wannier critical point

Used by\(\beta_c\) is the unique positive root of \(\sinh 2\beta = 1\) · Onsager's formula from the spin Kac-Ward identities · Onsager's formula

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.