Skip to content

Dual circuits decode to contours in two dimensions

7 fully proved

A. Primal and dual edges

DefinitionPrimal edge crossed by a dual edge#✓fully proved

The primal edge of ℤ² crossed by the dual edge between the faces f and g, defined symmetrically in f and g. See also sharedPrimalEdge, with which it agrees on adjacent faces (symPrimal_eq_shared).

noncomputable def symPrimal (f g : Site 2) : Sym2 (Site 2) := by
  classical
  exact if f 0 = g 0 then
    s(![f 0, max (f 1) (g 1)], ![f 0 + 1, max (f 1) (g 1)])
  else
    s(![max (f 0) (g 0), min (f 1) (g 1)], ![max (f 0) (g 0), min (f 1) (g 1) + 1])
Uses 1 · Used by 5
Statement usesSite of the hypercubic lattice
Used byPrimal edge crossed by an unordered pair of faces · 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

DefinitionPrimal edge crossed by an unordered pair of faces#✓fully proved

symPrimal on unordered pairs of faces.

noncomputable def symPrimalSym : Sym2 (Site 2) → Sym2 (Site 2) :=
  Sym2.lift ⟨symPrimal, symPrimal_comm⟩
Uses 2 · Used by 5
Statement usesSite of the hypercubic lattice · Primal edge crossed by a dual edge
Used byPrimal edges crossed by a closed dual walk · 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

DefinitionTwo faces flanking a primal edge#✓fully proved

The two faces of ℤ² flanking the primal edge {p, q}.

noncomputable def flankFaces (p q : Site 2) : Sym2 (Site 2) := by
  classical
  exact if p 0 = q 0 then
    s(![p 0 - 1, min (p 1) (q 1)], ![p 0, min (p 1) (q 1)])
  else
    s(![min (p 0) (q 0), min (p 1) (q 1) - 1], ![min (p 0) (q 0), min (p 1) (q 1)])
Uses 1 · Used by 5
Statement usesSite of the hypercubic lattice
Used byTwo faces flanking an unordered pair of sites · 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

DefinitionTwo faces flanking an unordered pair of sites#✓fully proved

flankFaces on unordered pairs of sites.

noncomputable def flankFacesSym : Sym2 (Site 2) → Sym2 (Site 2) :=
  Sym2.lift ⟨flankFaces, flankFaces_comm⟩
Uses 2 · Used by 4
Statement usesSite of the hypercubic lattice · Two faces flanking a primal edge
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

B. Decoding dual circuits

DefinitionPrimal edges crossed by a closed dual walk#✓fully proved

The set of primal edges crossed by a closed dual walk.

noncomputable def dualWalkContour (W : Σ v : Site 2, (hypercubicLattice 2).Walk v v) :
    Finset (Sym2 (Site 2)) :=
  (W.2.edges.map symPrimalSym).toFinset
Uses 3 · Used by 3
Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Primal edge crossed by an unordered pair of faces
Used byPlus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

C. Circuit data and the Peierls count

DefinitionConnected face-boundary graphs at the axis for all realised contours#✓fully proved

Every realised contour of length ℓ in Λ_n ⊆ ℤ² is the contour of a finite cluster whose face-boundary graph is connected on boundarySupport and meets an axis face (j, 0) with j < ℓ. The condition refers to the face set boundarySupport, which is chosen by Classical.choose.

def PeierlsContourCircuitData (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) = ℓ ∧
      ∃ hfin : (↑K : Set (Site 2)).Finite,
        FaceBoundaryConnected (↑K : Set (Site 2)) (boundarySupport hfin) ∧
        ∃ j : ℕ, j < ℓ ∧ axisVertex 2 j ∈ (boundarySupport hfin : Set (Site 2))
Uses 9
Statement usesBonds touching the box · Contour length of a set · Contour of a set: bonds crossing its boundary · Connectedness of the face-boundary graph on a face set · Site of the hypercubic lattice · Site \((j, 0, \ldots, 0)\) on the first coordinate axis · Finite face set containing the face-boundary support · Box \((-n, n)^d\) in the hypercubic lattice · Contours of length \(\ell\) realised by connected clusters in a box

DefinitionConnected face-boundary graphs at the axis for all connected clusters#✓fully proved

Every connected cluster in Λ_n ⊆ ℤ² with contour length ℓ is finite, has face-boundary graph connected on boundarySupport, and meets an axis face (j, 0) with j < ℓ. The condition refers to the face set boundarySupport, which is chosen by Classical.choose; TightAxisCircuitData avoids this choice.

def ContourGeometryResidue (n ℓ : ℕ) : Prop :=
  ∀ K : Finset (Site 2), K ∈ connClusterFamily (d := 2) n →
    contourLen (↑K : Set (Site 2)) (bondFinsetTouch 2 n) = ℓ →
    ∃ hfin : (↑K : Set (Site 2)).Finite,
      FaceBoundaryConnected (↑K : Set (Site 2)) (boundarySupport hfin) ∧
      ∃ j : ℕ, j < ℓ ∧ axisVertex 2 j ∈ (boundarySupport hfin : Set (Site 2))
Uses 7
Statement usesBonds touching the box · Connected clusters in the box containing the origin · Contour length of a set · Connectedness of the face-boundary graph on a face set · Site of the hypercubic lattice · Site \((j, 0, \ldots, 0)\) on the first coordinate axis · Finite face set containing the face-boundary support

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.