Russo–Seymour–Welsh theory

• Rectangles, crossings, annuli and the box-crossing property on ℤ²
• The left region of a rectangle cut by an open cluster
• Gluing crossings of adjacent rectangles
• Russo–Seymour–Welsh bounds for critical bond percolation on ℤ²

DefinitionSeparating set for a lattice rectangle#✓fully proved

There is a set containing the left side of [α, β] × [c, d] and disjoint from its right side such that every lattice edge of the rectangle crossing its boundary has an endpoint in P.

def ArcSeparatingSet (P : Set (Site 2)) (α β c d : ℤ) : Prop :=
  ∃ S : Set (Site 2),
    (∀ z : Site 2, z ∈ rect α β c d → z 0 = α → z ∈ S) ∧
    (∀ z : Site 2, z ∈ rect α β c d → z 0 = β → z ∉ S) ∧
    (∀ u v : Site 2, u ∈ rect α β c d → v ∈ rect α β c d →
        (hypercubicLattice 2).Adj u v → bdEdge S s(u, v) → u ∈ P ∨ v ∈ P)

Uses 4 · Used by 1

Statement usesSite of the hypercubic lattice · Boundary edge of a set · Hypercubic lattice \(\mathbb{Z}^d\) · Integer rectangle in the plane lattice

Used byOpen vertical crossings separate the sides of a rectangle

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.