Phase transition of the Ising model

DefinitionSpin at a site as a bounded continuous function#✓fully proved

The spin at x as a bounded continuous real function on the configuration space.

noncomputable def spinBCF (x : Site d) : ConfigSpace (Site d) →ᵇ ℝ :=
  ⟨⟨fun ω => spin ω x, continuous_spinObs x⟩,
    ⟨2, fun ω ω' => by
      have h1 := spinObs_le_one x ω
      have h2 := spinObs_le_one x ω'
      calc dist (spin ω x) (spin ω' x) ≤ ‖spin ω x‖ + ‖spin ω' x‖ := dist_le_norm_add_norm _ _
        _ ≤ 1 + 1 := by linarith
        _ = 2 := by ring⟩⟩

Uses 3 · Used by 10

Statement usesConfiguration space of a statistical-mechanics model · Spin of a configuration at a site · Site of the hypercubic lattice

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 · Peierls' theorem · Mean-field lower bound for the spontaneous magnetization · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Spin pair product as a bounded continuous function

LemmaMeasurability of the spin at a site#✓fully proved

The spin at a site is a measurable function of the configuration.

lemma measurable_spin (x : Site d) :
    Measurable (fun ω : ConfigSpace (Site d) => spin ω x)

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Spin of a configuration at a site · Site of the hypercubic lattice

Used byIntegrability of the spin at a site under finite measures

LemmaIntegrability of the spin at a site under finite measures#✓fully proved

The spin at a site is integrable for every finite measure.

lemma integrable_spin (x : Site d) (μ : Measure (ConfigSpace (Site d)))
    [IsFiniteMeasure μ] :
    Integrable (fun ω : ConfigSpace (Site d) => spin ω x) μ

Uses 4 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Spin of a configuration at a site · Site of the hypercubic lattice

Proof usesMeasurability of the spin at a site

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

DefinitionSpontaneous magnetization of the Ising model#✓fully proved

The spontaneous magnetization m*(β) = ⟨σ_0⟩⁺_β: the expected spin at the origin under the zero-field plus state.

noncomputable def magnetization (d : ℕ) (β : ℝ) : ℝ :=
  ∫ ω, spin ω (origin d) ∂(plusState d β 0 : Measure (ConfigSpace (Site d)))

Uses 5 · Used by 12

Statement usesConfiguration space of a statistical-mechanics model · Infinite-volume plus state as a subsequential weak limit · Spin of a configuration at a site · Site of the hypercubic lattice · Origin of the hypercubic lattice

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 \(\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\) · Existence of the Ising phase transition · Inverse temperatures with positive spontaneous magnetization · Peierls' theorem · Critical inverse temperature of the \(d\)-dimensional Ising model · Mean-field lower bound for the spontaneous magnetization · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\)

DefinitionInverse temperatures with positive spontaneous magnetization#✓fully proved

The set of inverse temperatures β ≥ 0 at which the spontaneous magnetization is positive.

def positiveMagnetizationSet (d : ℕ) : Set ℝ :=
  {β : ℝ | 0 ≤ β ∧ 0 < magnetization d β}

Uses 1 · Used by 3

Statement usesSpontaneous magnetization of the Ising model

Used byCritical inverse temperature from spontaneous magnetization · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\)

DefinitionCritical inverse temperature from spontaneous magnetization#✓fully proved

The critical inverse temperature β_c(d) = inf {β ≥ 0 | m*(β) > 0} (equal to 0 if the set is empty, by the convention sInf ∅ = 0).

noncomputable def betaC (d : ℕ) : ℝ :=
  sInf (positiveMagnetizationSet d)

Uses 1 · Used by 3

Statement usesInverse temperatures with positive spontaneous magnetization

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\) · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\)

TheoremPeierls' theorem#✓fully proved

