Connected dual contours of the singleton and rectangular clusters

3 fully proved

B. The singleton cluster

DefinitionFour faces meeting the origin#✓fully proved

The four faces meeting the origin, which support the contour of {0}.

noncomputable def singletonBoundarySupport : Finset (Site 2) :=
  {![(0:ℤ), 0], ![(-1:ℤ), 0], ![(-1:ℤ), -1], ![(0:ℤ), -1]}

Uses 1 · Used by 1

Statement usesSite of the hypercubic lattice

Used byOrigin-only minus configuration satisfies the filled-cluster data

C.1. The rectangle is a connected cluster

DefinitionRectangle \((0, m) \times (0, n)\) of sites#✓fully proved

The rectangle [0, m] × [0, n] of sites in ℤ².

noncomputable def boxCluster (m n : ℕ) : Finset (Site 2) :=
  (Finset.Icc (0 : ℤ) m ×ˢ Finset.Icc (0 : ℤ) n).image (fun p => ![p.1, p.2])

Uses 1

Statement usesSite of the hypercubic lattice

C.2. The surrounding frame of faces

DefinitionFrame of faces around a rectangle#✓fully proved

The frame of faces just outside the rectangle [0, m] × [0, n], which supports its contour.

noncomputable def boxFrame (m n : ℕ) : Finset (Site 2) :=
  ((Finset.Icc (-1 : ℤ) m).image (fun a => (![a, -1] : Site 2)))
  ∪ ((Finset.Icc (-1 : ℤ) m).image (fun a => (![a, (n:ℤ)] : Site 2)))
  ∪ ((Finset.Icc (-1 : ℤ) n).image (fun b => (![(-1:ℤ), b] : Site 2)))
  ∪ ((Finset.Icc (-1 : ℤ) n).image (fun b => (![(m:ℤ), b] : Site 2)))

Uses 1

Statement usesSite of the hypercubic lattice

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.