Vertical crossings separate the sides of a rectangle

DefinitionVertical overlap crossings meet every horizontal crossing#✓fully proved

For the configuration ω: whenever x_B on the bottom side of the overlap [m, m'] × [c, d] is joined to the top side inside the overlap, every open left–right path of [α, β] × [c, d] meets the open cluster of x_B inside the overlap.

def CrossingSeparatesH (ω : ConfigSpace (Sym2 (Site 2))) (α β m m' c d : ℤ) : Prop :=
  α ≤ m → m ≤ m' → m' ≤ β →
  ∀ (xB : Site 2) (hxB : xB ∈ rect m m' c d),
  xB ∈ bottomSide m m' c d →
  ∀ (yT : Site 2) (hyT : yT ∈ topSide m m' c d),
  ConnectedWithin 2 ω (rect m m' c d) ⟨xB, hxB⟩ ⟨yT, topSide_subset hyT⟩ →
  ∀ (x y : rect α β c d), (x : Site 2) 0 = α → (y : Site 2) 0 = β →
  ∀ (w : (openSubgraphInduce 2 ω (rect α β c d)).Walk x y),
    ∃ z ∈ w.support, (z : Site 2) ∈ overlapComp ω m m' c d xB hxB

Uses 8 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Connection by an open path within a set · Site of the hypercubic lattice · Open subgraph induced on a set of sites · Bottom side of a general lattice rectangle · Integer rectangle in the plane lattice · Top side of a general lattice rectangle · Open cluster inside the overlap rectangle

Used byRSW gluing from side separation

DefinitionVertical overlap crossings separate the sides of a rectangle#✓fully proved

For the configuration ω: whenever x_B on the bottom of the overlap is joined to its top, there is a set L containing the left side of [α, β] × [c, d] and disjoint from its right side such that every lattice edge of the rectangle crossing the boundary of L has an endpoint in the open cluster of x_B inside the overlap.

def CrossingArcSides (ω : ConfigSpace (Sym2 (Site 2))) (α β m m' c d : ℤ) : Prop :=
  α ≤ m → m ≤ m' → m' ≤ β →
  ∀ (xB : Site 2) (hxB : xB ∈ rect m m' c d),
  xB ∈ bottomSide m m' c d →
  ∀ (yT : Site 2) (hyT : yT ∈ topSide m m' c d),
  ConnectedWithin 2 ω (rect m m' c d) ⟨xB, hxB⟩ ⟨yT, topSide_subset hyT⟩ →
  ∃ L : Set (Site 2),
    (∀ z : Site 2, z ∈ rect α β c d → z 0 = α → z ∈ L) ∧
    (∀ z : Site 2, z ∈ rect α β c d → z 0 = β → z ∉ L) ∧
    (∀ u v : Site 2, u ∈ rect α β c d → v ∈ rect α β c d →
        (hypercubicLattice 2).Adj u v → bdEdge L s(u, v) →
        u ∈ overlapComp ω m m' c d xB hxB ∨ v ∈ overlapComp ω m m' c d xB hxB)

Uses 9 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Connection by an open path within a set · Site of the hypercubic lattice · Boundary edge of a set · Hypercubic lattice \(\mathbb{Z}^d\) · Bottom side of a general lattice rectangle · Integer rectangle in the plane lattice · Top side of a general lattice rectangle · Open cluster inside the overlap rectangle

Used byOpen vertical crossings separate the sides of a rectangle · RSW gluing from side separation

TheoremRSW gluing from side separation#✓fully proved

RSW gluing: for a positively associated probability measure μ, if CrossingArcSides holds for every configuration, then μ(H_{[a, m']}) μ(V_{[m, m']}) μ(H_{[m, b]}) ≤ μ(H_{[a, b]}).

theorem rsw_strip_glue_of_crossingArcSides (μ : Measure (ConfigSpace (Sym2 (Site 2))))
    [IsProbabilityMeasure μ] (hpa : PositivelyAssociated μ)
    {a m m' b c d : ℤ} (ham : a ≤ m) (hmm' : m ≤ m') (hm'b : m' ≤ b)
    (harcL : ∀ ω, CrossingArcSides ω a m' m m' c d)
    (harcR : ∀ ω, CrossingArcSides ω m b m m' c d) :
    μ.real (horizontalCrossingEvent a m' c d)
        * μ.real (verticalCrossingEvent m m' c d)
        * μ.real (horizontalCrossingEvent m b c d)
      ≤ μ.real (horizontalCrossingEvent a b c d)

Uses 31

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Left–right crossing event of a general rectangle · Bottom–top crossing event of a general rectangle · Vertical overlap crossings separate the sides of a rectangle · Positively associated measure

Proof usesIncreasing event · Intersection of two increasing events is increasing · Connection by an open path within a set · Boundary edge of a set · Open connection within a set is monotone in the set · Number of boundary crossings of a walk · Hypercubic lattice \(\mathbb{Z}^d\) · Open subgraph induced on a set of sites · Open left–right crossing of a general rectangle · Open bottom–top crossing of a general rectangle · Bottom side of a general lattice rectangle · Left side of a general lattice rectangle · Measurability of the left–right crossing event · Measurability of the bottom–top crossing event · Integer rectangle in the plane lattice · Right side of a general lattice rectangle · Top side of a general lattice rectangle · Monotonicity of the open subgraph in the plane · Vertical overlap crossings meet every horizontal crossing · Gluing horizontal crossings through a vertical overlap crossing · Horizontal and vertical crossings meet · Harris–FKG inequality for a positively associated probability measure · Walk in an induced open subgraph as a lattice walk · Open cluster inside the overlap rectangle · Projection of an induced open subgraph to the lattice

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.