Left–right paths cross every column

DefinitionProjection of an induced open subgraph to the lattice#✓fully proved

The graph homomorphism from the open subgraph induced on R to the lattice ℤ² (forgetting R).

def projHom (ω : ConfigSpace (Sym2 (Site 2))) (R : Set (Site 2)) :
    (openSubgraphInduce 2 ω R) →g (hypercubicLattice 2) where
  toFun := fun v => (v : Site 2)
  map_rel' := by
    intro a b hab
    simp only [openSubgraphInduce_adj] at hab
    exact openSubgraph_le ω hab

Uses 5 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Open subgraph of a bond configuration · Open subgraph induced on a set of sites

Used byOpen vertical crossings separate the sides of a rectangle · Walk in an induced open subgraph as a lattice walk · RSW gluing from side separation

DefinitionWalk in an induced open subgraph as a lattice walk#✓fully proved

A walk in the open subgraph induced on R, mapped to a walk in the lattice ℤ².

def liftWalk (ω : ConfigSpace (Sym2 (Site 2))) (R : Set (Site 2)) {x y : R}
    (w : (openSubgraphInduce 2 ω R).Walk x y) :
    (hypercubicLattice 2).Walk (x : Site 2) (y : Site 2) :=
  w.map (projHom ω R)

Uses 5 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Open subgraph induced on a set of sites · Projection of an induced open subgraph to the lattice

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

DefinitionHalf-plane left of a column#✓fully proved

The half-plane {z ∈ ℤ² : z_0 ≤ k}.

def colLeq (k : ℤ) : Set (Site 2) := {z | z 0 ≤ k}

Uses 1

Statement usesSite of the hypercubic lattice

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.