Rectangles, crossings, annuli and the box-crossing property on ℤ²

DefinitionInteger rectangle in the plane lattice#✓fully proved

The rectangle [a, b] × [c, d] in ℤ².

def rect (a b c d : ℤ) : Set (Site 2) :=
  {x | a ≤ x 0 ∧ x 0 ≤ b ∧ c ≤ x 1 ∧ x 1 ≤ d}

Uses 1 · Used by 29

Statement usesSite of the hypercubic lattice

Used byOpen vertical crossings separate the sides of a rectangle · Horizontal and vertical crossings meet · Open cluster inside the overlap rectangle · Every overlap cluster meets every horizontal crossing · Measurability of the overlap connection event · Open connection inside an overlap rectangle · Connection event inside an overlap rectangle · Vertical overlap crossings separate the sides of a rectangle · Vertical overlap crossings meet every horizontal crossing · RSW gluing from side separation · Separating set for a lattice rectangle · Open path from the left side of a rectangle to a point · Left half-crossing event · Measurability of the left half-crossing event · Measurability of the right half-crossing event · Open path from a point to the right side of a rectangle · Right half-crossing event · Bottom side of a general lattice rectangle · Open left–right crossing of a general rectangle · Left side of a general lattice rectangle · Measurability of the left–right crossing event · Measurability of the bottom–top crossing event · Right side of a general lattice rectangle · Top side of a general lattice rectangle · Open bottom–top crossing of a general rectangle · Left region of a rectangle cut by an open cluster · Condition that every left-right crossing meets the open cluster · Rectangle lattice with an open cluster removed · Sites reachable from the left side of a rectangle

TheoremMeasurability of connection inside a set#✓fully proved

The event that two vertices are connected by an open path inside S is measurable.

theorem measurableSet_connectedWithin {d : ℕ} (S : Set (Site d)) (x y : S) :
    MeasurableSet {ω : ConfigSpace (Sym2 (Site d)) | ConnectedWithin d ω S x y}

Uses 6 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Connection by an open path within a set · Site of the hypercubic lattice

Proof usesHypercubic lattice \(\mathbb{Z}^d\) · Open subgraph of a bond configuration · Open subgraph induced on a set of sites

Used byMeasurability of the overlap connection event · Measurability of the left half-crossing event · Measurability of the right half-crossing event · Measurability of the left–right crossing event · Measurability of the bottom–top crossing event

DefinitionLeft side of a general lattice rectangle#✓fully proved

The left side {a} × [c, d] of rect a b c d.

def leftSide (a b c d : ℤ) : Set (Site 2) := {x | x ∈ rect a b c d ∧ x 0 = a}

Uses 2 · Used by 6

Statement usesSite of the hypercubic lattice · Integer rectangle in the plane lattice

Used byHorizontal and vertical crossings meet · RSW gluing from side separation · Open path from the left side of a rectangle to a point · Measurability of the left half-crossing event · Open left–right crossing of a general rectangle · Measurability of the left–right crossing event

DefinitionRight side of a general lattice rectangle#✓fully proved

The right side {b} × [c, d] of rect a b c d.

def rightSide (a b c d : ℤ) : Set (Site 2) := {x | x ∈ rect a b c d ∧ x 0 = b}

Uses 2 · Used by 6

Statement usesSite of the hypercubic lattice · Integer rectangle in the plane lattice

Used byHorizontal and vertical crossings meet · RSW gluing from side separation · Measurability of the right half-crossing event · Open path from a point to the right side of a rectangle · Open left–right crossing of a general rectangle · Measurability of the left–right crossing event

DefinitionBottom side of a general lattice rectangle#✓fully proved

The bottom side [a, b] × {c} of rect a b c d.

def bottomSide (a b c d : ℤ) : Set (Site 2) := {x | x ∈ rect a b c d ∧ x 1 = c}

Uses 2 · Used by 7

Statement usesSite of the hypercubic lattice · Integer rectangle in the plane lattice

Used byOpen vertical crossings separate the sides of a rectangle · Horizontal and vertical crossings meet · Vertical overlap crossings separate the sides of a rectangle · Vertical overlap crossings meet every horizontal crossing · RSW gluing from side separation · Measurability of the bottom–top crossing event · Open bottom–top crossing of a general rectangle

DefinitionTop side of a general lattice rectangle#✓fully proved

The top side [a, b] × {d} of rect a b c d.

def topSide (a b c d : ℤ) : Set (Site 2) := {x | x ∈ rect a b c d ∧ x 1 = d}

Uses 2 · Used by 7

Statement usesSite of the hypercubic lattice · Integer rectangle in the plane lattice

Used byOpen vertical crossings separate the sides of a rectangle · Horizontal and vertical crossings meet · Vertical overlap crossings separate the sides of a rectangle · Vertical overlap crossings meet every horizontal crossing · RSW gluing from side separation · Measurability of the bottom–top crossing event · Open bottom–top crossing of a general rectangle