The two-dimensional Ising model has positive spontaneous magnetization at some inverse temperature (Peierls, On Ising's model of ferromagnetism, 1936; Griffiths, Phys. Rev. 136 (1964)).

theorem pup_exists_positive_magnetization :
    ∃ β > 0, 0 < magnetization 2 β

Uses 121 · Used by 5

Statement usesSpontaneous magnetization of the Ising model

Proof usesConfiguration space of a statistical-mechanics model · Contour event of a set: opposite spins across every crossing bond · Infinite-volume state of a sequence of measures · Connected cluster through the origin in the nearest-neighbour graph · Hole-free connected cluster through the origin · Filled-cluster winding hypothesis · Winding hypothesis for outer contours on \(\mathbb{Z}^2\) · Bond variable of an unordered pair · Bonds touching the box · Ordered nearest-neighbour pairs touching the box · Box \((-n, n)^d\) as a finite set of sites · Cluster family: all subsets of the box · Connected clusters in the box containing the origin · Contour length of a set · Bond variable of a crossing bond · Contour of a set: bonds crossing its boundary · Bond crossing the boundary of a set · Existence of infinite-volume states · Inside configuration with the spins in a set flipped · Flipping spins in a set as an involutive equivalence · Configuration with the spins in a set flipped · Box energy with a boundary condition · Finite-volume magnetization at the origin · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Finite-volume Gibbs probability with a boundary condition · Finite-volume Boltzmann weight with a boundary condition · Finite-volume partition function with a boundary condition · Configuration glued from inside spins and a boundary condition · Hole-free clusters with contour length \(\ell\) · Hole-free clusters in the box through the origin · Nearest-neighbour graph restricted to a set · Chosen subsequential weak limit of a sequence of measures · Minus cluster of a site · Nearest-neighbour graph on the minus sites · Set of minus sites · Origin of \(\mathbb{Z}^d\) · Exterior component of the complement of a set · Peierls series · Ratio \(2d e^{-2\beta}\) of the Peierls series · All-plus configuration · Plus-boundary Ising measure in a box · Infinite-volume plus state as a subsequential weak limit · Probability of the contour event of a set · Probability that the origin spin is minus · Spin of a configuration at a site · Spin at a site as a bounded continuous function · Set with its holes filled · Filled minus cluster of the origin as a finite set · Twice the Peierls series · Finite-volume plus-boundary magnetization at the origin · Connection by an open path · Euler's theorem for a graph supported on a finite connected set · Connectedness of the face-boundary graph on a face set · Nearest neighbours in \(\mathbb{Z}^d\) · Planar lattice subgraph of the square lattice · Site of the hypercubic lattice · Site on the positive horizontal axis · Site \((j, 0, \ldots, 0)\) on the first coordinate axis · Boundary edge of a set · Boundary indicator of an edge · Base point of the exterior of a box · Edge boundary of a set of sites · Box \((-n, n)^d\) in the hypercubic lattice · Nearest neighbours of a lattice site · Neighbour of a site in a coordinate direction · Edgeless graph has one component per vertex · Removing one element lowers cardinality by one · Open cluster of a site · Component of a face in the face-boundary graph · Faces of a set reachable from a face in the face-boundary graph · Four unit faces at a lattice site · Primal edges crossed by a closed dual walk · Edge boundary of a set of sites · Edge with exactly one endpoint in a set · Face below the exit edge · Face above the exit edge · Exit index of a finite origin cluster · Axis site lies outside the origin cluster · Exterior of a box in \(\mathbb{Z}^d\) · Boundary degree of a unit face · Face-boundary graph of a set · Lower left corner of the unit face at \((a, b)\) · Upper left corner of the unit face at \((a, b)\) · Lower right corner of the unit face at \((a, b)\) · Upper right corner of the unit face at \((a, b)\) · Every finite set of sites lies in a box · Two faces flanking a primal edge · Two faces flanking an unordered pair of sites · Hypercubic lattice \(\mathbb{Z}^d\) · Square lattice is connected · Image of a planar lattice subgraph in the square lattice · Bond configuration open on the edges inside a set · Bounded faces of a finite lattice graph are counted by its cycle rank · Outer face region of a planar lattice subgraph · \(\ell^1\) distance on \(\mathbb{Z}^d\) · Square lattice with the boundary edges of a set removed · Hypercubic lattice with the edge boundary removed · Site on the negative horizontal axis · Face below the left exit edge · Face above the left exit edge · Left exit index of a finite cluster · Left exit condition at an axis site · Cycle rank of a finite graph · Open subgraph of a bond configuration · Radius of a box containing a planar lattice subgraph · Support of the face-boundary graph of a finite set · Shift isomorphism: lattice minus barrier edges to face region graph · Face-boundary graph of a finite set as a planar subgraph · Setting a set of coordinates of a lattice site · Primal edge shared by adjacent faces · Shift of a site along a coordinate · Primal edge crossed by a dual edge · Primal edge crossed by an unordered pair of faces · Face-region graph of a square-lattice subgraph · Faithful discrete Jordan statement for the face count · Number of bounded faces of a lattice subgraph · Anchor sites for dual circuits · Origin of the hypercubic lattice · Weak convergence of probability measures on configuration space · Weak convergence implies convergence of integrals

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

TheoremFK critical point is less than one for \(d \ge 2\), \(q \ge 1\)#✓fully proved

The FK critical point satisfies p_c(d, q) < 1 for d ≥ 2 and q ≥ 1 (Grimmett, The Random-Cluster Model, Theorem 5.5).

theorem fkPc_lt_one_of_two_le {d : ℕ} {q : ℝ} (hd : 2 ≤ d) (hq : 1 ≤ q) :
    fkPc d q < 1

Uses 121

Statement usesCritical parameter \(p_c(q)\) of the random-cluster model

Proof usesConfiguration space of a statistical-mechanics model · Random-cluster probability with a boundary wiring · Boundary clique gives the wired random-cluster measure · Boundary-graph FK measure increases in \(p\) for \(q \ge 1\) · Bernoulli box cylinder probability equals its probability on the box · Event that the box origin connects to the box boundary · Box-boundary connection probability tends to percolation probability · Events \(0 \leftrightarrow \partial\Lambda_n\) decrease in \(n \ge 1\) · One-step decrease of the events \(0 \leftrightarrow \partial\Lambda_n\) · Vertex boundary of a box · Ising FK box-boundary connection profile tends to \(\theta^1(p, 2)\) · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Monotonicity of restriction between boxes · Inclusion of box vertices into the next box · Vertices of the box \((-n, n)^d\) · Number of open edges of a configuration · Connection to the boundary depends only on graph edges · Edges closed in one configuration and open in another · Inclusion of box edges into \(\mathbb{Z}^d\) · Bernoulli edge product · Normalizing constant relating the bond sum to the Potts weight · Edwards–Sokal joint weight · Edwards–Sokal bond sum is a multiple of the Potts weight · Extension of a box configuration by closed edges · Probability of an ambient FK configuration · \(q = 1\) measure equals Bernoulli percolation on graph-edge events · Free–wired domination on a finite graph for \(q \ge 1\) · Non-percolating parameters of the wired random-cluster measure · Wired random-cluster percolation probability \(\theta(p, q)\) · Wired \(q = 2\) percolation probability at most the Bernoulli one · Unnormalized random-cluster weight · At \(q = 1\) the random-cluster weight is the Bernoulli product · Ambient FK normalizer · Holley's inequality · Inclusion of box edges into the next box · Restriction of a next-box configuration to the inner edges · Cylinder events of a box are clopen · Origin-to-boundary connection is an increasing event · Ising spin value of a two-state color · Finite measure with prescribed point masses · Number of open clusters · Cluster count plus open-edge count is monotone · Reduced density \(p/(p + q(1-p))\) · Wired random-cluster measure on a box · Wired random-cluster measure as a probability mass function · Wired random-cluster probability of a configuration · Wired random-cluster weight · Wired random-cluster partition function · Wired infinite-volume random-cluster measure · Wired infinite-volume measure is a subsequential weak limit · Wired infinite-volume boundary connection tends to \(\theta^1(p, q)\) · Wired box measures decrease on inner increasing events for \(q \ge 1\) · Increasing event · Infinite-volume state of a sequence of measures · Bond variable of an unordered pair · Bonds touching the box · Ordered nearest-neighbour pairs touching the box · Box \((-n, n)^d\) as a finite set of sites · Existence of infinite-volume states · Box energy with a boundary condition · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Finite-volume Gibbs probability with a boundary condition · Finite-volume Gibbs measure as a probability measure · Finite-volume Boltzmann weight with a boundary condition · Finite-volume partition function with a boundary condition · Configuration glued from inside spins and a boundary condition · Integrability of the spin at a site under finite measures · Chosen subsequential weak limit of a sequence of measures · Spontaneous magnetization of the Ising model · Origin of \(\mathbb{Z}^d\) · All-plus configuration · Plus-boundary Ising measure in a box · Infinite-volume plus state as a subsequential weak limit · Spin of a configuration at a site · Spin at a site as a bounded continuous function · Coloring fixed to a color on the boundary · Open connection of a vertex to the boundary · Two-state color of a Boolean spin · Wired probability that the origin reaches the box boundary · Origin as a vertex of the box graph · Edwards–Sokal weight with fixed boundary color · Wired Edwards–Sokal one-point function · Edwards–Sokal one-point identity · Total wired Edwards–Sokal weight · Finite-volume plus-boundary magnetization at the origin · Box configurations as box-graph colorings with boundary color \(0\) · Ising bond variable of a two-state coloring · Plus-boundary Ising one-point function on a graph · Ising weight of a coloring with plus boundary · Plus-boundary Ising partition function on a graph · Box configuration as a coloring of the next larger box · FK edge parameter of an Ising inverse temperature · Potts weight with fixed boundary color · Potts partition function with fixed boundary color · Peierls' theorem · Wired random-cluster probability of connecting to the boundary · Site of the hypercubic lattice · Complete graph on the boundary vertices · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Number of open clusters with wired boundary conditions · Inner vertex boundary of a box · Boundary wiring relation · Origin of the hypercubic lattice · Percolation event for the origin · Percolation probability of bond percolation · \(\theta_2(p) \le \theta_{2+k}(p)\) for Bernoulli percolation · Agreement count of a spin configuration · Monochromatic-edge indicator · Potts Boltzmann weight · Stochastic domination of measures on configurations · Stochastic domination compares real-valued masses · Weak convergence of probability measures on configuration space · Weak convergence implies convergence of integrals · Portmanteau theorem for clopen events · Bernoulli distribution on the Booleans · Bernoulli product measure on configuration space

TheoremExistence of the Ising phase transition#✓fully proved

Existence of the Ising phase transition in dimension d ≥ 2: there is β_c > 0 such that the spontaneous magnetization vanishes for 0 < β < β_c and is positive for β > β_c (Peierls, 1936; Griffiths, Phys. Rev. 136 (1964); Duminil-Copin, Lectures on the Ising and Potts models on the hypercubic lattice, 2017). The statement says nothing about β = β_c.

theorem ising_phase_transition_of_two_le {d : ℕ} (hd : 2 ≤ d) :
    ∃ betaC : ℝ, 0 < betaC ∧
      (∀ beta, 0 < beta → beta < betaC → magnetization d beta = 0) ∧
      (∀ beta, betaC < beta → 0 < magnetization d beta)

Uses 105 · Used by 2

Statement usesSpontaneous magnetization of the Ising model

Proof usesConfiguration space of a statistical-mechanics model · Bernoulli box cylinder probability equals its probability on the box · Event that the box origin connects to the box boundary · Wired \(q = 2\) percolation probability as the limit of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_n\) · Box-boundary connection probability tends to percolation probability · Vertex boundary of a box · Ising FK box-boundary connection profile tends to \(\theta^1(p, 2)\) · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Number of open edges of a configuration · Connection to the boundary depends only on graph edges · Edges closed in one configuration and open in another · Inclusion of box edges into \(\mathbb{Z}^d\) · Bernoulli edge product · Normalizing constant relating the bond sum to the Potts weight · Edwards–Sokal joint weight · Edwards–Sokal bond sum is a multiple of the Potts weight · Critical parameter \(p_c(q)\) of the random-cluster model · Positive random-cluster critical point for \(d \ge 2\), \(q \ge 1\) · Probability of an ambient FK configuration · \(q = 1\) measure equals Bernoulli percolation on graph-edge events · Free–wired domination on a finite graph for \(q \ge 1\) · Non-percolating parameters of the wired random-cluster measure · Wired random-cluster percolation probability \(\theta(p, q)\) · Wired \(q = 2\) percolation probability at most the Bernoulli one · Unnormalized random-cluster weight · At \(q = 1\) the random-cluster weight is the Bernoulli product · Ambient FK normalizer · Holley's inequality · Origin-to-boundary connection is an increasing event · Ising spin value of a two-state color · Subcritical parameters are at most the critical point · Finite measure with prescribed point masses · Number of open clusters · Cluster count plus open-edge count is monotone · Reduced density \(p/(p + q(1-p))\) · No percolation below the critical point at \(q = 2\) · Monotonicity of \(\theta^1(p, 2)\) in \(p\) · Wired random-cluster measure on a box · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired random-cluster probability of a configuration · Wired infinite-volume random-cluster measure · Increasing event · Infinite-volume state of a sequence of measures · Bond variable of an unordered pair · Bonds touching the box · Ordered nearest-neighbour pairs touching the box · Box \((-n, n)^d\) as a finite set of sites · Existence of infinite-volume states · Box energy with a boundary condition · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Finite-volume Gibbs probability with a boundary condition · Finite-volume Gibbs measure as a probability measure · Finite-volume Boltzmann weight with a boundary condition · Finite-volume partition function with a boundary condition · Configuration glued from inside spins and a boundary condition · Integrability of the spin at a site under finite measures · Chosen subsequential weak limit of a sequence of measures · Origin of \(\mathbb{Z}^d\) · All-plus configuration · Plus-boundary Ising measure in a box · Infinite-volume plus state as a subsequential weak limit · Spin of a configuration at a site · Spin at a site as a bounded continuous function · Coloring fixed to a color on the boundary · Open connection of a vertex to the boundary · Two-state color of a Boolean spin · Wired probability that the origin reaches the box boundary · Origin as a vertex of the box graph · Edwards–Sokal weight with fixed boundary color · Wired Edwards–Sokal one-point function · Edwards–Sokal one-point identity · Total wired Edwards–Sokal weight · Finite-volume plus-boundary magnetization at the origin · Box configurations as box-graph colorings with boundary color \(0\) · Ising bond variable of a two-state coloring · Plus-boundary Ising one-point function on a graph · Ising weight of a coloring with plus boundary · Plus-boundary Ising partition function on a graph · Box configuration as a coloring of the next larger box · FK edge parameter of an Ising inverse temperature · Potts inverse temperature of an FK edge parameter · Potts weight with fixed boundary color · Potts partition function with fixed boundary color · Peierls' theorem · Wired random-cluster probability of connecting to the boundary · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Inner vertex boundary of a box · Origin of the hypercubic lattice · Percolation event for the origin · Percolation probability of bond percolation · \(\theta_2(p) \le \theta_{2+k}(p)\) for Bernoulli percolation · Agreement count of a spin configuration · Monochromatic-edge indicator · Potts Boltzmann weight · Stochastic domination of measures on configurations · Stochastic domination compares real-valued masses · Weak convergence of probability measures on configuration space · Weak convergence implies convergence of integrals · Bernoulli distribution on the Booleans · Bernoulli product measure on configuration space

