Rectangle crossings on the square lattice

DefinitionRectangle at the origin in the plane lattice#✓fully proved

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

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

Uses 1 · Used by 6

Statement usesSite of the hypercubic lattice

Used byBottom side of a rectangle at the origin · Open left–right crossing of a rectangle at the origin · Left side of a rectangle at the origin · Right side of a rectangle at the origin · Top side of a rectangle at the origin · Open bottom–top crossing of a rectangle at the origin

DefinitionLeft side of a rectangle at the origin#✓fully proved

The left side {0} × [0, b] of rectangle a b.

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

Uses 2 · Used by 1

Statement usesSite of the hypercubic lattice · Rectangle at the origin in the plane lattice

Used byOpen left–right crossing of a rectangle at the origin

DefinitionRight side of a rectangle at the origin#✓fully proved

The right side {a} × [0, b] of rectangle a b.

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

Uses 2 · Used by 1

Statement usesSite of the hypercubic lattice · Rectangle at the origin in the plane lattice

Used byOpen left–right crossing of a rectangle at the origin

DefinitionBottom side of a rectangle at the origin#✓fully proved

The bottom side [0, a] × {0} of rectangle a b.

def bottomSide (a b : ℤ) : Set (Site 2) := {x | x ∈ rectangle a b ∧ x 1 = 0}

Uses 2 · Used by 1

Statement usesSite of the hypercubic lattice · Rectangle at the origin in the plane lattice

Used byOpen bottom–top crossing of a rectangle at the origin

DefinitionTop side of a rectangle at the origin#✓fully proved

The top side [0, a] × {b} of rectangle a b.

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

Uses 2 · Used by 1

Statement usesSite of the hypercubic lattice · Rectangle at the origin in the plane lattice

Used byOpen bottom–top crossing of a rectangle at the origin

DefinitionOpen left–right crossing of a rectangle at the origin#✓fully proved

ω has an open left–right crossing of rectangle a b: an open path inside the rectangle from its left side to its right side.

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

Uses 6 · Used by 1

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 rectangle at the origin · Rectangle at the origin in the plane lattice · Right side of a rectangle at the origin

Used byLeft–right crossing event of a rectangle at the origin

DefinitionLeft–right crossing event of a rectangle at the origin#✓fully proved

The event that rectangle a b has an open left–right crossing.

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

Uses 3 · Used by 1

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

Used byLeft–right crossing event of a translated rectangle

DefinitionOpen bottom–top crossing of a rectangle at the origin#✓fully proved

ω has an open bottom–top crossing of rectangle a b: an open path inside the rectangle from its bottom side to its top side.

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

Uses 6 · Used by 1

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 rectangle at the origin · Rectangle at the origin in the plane lattice · Top side of a rectangle at the origin

Used byBottom–top crossing event of a rectangle at the origin

DefinitionBottom–top crossing event of a rectangle at the origin#✓fully proved

The event that rectangle a b has an open bottom–top crossing.

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

Uses 3 · Used by 1

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

Used byBottom–top crossing event of a translated rectangle

TheoremMonotonicity of the open subgraph in the plane#✓fully proved

The open subgraph is monotone in the configuration (d = 2 case of StatMech.Universality.openSubgraph_mono_dim).

theorem openSubgraph_mono {ω ω' : ConfigSpace (Sym2 (Site 2))} (h : ω ≤ ω') :
    openSubgraph 2 ω ≤ openSubgraph 2 ω'

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Open subgraph of a bond configuration

Proof usesHypercubic lattice \(\mathbb{Z}^d\)

Used byRSW gluing from side separation

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.