Gluing crossings of adjacent rectangles

DefinitionOpen path from the left side of a rectangle to a point#✓fully proved

An open path inside rect a m c d from its left side to the point z (on its right side).

def LeftHalfCrossing (ω : ConfigSpace (Sym2 (Site 2))) (a m c d : ℤ) (z : Site 2)
    (hz : z ∈ rect a m c d) : Prop :=
  ∃ xL : leftSide a m c d,
    ConnectedWithin 2 ω (rect a m c d) ⟨xL, leftSide_subset xL.2⟩ ⟨z, hz⟩

Uses 5 · 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 general lattice rectangle · Integer rectangle in the plane lattice

Used byLeft half-crossing event

DefinitionOpen path from a point to the right side of a rectangle#✓fully proved

An open path inside rect m b c d from the point z (on its left side) to its right side.

def RightHalfCrossing (ω : ConfigSpace (Sym2 (Site 2))) (m b c d : ℤ) (z : Site 2)
    (hz : z ∈ rect m b c d) : Prop :=
  ∃ yR : rightSide m b c d,
    ConnectedWithin 2 ω (rect m b c d) ⟨z, hz⟩ ⟨yR, rightSide_subset yR.2⟩

Uses 5 · Used by 1

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 · Right side of a general lattice rectangle

Used byRight half-crossing event

DefinitionLeft half-crossing event#✓fully proved

The event LeftHalfCrossing.

def leftHalfCrossingEvent (a m c d : ℤ) (z : Site 2) (hz : z ∈ rect a m c d) :
    Set (ConfigSpace (Sym2 (Site 2))) :=
  {ω | LeftHalfCrossing ω a m c d z hz}

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Integer rectangle in the plane lattice · Open path from the left side of a rectangle to a point

Used byMeasurability of the left half-crossing event

DefinitionRight half-crossing event#✓fully proved

The event RightHalfCrossing.

def rightHalfCrossingEvent (m b c d : ℤ) (z : Site 2) (hz : z ∈ rect m b c d) :
    Set (ConfigSpace (Sym2 (Site 2))) :=
  {ω | RightHalfCrossing ω m b c d z hz}

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Integer rectangle in the plane lattice · Open path from a point to the right side of a rectangle

Used byMeasurability of the right half-crossing event

TheoremMeasurability of the left half-crossing event#✓fully proved

A left half-crossing event is measurable.

theorem measurableSet_leftHalfCrossingEvent (a m c d : ℤ) (z : Site 2)
    (hz : z ∈ rect a m c d) :
    MeasurableSet (leftHalfCrossingEvent a m c d z hz)

Uses 7

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Integer rectangle in the plane lattice · Left half-crossing event

Proof usesConnection by an open path within a set · Left side of a general lattice rectangle · Measurability of connection inside a set

TheoremMeasurability of the right half-crossing event#✓fully proved

A right half-crossing event is measurable.

theorem measurableSet_rightHalfCrossingEvent (m b c d : ℤ) (z : Site 2)
    (hz : z ∈ rect m b c d) :
    MeasurableSet (rightHalfCrossingEvent m b c d z hz)

Uses 7

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Integer rectangle in the plane lattice · Right half-crossing event

Proof usesConnection by an open path within a set · Measurability of connection inside a set · Right side of a general lattice rectangle

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.