Used bySharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\)

TheoremSup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\)#✓fully proved

The sup-based critical inverse temperature IsingFK.betaC (magnetization d) in dimension d ≥ 2 is -(1/2) log (1 - p_c(d, 2)), the image of the FK critical point. This is the supremum of the zero-magnetization inverse temperatures, not yet the public Ising.betaC d (see ising_betaC_eq_sup_betaC_of_two_le for the bridge).

theorem isingFK_betaC_eq_fkPc_of_two_le {d : ℕ} (hd : 2 ≤ d) :
    betaC (magnetization d) = -(1 / 2) * Real.log (1 - fkPc d 2)

Uses 106 · Used by 2

Statement usesCritical parameter \(p_c(q)\) of the random-cluster model · Spontaneous magnetization of the Ising model · Critical inverse temperature of a magnetization curve

Proof usesConfiguration space of a statistical-mechanics model · Bernoulli box cylinder probability equals its probability on the box · Event that the box origin connects to the box boundary · Wired \(q = 2\) percolation probability as the limit of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_n\) · Box-boundary connection probability tends to percolation probability · Vertex boundary of a box · Ising FK box-boundary connection profile tends to \(\theta^1(p, 2)\) · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Number of open edges of a configuration · Connection to the boundary depends only on graph edges · Edges closed in one configuration and open in another · Inclusion of box edges into \(\mathbb{Z}^d\) · Bernoulli edge product · Normalizing constant relating the bond sum to the Potts weight · Edwards–Sokal joint weight · Edwards–Sokal bond sum is a multiple of the Potts weight · Positive random-cluster critical point for \(d \ge 2\), \(q \ge 1\) · Probability of an ambient FK configuration · \(q = 1\) measure equals Bernoulli percolation on graph-edge events · Free–wired domination on a finite graph for \(q \ge 1\) · Non-percolating parameters of the wired random-cluster measure · Wired random-cluster percolation probability \(\theta(p, q)\) · Wired \(q = 2\) percolation probability at most the Bernoulli one · Unnormalized random-cluster weight · At \(q = 1\) the random-cluster weight is the Bernoulli product · Ambient FK normalizer · Holley's inequality · Origin-to-boundary connection is an increasing event · Ising spin value of a two-state color · Subcritical parameters are at most the critical point · Finite measure with prescribed point masses · Number of open clusters · Cluster count plus open-edge count is monotone · Reduced density \(p/(p + q(1-p))\) · No percolation below the critical point at \(q = 2\) · Monotonicity of \(\theta^1(p, 2)\) in \(p\) · Wired random-cluster measure on a box · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired random-cluster probability of a configuration · Wired infinite-volume random-cluster measure · Increasing event · Infinite-volume state of a sequence of measures · Bond variable of an unordered pair · Bonds touching the box · Ordered nearest-neighbour pairs touching the box · Box \((-n, n)^d\) as a finite set of sites · Existence of infinite-volume states · Box energy with a boundary condition · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Finite-volume Gibbs probability with a boundary condition · Finite-volume Gibbs measure as a probability measure · Finite-volume Boltzmann weight with a boundary condition · Finite-volume partition function with a boundary condition · Configuration glued from inside spins and a boundary condition · Integrability of the spin at a site under finite measures · Chosen subsequential weak limit of a sequence of measures · Origin of \(\mathbb{Z}^d\) · All-plus configuration · Plus-boundary Ising measure in a box · Infinite-volume plus state as a subsequential weak limit · Spin of a configuration at a site · Spin at a site as a bounded continuous function · Coloring fixed to a color on the boundary · Open connection of a vertex to the boundary · Two-state color of a Boolean spin · Wired probability that the origin reaches the box boundary · Origin as a vertex of the box graph · Edwards–Sokal weight with fixed boundary color · Wired Edwards–Sokal one-point function · Edwards–Sokal one-point identity · Total wired Edwards–Sokal weight · Finite-volume plus-boundary magnetization at the origin · Box configurations as box-graph colorings with boundary color \(0\) · Ising bond variable of a two-state coloring · Plus-boundary Ising one-point function on a graph · Ising weight of a coloring with plus boundary · Plus-boundary Ising partition function on a graph · Box configuration as a coloring of the next larger box · FK edge parameter of an Ising inverse temperature · Potts inverse temperature of an FK edge parameter · Potts weight with fixed boundary color · Potts partition function with fixed boundary color · Peierls' theorem · Wired random-cluster probability of connecting to the boundary · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Inner vertex boundary of a box · Origin of the hypercubic lattice · Percolation event for the origin · Percolation probability of bond percolation · \(\theta_2(p) \le \theta_{2+k}(p)\) for Bernoulli percolation · Agreement count of a spin configuration · Monochromatic-edge indicator · Potts Boltzmann weight · Stochastic domination of measures on configurations · Stochastic domination compares real-valued masses · Weak convergence of probability measures on configuration space · Weak convergence implies convergence of integrals · Bernoulli distribution on the Booleans · Bernoulli product measure on configuration space

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\)

