A connected cluster is determined by its edge boundary

DefinitionEdge with exactly one endpoint in a set#✓fully proved

An edge straddles K if exactly one of its endpoints lies in K.

def edgeStraddles (K : Set (Site d)) (e : Sym2 (Site d)) : Prop := by
  classical
  exact Sym2.lift ⟨fun x y => (x ∈ K ↔ y ∉ K), by
    intro x y
    simp only [eq_iff_iff]
    by_cases hx : x ∈ K <;> by_cases hy : y ∈ K <;> tauto⟩ e

Uses 1 · Used by 6

Statement usesSite of the hypercubic lattice

Used byEdge boundary of a set of sites · Hypercubic lattice with the edge boundary removed · Shift isomorphism: lattice minus barrier edges to face region graph · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionEdge boundary of a set of sites#✓fully proved

The edge boundary ∂K: the lattice edges that straddle K.

def boundaryEdgeSet (K : Set (Site d)) : Set (Sym2 (Site d)) :=
  {e | e ∈ (hypercubicLattice d).edgeSet ∧ edgeStraddles K e}

Uses 3 · Used by 4

Statement usesSite of the hypercubic lattice · Edge with exactly one endpoint in a set · Hypercubic lattice \(\mathbb{Z}^d\)

Used byShift isomorphism: lattice minus barrier edges to face region graph · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionHypercubic lattice with the edge boundary removed#✓fully proved

The hypercubic lattice with the edges straddling K removed.

def latticeMinusBoundary (K : Set (Site d)) : SimpleGraph (Site d) where
  Adj x y := (hypercubicLattice d).Adj x y ∧ ¬ edgeStraddles K s(x, y)
  symm := by
    refine ⟨?_⟩
    intro x y ⟨hadj, hbd⟩
    refine ⟨hadj.symm, ?_⟩
    rwa [← edgeStraddles_comm]
  loopless := ⟨fun x h => (hypercubicLattice d).irrefl h.1⟩

Uses 3 · Used by 3

Statement usesSite of the hypercubic lattice · Edge with exactly one endpoint in a set · Hypercubic lattice \(\mathbb{Z}^d\)

Used byPlus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.