Contours of clusters in a box and closed-walk encodings

3 fully proved

A. Contours of clusters in a box

DefinitionSites reachable from the origin after deleting edges#✓fully proved

The set of sites reachable from the origin in the hypercubic lattice after deleting the edges in F.

noncomputable def regionDel (d : ℕ) (F : Set (Sym2 (Site d))) : Set (Site d) :=
  {x | ((hypercubicLattice d).deleteEdges F).Reachable (origin d) x}

Uses 3

Statement usesOrigin of \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

B. Closed-walk encodings and the Peierls count

DefinitionConnected clusters in a box with contour length \(\ell\)#✓fully proved

The connected clusters in the box Λ_n whose contour has exactly ℓ bonds.

noncomputable def ccb_contourFiber (d n ℓ : ℕ) : Finset (Finset (Site d)) :=
  (connClusterFamily (d := d) n).filter
    (fun (K : Finset (Site d)) => contourLen (↑K) (bondFinsetTouch d n) = ℓ)

Uses 4 · Used by 2

Statement usesBonds touching the box · Connected clusters in the box containing the origin · Contour length of a set · Site of the hypercubic lattice

Used byAnchored closed-walk decoding of cluster contours in \(\mathbb{Z}^2\) · Injective closed-walk encoding of clusters of contour length \(\ell\)

DefinitionInjective closed-walk encoding of clusters of contour length \(\ell\)#✓fully proved

The clusters with contour length ℓ admit an injective encoding by closed lattice walks of length ℓ based at one of at most ℓ anchor sites.

def ccb_ContourEncodingExists (d n ℓ : ℕ) : Prop :=
  ∃ anchors : Finset (Site d),
    anchors.card ≤ ℓ ∧
    ∃ enc : Finset (Site d) → Σ v : Site d, (hypercubicLattice d).Walk v v,
      (∀ K ∈ ccb_contourFiber d n ℓ, (enc K).1 ∈ anchors ∧ (enc K).2.length = ℓ) ∧
      Set.InjOn enc (↑(ccb_contourFiber d n ℓ))

Uses 3

Statement usesSite of the hypercubic lattice · Connected clusters in a box with contour length \(\ell\) · Hypercubic lattice \(\mathbb{Z}^d\)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.