DefinitionOpen left–right crossing of a general rectangle#✓fully proved

An open left–right crossing of rect a b c d by a path inside the rectangle.

def HorizontalCrossing (ω : ConfigSpace (Sym2 (Site 2))) (a b c d : ℤ) : Prop :=
  ∃ (x : leftSide a b c d) (y : rightSide a b c d),
    ConnectedWithin 2 ω (rect a b c d)
      ⟨(x : Site 2), leftSide_subset x.2⟩ ⟨(y : Site 2), rightSide_subset y.2⟩

Uses 6 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Connection by an open path within a set · Site of the hypercubic lattice · Left side of a general lattice rectangle · Integer rectangle in the plane lattice · Right side of a general lattice rectangle

Used byGluing horizontal crossings through a vertical overlap crossing · RSW gluing from side separation · Dual left–right crossing of a rectangle · Left–right crossing event of a general rectangle

DefinitionOpen bottom–top crossing of a general rectangle#✓fully proved

An open bottom–top crossing of rect a b c d by a path inside the rectangle.

def VerticalCrossing (ω : ConfigSpace (Sym2 (Site 2))) (a b c d : ℤ) : Prop :=
  ∃ (x : bottomSide a b c d) (y : topSide a b c d),
    ConnectedWithin 2 ω (rect a b c d)
      ⟨(x : Site 2), bottomSide_subset x.2⟩ ⟨(y : Site 2), topSide_subset y.2⟩

Uses 6 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Connection by an open path within a set · Site of the hypercubic lattice · Bottom side of a general lattice rectangle · Integer rectangle in the plane lattice · Top side of a general lattice rectangle

Used byGluing horizontal crossings through a vertical overlap crossing · RSW gluing from side separation · Dual bottom–top crossing of a rectangle · Bottom–top crossing event of a general rectangle

DefinitionLeft–right crossing event of a general rectangle#✓fully proved

The event that rect a b c d has an open left–right crossing.

def horizontalCrossingEvent (a b c d : ℤ) : Set (ConfigSpace (Sym2 (Site 2))) :=
  {ω | HorizontalCrossing ω a b c d}

Uses 3 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Open left–right crossing of a general rectangle

Used byRSW gluing from side separation · Left–right crossing event of a box with given aspect ratio · Measurability of the left–right crossing event

DefinitionBottom–top crossing event of a general rectangle#✓fully proved

The event that rect a b c d has an open bottom–top crossing.

def verticalCrossingEvent (a b c d : ℤ) : Set (ConfigSpace (Sym2 (Site 2))) :=
  {ω | VerticalCrossing ω a b c d}

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Open bottom–top crossing of a general rectangle

Used byRSW gluing from side separation · Measurability of the bottom–top crossing event

TheoremMeasurability of the left–right crossing event#✓fully proved

A left–right crossing event of a rectangle is measurable.

theorem measurableSet_horizontalCrossingEvent (a b c d : ℤ) :
    MeasurableSet (horizontalCrossingEvent a b c d)

Uses 8 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Left–right crossing event of a general rectangle

Proof usesConnection by an open path within a set · Left side of a general lattice rectangle · Measurability of connection inside a set · Integer rectangle in the plane lattice · Right side of a general lattice rectangle

Used byRSW gluing from side separation

TheoremMeasurability of the bottom–top crossing event#✓fully proved

A bottom–top crossing event of a rectangle is measurable.

theorem measurableSet_verticalCrossingEvent (a b c d : ℤ) :
    MeasurableSet (verticalCrossingEvent a b c d)

Uses 8 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Bottom–top crossing event of a general rectangle

Proof usesConnection by an open path within a set · Bottom side of a general lattice rectangle · Measurability of connection inside a set · Integer rectangle in the plane lattice · Top side of a general lattice rectangle

Used byRSW gluing from side separation

DefinitionDual left–right crossing of a rectangle#✓fully proved

A left–right crossing of rect a b c d in the dual configuration dualConfig ω (an open crossing of the dual lattice, read through the primal coordinates of dualConfig).

def DualHorizontalCrossing (ω : ConfigSpace (Sym2 (Site 2))) (a b c d : ℤ) : Prop :=
  HorizontalCrossing (dualConfig ω) a b c d

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Rotated dual configuration · Open left–right crossing of a general rectangle

Used byDual left–right crossing event

DefinitionDual bottom–top crossing of a rectangle#✓fully proved

A bottom–top crossing of rect a b c d in the dual configuration dualConfig ω.

def DualVerticalCrossing (ω : ConfigSpace (Sym2 (Site 2))) (a b c d : ℤ) : Prop :=
  VerticalCrossing (dualConfig ω) a b c d

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Rotated dual configuration · Open bottom–top crossing of a general rectangle

Used byDual bottom–top crossing event

DefinitionDual left–right crossing event#✓fully proved

The event DualHorizontalCrossing.

