Horizontal and vertical crossings meet

DefinitionHorizontal and vertical crossings meet#✓fully proved

For the configuration ω: whenever x_L (left side of [α, β] × [c, d]) is joined to the right side and x_B (bottom of the overlap [m, m'] × [c, d]) is joined to its top, there is a point z of the overlap reached from x_L inside [α, β] × [c, d] and from x_B inside the overlap.

def HVMeetProperty (ω : ConfigSpace (Sym2 (Site 2))) (α β m m' c d : ℤ) : Prop :=
  α ≤ m → m ≤ m' → m' ≤ β →
  ∀ (xL : leftSide α β c d) (yR : rightSide α β c d),
    ConnectedWithin 2 ω (rect α β c d)
      ⟨(xL : Site 2), leftSide_subset xL.2⟩ ⟨(yR : Site 2), rightSide_subset yR.2⟩ →
  ∀ (xB : bottomSide m m' c d) (yT : topSide m m' c d),
    ConnectedWithin 2 ω (rect m m' c d)
      ⟨(xB : Site 2), bottomSide_subset xB.2⟩ ⟨(yT : Site 2), topSide_subset yT.2⟩ →
  ∃ (z : Site 2) (hzO : z ∈ rect m m' c d) (hzH : z ∈ rect α β c d),
    ConnectedWithin 2 ω (rect α β c d)
        ⟨(xL : Site 2), leftSide_subset xL.2⟩ ⟨z, hzH⟩ ∧
    ConnectedWithin 2 ω (rect m m' c d)
        ⟨(xB : Site 2), bottomSide_subset xB.2⟩ ⟨z, hzO⟩

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 · Bottom side of a general lattice rectangle · Left side of a general lattice rectangle · Integer rectangle in the plane lattice · Right side of a general lattice rectangle · Top side of a general lattice rectangle

Used byRSW gluing from side separation

DefinitionOpen cluster inside the overlap rectangle#✓fully proved

The open cluster of x_B inside the overlap rectangle [m, m'] × [c, d].

def overlapComp (ω : ConfigSpace (Sym2 (Site 2))) (m m' c d : ℤ)
    (xB : Site 2) (hxB : xB ∈ rect m m' c d) : Set (Site 2) :=
  {z | ∃ hz : z ∈ rect m m' c d, ConnectedWithin 2 ω (rect m m' c d) ⟨xB, hxB⟩ ⟨z, hz⟩}

Uses 4 · Used by 8

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

Used byOpen vertical crossings separate the sides of a rectangle · Every overlap cluster meets every horizontal crossing · Vertical overlap crossings separate the sides of a rectangle · Vertical overlap crossings meet every horizontal crossing · RSW gluing from side separation · 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

DefinitionEvery overlap cluster meets every horizontal crossing#✓fully proved

For the configuration ω and every point x_B of the overlap [m, m'] × [c, d], every open left–right path of [α, β] × [c, d] meets the open cluster of x_B inside the overlap. For c < d this fails for some ω; see CrossingSeparatesH for the version that only concerns bottom points x_B joined to the top.

def VSeparatesH (ω : ConfigSpace (Sym2 (Site 2))) (α β m m' c d : ℤ) : Prop :=
  α ≤ m → m ≤ m' → m' ≤ β →
  ∀ (xB : Site 2) (hxB : xB ∈ rect m m' c d),
  ∀ (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 5

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Open subgraph induced on a set of sites · Integer rectangle in the plane lattice · Open cluster inside the overlap rectangle

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.