Injectivity of contours and the reduction to counting contour sets

DefinitionContours of length \(\ell\) realised by connected clusters in a box#✓fully proved

The contours of length ℓ realised by connected clusters in the box Λ_n.

noncomputable def realisedContours (d n ℓ : ℕ) : Finset (Finset (Sym2 (Site d))) :=
  ((connClusterFamily (d := d) n).filter
      (fun K : Finset (Site d) => contourLen (↑K) (bondFinsetTouch d n) = ℓ)).image
    (fun K : Finset (Site d) => crossEdges (↑K : Set (Site d)) (bondFinsetTouch d n))

Uses 5 · Used by 6

Statement usesBonds touching the box · Connected clusters in the box containing the origin · Contour length of a set · Contour of a set: bonds crossing its boundary · Site of the hypercubic lattice

Used byClosed-walk decoding of each realised contour from an axis site · Closed-walk decoding of each realised contour from an anchor pool · Connected face-boundary graphs at the axis for all realised contours · Tight axis circuit data: contour edges in one axis-face component · Peierls counting bound on realised contours of length \(\ell\) · Closed-walk encoding of realised contours of length \(\ell\)

DefinitionPeierls counting bound on realised contours of length \(\ell\)#✓fully proved

The Peierls counting bound: at most ℓ (2d)^ℓ contours of length ℓ are realised by connected clusters in Λ_n.

def ContourSubsetCountBound (d n ℓ : ℕ) : Prop :=
  (realisedContours d n ℓ).card ≤ ℓ * (2 * d) ^ ℓ

Uses 2

Statement usesSite of the hypercubic lattice · Contours of length \(\ell\) realised by connected clusters in a box

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.