Magnetization equals FK percolation probability, through box graphs

LemmaOrigin lies in every box#✓fully proved

The origin lies in every box. Same statement as Ising.origin_mem_box, which this module does not import.

lemma origin_mem_box_boxVerts (d n : ℕ) : origin d ∈ box d n

Uses 3 · Used by 1

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Origin of the hypercubic lattice

Used byOrigin as a vertex of the box graph

DefinitionOrigin as a vertex of the box graph#✓fully proved

The origin as a vertex of the box graph.

def boxOrigin (d n : ℕ) : boxVerts d n := ⟨origin d, origin_mem_box_boxVerts d n⟩

Uses 5 · Used by 27

Statement usesVertices of the box \((-n, n)^d\) · Origin lies in every box · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Origin of the hypercubic lattice

Used byPositive planar percolation at some \(p < 1\) via the Ising model · Monotonicity in \(p\) of the Bernoulli percolation probability · Wired \(q = 2\) origin-to-boundary probability at most Bernoulli · 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 · Wired box-boundary connection probability is monotone in \(p\) at \(q = 2\) · Wired probability that the origin reaches the box boundary · Event that the box origin connects to the box boundary · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Origin-to-\(\partial\Lambda_n\) event as an event on \(\Lambda_{n+1}\) · A connection to outside the box passes through the box boundary · Boundary connection of \(\Lambda_n\) is a \(\Lambda_m\) cylinder event · Boundary connection inside \(\Lambda_n\) reaches outside \(\Lambda_{n-1}\) · One-step decrease of the events \(0 \leftrightarrow \partial\Lambda_n\) · Open path from the origin out of \(\Lambda_n\) gives \(0 \leftrightarrow \partial\Lambda_n\) inside \(\Lambda_n\) · Box inclusion maps the origin to the origin · Boundary-connection event of \(\Lambda_n\) as an event on \(\Lambda_m\) · Paths to \(\partial\Lambda_{n+1}\) pass through \(\partial\Lambda_n\) · Leaving \(\Lambda_n\) implies connecting to \(\partial\Lambda_n\) · Origin-to-boundary connection is an increasing event · Boundary-connection event of \(\Lambda_n\) on \(\Lambda_m\) is increasing · Cylinder form of the \(\Lambda_n\) boundary connection is measurable · Infinite-volume limit of the wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_k\) · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+1}\) at most in \(\Lambda_n\)

DefinitionWired probability that the origin reaches the box boundary#✓fully proved

The probability φ^w_n(0 ↔ ∂Λ_n) that the origin is connected to the boundary of the box graph of Λ_n under the wired FK measure with q = 2.

noncomputable def boxBoundaryConnProfile (d : ℕ) {p : ℝ} (_hp : 0 < p) (_hp1 : p < 1)
    (_hq : (0 : ℝ) < 2) (n : ℕ) : ℝ :=
  wiredConnToBdryProb (boxGraph d n) (boxBoundary d n) p (boxOrigin d n)

Uses 7 · Used by 7

Statement usesVertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Origin as a vertex of the box graph · Wired random-cluster probability of connecting to the boundary · Site of the hypercubic lattice · Box \((-n, n)^d\) in 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 · Box-boundary profile tends to \(\theta(p,2)\) if wired probabilities do · Ising FK box-boundary connection profile tends to \(\theta^1(p, 2)\)

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.