Dual circuits through one component of the contour

3 fully proved

A. The component graph of a face

DefinitionFaces of a set reachable from a face in the face-boundary graph#✓fully proved

The faces of T reachable from f in the face-boundary graph of K.

noncomputable def componentSupport (K : Set (Site 2)) (T : Finset (Site 2)) (f : Site 2) :
    Finset (Site 2) :=
  T.filter (fun g => (faceBoundaryGraph K).Reachable f g)

Uses 2 · Used by 3

Statement usesSite of the hypercubic lattice · Face-boundary graph of a set

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

DefinitionComponent of a face in the face-boundary graph#✓fully proved

The connected component of the face f in the face-boundary graph of K, as a graph on all faces.

def componentGraph (K : Set (Site 2)) (f : Site 2) : SimpleGraph (Site 2) where
  Adj a b := (faceBoundaryGraph K).Adj a b ∧ (faceBoundaryGraph K).Reachable f a ∧
    (faceBoundaryGraph K).Reachable f b
  symm := by
    refine ⟨?_⟩
    rintro a b ⟨hadj, hra, hrb⟩
    exact ⟨hadj.symm, hrb, hra⟩
  loopless := by
    refine ⟨fun a => ?_⟩
    rintro ⟨hadj, _, _⟩
    exact (faceBoundaryGraph K).irrefl hadj

Uses 2 · Used by 6

Statement usesSite of the hypercubic lattice · Face-boundary graph of a set

Used byTight axis circuit data: contour edges in one axis-face component · Hole-free connected cluster through the origin · Winding hypothesis for outer contours on \(\mathbb{Z}^2\) · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

C. Tight circuit data and the Peierls count

DefinitionTight axis circuit data: contour edges in one axis-face component#✓fully proved

Every realised contour of length ℓ in Λ_n ⊆ ℤ² is the contour of a cluster whose face-boundary graph has all its edges in the component of an axis face (j, 0) with j < ℓ.

def TightAxisCircuitData (n ℓ : ℕ) : Prop :=
  ∀ F ∈ realisedContours 2 n ℓ,
    ∃ K : Finset (Site 2), (↑K : Set (Site 2)) ⊆ box 2 n ∧
      crossEdges (↑K : Set (Site 2)) (bondFinsetTouch 2 n) = F ∧
      contourLen (↑K : Set (Site 2)) (bondFinsetTouch 2 n) = ℓ ∧
      ∃ (T : Finset (Site 2)) (j : ℕ),
        (faceBoundaryGraph (↑K : Set (Site 2))).support ⊆ (T : Set (Site 2)) ∧
        j < ℓ ∧ axisVertex 2 j ∈ T ∧
        (∀ e ∈ (faceBoundaryGraph (↑K : Set (Site 2))).edgeSet,
          e ∈ (componentGraph (↑K : Set (Site 2)) (axisVertex 2 j)).edgeSet)

Uses 9

Statement usesBonds touching the box · Contour length of a set · Contour of a set: bonds crossing its boundary · Site of the hypercubic lattice · Site \((j, 0, \ldots, 0)\) on the first coordinate axis · Box \((-n, n)^d\) in the hypercubic lattice · Component of a face in the face-boundary graph · Face-boundary graph of a set · Contours of length \(\ell\) realised by connected clusters in a box

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.