The left region of a rectangle cut by an open cluster

DefinitionRectangle lattice with an open cluster removed#✓fully proved

The square lattice restricted to the rectangle [α, β] × [c, d], with the open cluster of x_B in the overlap rectangle removed.

noncomputable def boxMinusP (ω : ConfigSpace (Sym2 (Site 2))) (α β m m' c d : ℤ)
    (xB : Site 2) (hxB : xB ∈ rect m m' c d) : SimpleGraph (Site 2) where
  Adj u v := (hypercubicLattice 2).Adj u v ∧ u ∈ rect α β c d ∧ v ∈ rect α β c d ∧
             u ∉ overlapComp ω m m' c d xB hxB ∧ v ∉ overlapComp ω m m' c d xB hxB
  symm := ⟨by intro u v ⟨h1, h2, h3, h4, h5⟩; exact ⟨h1.symm, h3, h2, h5, h4⟩⟩
  loopless := ⟨fun u h => (hypercubicLattice 2).irrefl h.1⟩

Uses 5 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Integer rectangle in the plane lattice · Open cluster inside the overlap rectangle

Used bySites reachable from the left side of a rectangle

DefinitionSites reachable from the left side of a rectangle#✓fully proved

The sites reachable from the left side of [α, β] × [c, d] inside the rectangle without touching the open cluster of x_B in the overlap.

def floodFromLeft (ω : ConfigSpace (Sym2 (Site 2))) (α β m m' c d : ℤ)
    (xB : Site 2) (hxB : xB ∈ rect m m' c d) : Set (Site 2) :=
  {z | ∃ x : Site 2, x ∈ rect α β c d ∧ x 0 = α ∧ x ∉ overlapComp ω m m' c d xB hxB ∧
        (boxMinusP ω α β m m' c d xB hxB).Reachable x z}

Uses 5 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Rectangle lattice with an open cluster removed · Integer rectangle in the plane lattice · Open cluster inside the overlap rectangle

Used byLeft region of a rectangle cut by an open cluster

DefinitionLeft region of a rectangle cut by an open cluster#✓fully proved

The left region: the left side of [α, β] × [c, d] together with floodFromLeft.

def arcS_leftRegion (ω : ConfigSpace (Sym2 (Site 2))) (α β m m' c d : ℤ)
    (xB : Site 2) (hxB : xB ∈ rect m m' c d) : Set (Site 2) :=
  {z | z ∈ rect α β c d ∧ (z 0 = α ∨ z ∈ floodFromLeft ω α β m m' c d xB hxB)}

Uses 4

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Sites reachable from the left side of a rectangle · Integer rectangle in the plane lattice

DefinitionCondition that every left-right crossing meets the open cluster#✓fully proved

Every lattice path inside [α, β] × [c, d] from the left side to the right side meets the open cluster of x_B in the overlap [m, m'] × [c, d]. This fails for some configurations (StatMech.Lattice.tpc_arcS_twoPathsCross_false).

def ArcS_TwoPathsCross (ω : ConfigSpace (Sym2 (Site 2))) (α β m m' c d : ℤ)
    (xB : Site 2) (hxB : xB ∈ rect m m' c d) : Prop :=
  α ≤ m → m ≤ m' → m' ≤ β →
  ∀ (x y : Site 2), x ∈ rect α β c d → y ∈ rect α β c d → x 0 = α → y 0 = β →
  ∀ (γ : (hypercubicLattice 2).Walk x y),
    (∀ z ∈ γ.support, z ∈ rect α β c d) →
    ∃ z ∈ γ.support, z ∈ overlapComp ω m m' c d xB hxB

Uses 5

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Integer rectangle in the plane lattice · Open cluster inside the overlap rectangle

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.