TheoremInf-based and sup-based Ising critical points agree for \(d \ge 2\)#✓fully proved

Bridge between the two critical-point definitions: the public Ising.betaC d = sInf {β ≥ 0 | m*(β) > 0} equals the sup-based IsingFK.betaC (magnetization d) = sSup {β > 0 | m*(β) = 0} in dimension d ≥ 2. The β = 0 case is not covered by the phase-transition statement (which only speaks about β > 0), so it is settled separately: φ_0({0}) = tanh 0 * … = 0 < 1, hence the plus-state two-point function at β = 0 is summable, hence m*(0) = 0.

theorem ising_betaC_eq_sup_betaC_of_two_le {d : ℕ} (hd : 2 ≤ d) :
    _root_.StatMech.Ising.betaC d = betaC (magnetization d)

Uses 172 · Used by 1

Statement usesCritical inverse temperature from spontaneous magnetization · Spontaneous magnetization of the Ising model · Critical inverse temperature of a magnetization curve

Proof usesConfiguration space of a statistical-mechanics model · Translation-invariant measure on configuration space · Shift of a configuration by a group element · Bernoulli box cylinder probability equals its probability on the box · Event that the box origin connects to the box boundary · Wired \(q = 2\) percolation probability as the limit of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_n\) · Box-boundary connection probability tends to percolation probability · Vertex boundary of a box · Ising FK box-boundary connection profile tends to \(\theta^1(p, 2)\) · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Number of open edges of a configuration · Connection to the boundary depends only on graph edges · Edges closed in one configuration and open in another · Inclusion of box edges into \(\mathbb{Z}^d\) · Bernoulli edge product · Normalizing constant relating the bond sum to the Potts weight · Edwards–Sokal joint weight · Edwards–Sokal bond sum is a multiple of the Potts weight · Critical parameter \(p_c(q)\) of the random-cluster model · Positive random-cluster critical point for \(d \ge 2\), \(q \ge 1\) · Probability of an ambient FK configuration · \(q = 1\) measure equals Bernoulli percolation on graph-edge events · Free–wired domination on a finite graph for \(q \ge 1\) · Non-percolating parameters of the wired random-cluster measure · Wired random-cluster percolation probability \(\theta(p, q)\) · Wired \(q = 2\) percolation probability at most the Bernoulli one · Unnormalized random-cluster weight · At \(q = 1\) the random-cluster weight is the Bernoulli product · Ambient FK normalizer · Event that every coordinate of a finite set is open · Holley's inequality · Origin-to-boundary connection is an increasing event · Ising spin value of a two-state color · Subcritical parameters are at most the critical point · Finite measure with prescribed point masses · Number of open clusters · Cluster count plus open-edge count is monotone · Reduced density \(p/(p + q(1-p))\) · No percolation below the critical point at \(q = 2\) · Monotonicity of \(\theta^1(p, 2)\) in \(p\) · Wired random-cluster measure on a box · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired random-cluster probability of a configuration · Wired infinite-volume random-cluster measure · FKG lattice condition · Increasing event · Infinite-volume state of a sequence of measures · Even subgraph condition on an edge set · Bond variable of an unordered pair · Bonds touching the box · Ordered nearest-neighbour pairs touching the box · Bond variable takes values \(\pm 1\) · Box \((-n, n)^d\) as a finite set of sites · Existence of infinite-volume states · Box energy with a boundary condition · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Finite-volume Gibbs probability with a boundary condition · Finite-volume Gibbs measure as a probability measure · Finite-volume Boltzmann weight with a boundary condition · Finite-volume partition function with a boundary condition · First Griffiths inequality (GKS I) · Configuration glued from inside spins and a boundary condition · Site with its nearest neighbours · Bonds touching a set · Set with its nearest neighbours · Energy on a set with a boundary condition · Configuration glued from a set and a boundary condition · Finite-volume Gibbs measure on a finite set · Finite-volume Gibbs measure with plus boundary condition · Gibbs probability on a set with a boundary condition · Unit vector of \(\mathbb{Z}^d\) · Boltzmann weight on a set with a boundary condition · Partition function on a set with a boundary condition · Number of edges of an edge set incident to a vertex · Integrability of the spin at a site under finite measures · Box sites as a set and as a finite set · Translation invariance of the plus state · Finite-volume Ising expectation · Chosen subsequential weak limit of a sequence of measures · Origin of \(\mathbb{Z}^d\) · All-plus configuration · Plus-boundary Ising measure in a box · Infinite-volume plus state as a subsequential weak limit · Inverse temperatures with positive spontaneous magnetization · Plus-spin indicator at a site as a bounded continuous function · Spin of a configuration at a site · Spin value of a Boolean · Spin at a site as a bounded continuous function · Spin product over a vertex set · Coloring fixed to a color on the boundary · Open connection of a vertex to the boundary · Two-state color of a Boolean spin · Wired probability that the origin reaches the box boundary · Origin as a vertex of the box graph · Edwards–Sokal weight with fixed boundary color · Wired Edwards–Sokal one-point function · Edwards–Sokal one-point identity · Total wired Edwards–Sokal weight · Finite-volume plus-boundary magnetization at the origin · Box configurations as box-graph colorings with boundary color \(0\) · Ising bond variable of a two-state coloring · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Plus-boundary Ising one-point function on a graph · Ising weight of a coloring with plus boundary · Plus-boundary Ising partition function on a graph · Box configuration as a coloring of the next larger box · FK edge parameter of an Ising inverse temperature · Potts inverse temperature of an FK edge parameter · Potts weight with fixed boundary color · Potts partition function with fixed boundary color · Peierls' theorem · Wired random-cluster probability of connecting to the boundary · Nearest neighbours in \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Every finite set of sites lies in a box · Hypercubic lattice \(\mathbb{Z}^d\) · Inner vertex boundary of a box · Oriented edge boundary of a finite lattice set · Origin of the hypercubic lattice · Percolation event for the origin · Percolation probability of bond percolation · \(\theta_2(p) \le \theta_{2+k}(p)\) for Bernoulli percolation · Agreement count of a spin configuration · Monochromatic-edge indicator · Potts Boltzmann weight · Global spin flip · Ghost edges · Graph edges as ghost-graph edges · Embedding of vertices into the ghost graph · Edge set with prescribed odd-degree vertices · Boltzmann weight with couplings · Free origin correlation in a set, extended by zero · Unordered pair inside a set · Correlation function with couplings · Free-boundary zero-field two-point function in a finite set · Induced subgraph of \(\mathbb{Z}^d\) on a finite set · Edge sets with a given boundary · High-temperature source sum · High-temperature weight of an edge set · Partition function with couplings · Duminil-Copin–Tassion quantity \(\varphi_\beta(S)\) for the Ising model · Boundary edges of a finite volume · Field induced by the plus boundary condition · Plus-state two-point function at zero field · Window sum of plus-state correlations · Supremum of plus-state window sums over windows of at most \(n\) sites · Simon–Lieb inequality in the infinite-volume plus state · Simon–Lieb boundary sum in the plus state · Source pair \(\{a\} \triangle \{b\}\) · Spin pair product as a bounded continuous function · Two-point function with couplings · Unit coupling on the edges of a graph · Gibbs expectation with a site field · Two-point function with a site field · Boltzmann weight with a site field · Partition function with a site field · Ghost-graph coupling with a site field · Graph with a ghost vertex joined to every site · Stochastic domination of measures on configurations · Stochastic domination compares real-valued masses · Weak convergence of probability measures on configuration space · Weak convergence implies convergence of integrals · Portmanteau theorem for clopen events · Bernoulli distribution on the Booleans · Bernoulli product measure on configuration space · FKG inequality for increasing events

Used byInf-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\)

TheoremInf-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\)#✓fully proved

The public Ising critical inverse temperature Ising.betaC d in dimension d ≥ 2 is -(1/2) log (1 - p_c(d, 2)), the image of the FK critical point. This is the form usable with ising_sharp_phase_transition, whose β_c is Ising.betaC d.

theorem isingBetaC_eq_fkPc_of_two_le {d : ℕ} (hd : 2 ≤ d) :
    _root_.StatMech.Ising.betaC d = -(1 / 2) * Real.log (1 - fkPc d 2)

Uses 6

Statement usesCritical parameter \(p_c(q)\) of the random-cluster model · Critical inverse temperature from spontaneous magnetization

Proof usesSpontaneous magnetization of the Ising model · Critical inverse temperature of a magnetization curve · Sup-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\)

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.