Dual circuits anchored on a coordinate axis

4 fully proved

A. Per-contour circuits

DefinitionClosed-walk decoding of each realised contour from an anchor pool#✓fully proved

Every realised contour of length ℓ is decoded from a closed walk of length ℓ based at a site of a common pool of at most ℓ anchors.

def PerContourDualCircuit (d n ℓ : ℕ) : Prop :=
  ∃ anchorPool : Finset (Site d), anchorPool.card ≤ ℓ ∧
    ∃ decode : (Σ v : Site d, (hypercubicLattice d).Walk v v) → Finset (Sym2 (Site d)),
      ∀ F ∈ realisedContours d n ℓ,
        ∃ v : Site d, v ∈ anchorPool ∧
          ∃ W : (hypercubicLattice d).Walk v v, W.length = ℓ ∧ decode ⟨v, W⟩ = F

Uses 3

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Contours of length \(\ell\) realised by connected clusters in a box

B. Circuits anchored on the axis

DefinitionSite \((j, 0, \ldots, 0)\) on the first coordinate axis#✓fully proved

The site (j, 0, …, 0) on the first coordinate axis.

def axisVertex (d j : ℕ) : Site d := fun i => if i.val = 0 then (j : ℤ) else 0

Uses 1 · Used by 12

Statement usesSite of the hypercubic lattice

Used byFirst \(\ell\) sites of the first coordinate axis · Closed-walk decoding of each realised contour from an axis site · Connected face-boundary graphs at the axis for all connected clusters · Connected face-boundary graphs at the axis for all realised contours · Tight 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\) · Filled-cluster winding hypothesis · Origin-only minus configuration satisfies the filled-cluster data · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionFirst \(\ell\) sites of the first coordinate axis#✓fully proved

The axis sites (j, 0, …, 0) with j < ℓ.

noncomputable def axisAnchorPool (d ℓ : ℕ) : Finset (Site d) :=
  (Finset.range ℓ).image (fun j => axisVertex d j)

Uses 2

Statement usesSite of the hypercubic lattice · Site \((j, 0, \ldots, 0)\) on the first coordinate axis

DefinitionClosed-walk decoding of each realised contour from an axis site#✓fully proved

Every realised contour of length ℓ is decoded from a closed walk of length ℓ based at an axis site (j, 0, …, 0) with j < ℓ.

def AxisContourDualCircuit (d n ℓ : ℕ) : Prop :=
  ∃ decode : (Σ v : Site d, (hypercubicLattice d).Walk v v) → Finset (Sym2 (Site d)),
    ∀ F ∈ realisedContours d n ℓ,
      ∃ j : ℕ, j < ℓ ∧
        ∃ W : (hypercubicLattice d).Walk (axisVertex d j) (axisVertex d j),
          W.length = ℓ ∧ decode ⟨axisVertex d j, W⟩ = F

Uses 4

Statement usesSite of the hypercubic lattice · Site \((j, 0, \ldots, 0)\) on the first coordinate axis · Hypercubic lattice \(\mathbb{Z}^d\) · 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.