Outer contours on the square lattice

5 fully proved

A. The doubled Peierls series

DefinitionTwice the Peierls series#✓fully proved

Twice the Peierls series.

noncomputable def twoPeierlsBound (d : ℕ) (β : ℝ) : ℝ := 2 * peierlsBound d β

Uses 1 · Used by 3

Statement usesPeierls series

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

B. Outer circuits

DefinitionAssignment of interiors to closed walks of \(\mathbb{Z}^2\)#✓fully proved

An assignment of a set of sites (its interior) to every closed walk of ℤ².

def InteriorAssignment : Type :=
  (u : Site 2) → (hypercubicLattice 2).Walk u u → Finset (Site 2)

Uses 2 · Used by 2

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

Used byOuter contour map: clusters as interiors of boundary circuits · Boltzmann weight of a closed walk in the circuit sum

DefinitionOuter contour map: clusters as interiors of boundary circuits#✓fully proved

Every cluster through the origin is the interior of one of its closed boundary circuits, for some interior assignment.

def OuterContourMap (n : ℕ) : Prop :=
  ∃ interiorOf : InteriorAssignment,


    (∀ (ℓ : ℕ) (u : Site 2) (γ : (hypercubicLattice 2).Walk u u),
        u ∈ anchorFinset ℓ → γ.length = ℓ → γ.IsCycle →
          (↑(interiorOf u γ) : Set (Site 2)) ⊆ box 2 n ∧
          contourLen (↑(interiorOf u γ)) (bondFinsetTouch 2 n) = ℓ) ∧
    (∀ τ : {x // x ∈ box 2 n} → Bool, glue (plusField 2) τ (origin 2) = false →
      ∃ (ℓ : ℕ) (u : Site 2) (γ : (hypercubicLattice 2).Walk u u),
        u ∈ anchorFinset ℓ ∧ γ.length = ℓ ∧ γ.IsCycle ∧
        ContourEvent (↑(interiorOf u γ)) (bondFinsetTouch 2 n) (glue (plusField 2) τ))

Uses 11

Statement usesContour event of a set: opposite spins across every crossing bond · Assignment of interiors to closed walks of \(\mathbb{Z}^2\) · Bonds touching the box · Contour length of a set · Configuration glued from inside spins and a boundary condition · Origin of \(\mathbb{Z}^d\) · All-plus configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Anchor sites for dual circuits

DefinitionCycles of length less than \(M\) based near the origin#✓fully proved

The closed walks of ℤ² of length at most M based near the origin.

noncomputable def poc_circuitFamily (M : ℕ) :
    Finset (Σ _ℓ : ℕ, Σ u : Site 2, (hypercubicLattice 2).Walk u u) :=
  (Finset.range M).sigma (fun ℓ => Percolation.cyclesAtLen ℓ)

Uses 3

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Anchored dual cycles of a given length

DefinitionBoltzmann weight of a closed walk in the circuit sum#✓fully proved

The Boltzmann weight attached to a closed walk in the circuit sum.

noncomputable def poc_circuitSummand (n : ℕ) (β : ℝ) (interiorOf : InteriorAssignment)
    (σ : Σ _ℓ : ℕ, Σ u : Site 2, (hypercubicLattice 2).Walk u u) : ℝ :=
  probContour (↑(interiorOf σ.2.1 σ.2.2)) (plusField 2) n (bondFinsetTouch 2 n) β

Uses 6

Statement usesAssignment of interiors to closed walks of \(\mathbb{Z}^2\) · Bonds touching the box · All-plus configuration · Probability of the contour event of a set · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.