def dualHorizontalCrossingEvent (a b c d : ℤ) : Set (ConfigSpace (Sym2 (Site 2))) :=
  {ω | DualHorizontalCrossing ω a b c d}

Uses 3

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Dual left–right crossing of a rectangle

DefinitionDual bottom–top crossing event#✓fully proved

The event DualVerticalCrossing.

def dualVerticalCrossingEvent (a b c d : ℤ) : Set (ConfigSpace (Sym2 (Site 2))) :=
  {ω | DualVerticalCrossing ω a b c d}

Uses 3

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Dual bottom–top crossing of a rectangle

DefinitionSquare annulus in the plane lattice#✓fully proved

The annulus z + (Λ_{2n} \ Λ_n), where Λ_n = [-n, n]².

def annulus (z : Site 2) (n : ℕ) : Set (Site 2) :=
  (fun x => z + x) '' (box 2 (2 * n) \ box 2 n)

Uses 2 · Used by 1

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

Used byOpen circuit lying in an annulus

DefinitionOpen circuit lying in an annulus#✓fully proved

The closed walk w is an open circuit all of whose vertices lie in annulus z n.

def IsAnnulusCircuit (ω : ConfigSpace (Sym2 (Site 2))) (z : Site 2) (n : ℕ)
    {v : Site 2} (w : (openSubgraph 2 ω).Walk v v) : Prop :=
  IsOpenCircuit 2 ω w ∧ ∀ u ∈ w.support, u ∈ annulus z n

Uses 5 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Open circuit in a bond configuration · Site of the hypercubic lattice · Open subgraph of a bond configuration · Square annulus in the plane lattice

Used byExistence of an open circuit in an annulus

DefinitionExistence of an open circuit in an annulus#✓fully proved

There is an open circuit inside annulus z n.

def AnnulusCircuit (ω : ConfigSpace (Sym2 (Site 2))) (z : Site 2) (n : ℕ) : Prop :=
  ∃ (v : Site 2) (w : (openSubgraph 2 ω).Walk v v), IsAnnulusCircuit ω z n w

Uses 4 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Open subgraph of a bond configuration · Open circuit lying in an annulus

Used byOpen circuit event in an annulus · Open circuit in an annulus centered at the origin

DefinitionOpen circuit event in an annulus#✓fully proved

The event AnnulusCircuit.

def annulusCircuitEvent (z : Site 2) (n : ℕ) : Set (ConfigSpace (Sym2 (Site 2))) :=
  {ω | AnnulusCircuit ω z n}

Uses 3

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Existence of an open circuit in an annulus

DefinitionOpen circuit in an annulus centered at the origin#✓fully proved

There is an open circuit inside the annulus Λ_{2n} \ Λ_n centered at the origin.

def AnnulusCircuit0 (ω : ConfigSpace (Sym2 (Site 2))) (n : ℕ) : Prop :=
  AnnulusCircuit ω (fun _ => 0) n

Uses 3

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Existence of an open circuit in an annulus

DefinitionLeft–right crossing event of a box with given aspect ratio#✓fully proved

The left–right open crossing of the box [0, ⌊αn⌋] × [0, n] (aspect ratio α).

noncomputable def boxCrossingEvent (α : ℝ) (n : ℕ) :
    Set (ConfigSpace (Sym2 (Site 2))) :=
  horizontalCrossingEvent 0 (⌊α * n⌋.toNat) 0 n

Uses 3 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Left–right crossing event of a general rectangle

Used byBox-crossing property for a sequence of measures · Uniform two-sided box-crossing property · Russo–Seymour–Welsh theorem

DefinitionBox-crossing property for a sequence of measures#✓fully proved

The box-crossing property for a sequence of set functions μ n: for every aspect ratio α > 0 there is c > 0 with μ n (boxCrossingEvent α n) ≥ c for all n.

def P5 (μ : ℕ → Set (ConfigSpace (Sym2 (Site 2))) → ℝ) : Prop :=
  ∀ α : ℝ, 0 < α → ∃ c : ℝ, 0 < c ∧ ∀ n : ℕ, c ≤ μ n (boxCrossingEvent α n)

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Left–right crossing event of a box with given aspect ratio

Used byRusso–Seymour–Welsh theorem

DefinitionUniform two-sided box-crossing property#✓fully proved

The uniform two-sided box-crossing property for a family μ ξ n: for every α > 0 there is c > 0 with c ≤ μ ξ n (boxCrossingEvent α n) ≤ 1 - c for all ξ and n.

def P5c {Ξ : Type*} (μ : Ξ → ℕ → Set (ConfigSpace (Sym2 (Site 2))) → ℝ) : Prop :=
  ∀ α : ℝ, 0 < α → ∃ c : ℝ, 0 < c ∧ ∀ (ξ : Ξ) (n : ℕ),
    c ≤ μ ξ n (boxCrossingEvent α n) ∧ μ ξ n (boxCrossingEvent α n) ≤ 1 - c

Uses 3

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Left–right crossing event of a box with given aspect ratio

24 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.