The Potts critical temperature and the FK critical parameter

6 fully proved

A. The FK parametrization

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

The Potts inverse temperature -((q - 1)/q) log (1 - p) corresponding to the FK edge parameter p.

noncomputable def pToBeta (q p : ℝ) : ℝ := -((q - 1) / q) * Real.log (1 - p)

Used by 4

Used byInf-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 · Inverse-temperature map of the Potts model at \(q = 2\) is the Ising map

DefinitionFK edge parameter of a Potts inverse temperature#✓fully proved

The FK edge parameter 1 - e^{-qβ/(q-1)} of the q-state Potts model at inverse temperature β.

noncomputable def betaToP (q β : ℝ) : ℝ := 1 - Real.exp (-(q / (q - 1)) * β)

Used by 1

Used byFK edge-parameter map of the Potts model at \(q = 2\) is the Ising map

LemmaInverse-temperature map of the Potts model at \(q = 2\) is the Ising map#✓fully proved

At q = 2 the general parametrization pToBeta is betaOfP.

lemma pToBeta_two_eq_betaOfP (p : ℝ) : pToBeta 2 p = betaOfP p

Uses 2

Statement usesIsing inverse temperature of an FK edge parameter · Potts inverse temperature of an FK edge parameter

LemmaFK edge-parameter map of the Potts model at \(q = 2\) is the Ising map#✓fully proved

At q = 2 the general parametrization betaToP is pOfBeta.

lemma betaToP_two_eq_pOfBeta (β : ℝ) : betaToP 2 β = pOfBeta β

Uses 2

Statement usesFK edge parameter of a Potts inverse temperature · FK edge parameter of an Ising inverse temperature

B. Critical inverse temperatures

DefinitionCritical inverse temperature of a magnetization curve#✓fully proved

The critical inverse temperature sup {β > 0 : m*(β) = 0} of a spontaneous-magnetization curve m*. See also Ising.betaC, the infimum of the inverse temperatures with positive magnetization.

noncomputable def betaC (mStar : ℝ → ℝ) : ℝ :=
  sSup {β : ℝ | 0 < β ∧ mStar β = 0}

Used by 4

Used byInf-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · 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\) · Critical inverse temperature of the \(d\)-dimensional Ising model

DefinitionCritical inverse temperature of the \(d\)-dimensional Ising model#✓fully proved

The critical inverse temperature of the d-dimensional Ising model, sup {β > 0 : m*(β) = 0}.

noncomputable def isingBetaC (d : ℕ) : ℝ :=
  betaC (Ising.magnetization d)

Uses 2

Statement usesSpontaneous magnetization of the Ising model · Critical inverse temperature of a magnetization curve

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.