Boundary contours in the square lattice

StructureDart of the square lattice#✓fully proved

An oriented edge of the square lattice: a pair of nearest-neighbour sites. This is the same data as Mathlib's SimpleGraph.Dart of hypercubicLattice 2; see StatMech.Lattice.Dart.equivSimpleGraphDart.

structure Dart where
  /-- The site the dart starts at. -/
  tail : Site 2
  /-- The site the dart points to. -/
  head : Site 2
  /-- The tail and head are nearest neighbours. -/
  adj : (hypercubicLattice 2).Adj tail head

Uses 2 · Used by 82

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

Used byTotal turning of a boundary orbit is bounded by its length · Cumulative turn along a boundary-tracing orbit · Successor of a boundary dart · Next boundary dart direction is rotated by the turn · Successor map on boundary darts · Minimal period of a boundary dart · Closed walk around a boundary dart orbit · Successor graph on boundary darts · Direction of a lattice dart · Dart direction after k steps is rotated by the cumulative turn · Base boundary dart of the domino · Downward domino dart at the left site · Leftward domino dart at the left site · Upward domino dart at the left site · Upward domino dart at the right site · Rightward domino dart at the right site · Downward domino dart at the right site · Face loop around the domino · Lattice darts agree with graph darts of the square lattice · Dart correspondence respects reversal · Total turning over the minimal period is divisible by four · Total turning of a closed orbit segment is divisible by four · Boundary darts with heads in one component share an orbit · Boundary dart of a set of sites · Inner corner of a boundary dart · Number of convex corners in a boundary orbit · Dart from a site in a unit direction · Face loop left of one period of a boundary orbit · Minimal-period orbit loop as a lattice walk · No diagonal touch along a boundary orbit · Boundary orbit face loop as a lattice walk · No-pinch condition for a boundary orbit · Orbit saturation by heads connected in the complement · Boundary orbits spread along king moves · Boundary orbit with a full revolution has length at least four · Site reached by a boundary orbit · Orbit saturation at reached sites · Walk along the first iterates of a boundary dart · Reversal of a lattice dart · Number of reflex corners in a boundary orbit · Nontrivial quarter-turn rotations fix no lattice direction · Two darts in the same boundary orbit · Corner balance of a simple lattice polygon · Number of straight steps in a boundary orbit · Total signed turning along a boundary orbit · Quarter turn between consecutive boundary darts modulo 4 · Signed quarter turn between consecutive boundary darts · Boundary orbit making exactly one full revolution · Base boundary dart of the unit cell · Rightward boundary dart of the unit cell · Downward boundary dart of the unit cell · Leftward boundary dart of the unit cell · Upward boundary dart of the unit cell · Face loop around the unit cell · Each face visited once per period by a boundary orbit · Local turn of a boundary orbit at a face · Faces visited by a boundary orbit in one period · \(p_c(\mathbb{Z}^2) < 1\) under a no-pinch hypothesis · Visit times of a boundary orbit to a face · Boundary darts of a component off a closed walk · Facial orbit of a boundary dart · Facial orbits cover the components of the complement · Canonical contour of a finite origin cluster · Darts of the canonical contour · Canonical contour is longer than the exit index · Closed face walk of the canonical contour · Face walk along the first successors of a boundary dart · Primal edges of the canonical contour · Event that every edge of the canonical contour is closed · Unit face to the left of a dart · Face loop of a boundary orbit in the face-boundary graph · Face walk along a boundary orbit · Undirected lattice edge of a dart · Exit dart of a finite origin cluster · Exit dart on the positive horizontal axis · Left and right exit darts lie in the same boundary orbit · Minimal-period face loop of the exit orbit · Face loop of the exit orbit of a finite cluster · Exit dart on the negative horizontal axis · Simplicity of the exit orbit's face walk · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle

DefinitionReversal of a lattice dart#✓fully proved

The dart with tail and head exchanged.

def rev (d : Dart) : Dart where
  tail := d.head
  head := d.tail
  adj := d.adj.symm

Uses 3 · Used by 1

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

Used byDart correspondence respects reversal

DefinitionDirection of a lattice dart#✓fully proved

The direction head - tail of a dart, one of the four unit vectors of ℤ².

def dir (d : Dart) : Site 2 := d.head - d.tail

Uses 2 · Used by 24

Statement usesDart of the square lattice · Site of the hypercubic lattice

Used byTotal turning of a boundary orbit is bounded by its length · Successor of a boundary dart · Next boundary dart direction is rotated by the turn · Successor map on boundary darts · Dart direction after k steps is rotated by the cumulative turn · Face loop around the domino · Total turning of a closed orbit segment is divisible by four · Inner corner of a boundary dart · No-pinch condition for a boundary orbit · Walk along the first iterates of a boundary dart · Nontrivial quarter-turn rotations fix no lattice direction · Quarter turn between consecutive boundary darts modulo 4 · Signed quarter turn between consecutive boundary darts · Face loop around the unit cell · \(p_c(\mathbb{Z}^2) < 1\) under a no-pinch hypothesis · Closed face walk of the canonical contour · Face walk along the first successors of a boundary dart · Unit face to the left of a dart · Face loop of a boundary orbit in the face-boundary graph · Face walk along a boundary orbit · Minimal-period face loop of the exit orbit · Face loop of the exit orbit of a finite cluster · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle

DefinitionLattice darts agree with graph darts of the square lattice#✓fully proved

Lattice darts are exactly Mathlib's darts of the square lattice.

def equivSimpleGraphDart : Dart ≃ (hypercubicLattice 2).Dart where
  toFun d := ⟨(d.tail, d.head), d.adj⟩
  invFun d := ⟨d.fst, d.snd, d.adj⟩
  left_inv _ := rfl
  right_inv _ := rfl

Uses 3 · Used by 1

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

Used byDart correspondence respects reversal

TheoremDart correspondence respects reversal#✓fully proved

Reversing a lattice dart corresponds to SimpleGraph.Dart.symm.

theorem equivSimpleGraphDart_rev (d : Dart) :
    equivSimpleGraphDart d.rev = (equivSimpleGraphDart d).symm

Uses 5

Statement usesDart of the square lattice · Lattice darts agree with graph darts of the square lattice · Reversal of a lattice dart · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Definition\(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)#✓fully proved

The ℓ¹ norm |z 0| + |z 1| of a vector of ℤ².

def unitWt (z : Site 2) : ℕ := ∑ i, (z i).natAbs

Uses 1 · Used by 26

Statement usesSite of the hypercubic lattice

Used bySuccessor of a boundary dart · Next boundary dart direction is rotated by the turn · Successor map on boundary darts · Base boundary dart of the domino · Downward domino dart at the left site · Leftward domino dart at the left site · Upward domino dart at the left site · Upward domino dart at the right site · Rightward domino dart at the right site · Downward domino dart at the right site · Face loop around the domino · Dart from a site in a unit direction · Walk along the first iterates of a boundary dart · Nontrivial quarter-turn rotations fix no lattice direction · Base boundary dart of the unit cell · Rightward boundary dart of the unit cell · Downward boundary dart of the unit cell · Leftward boundary dart of the unit cell · Upward boundary dart of the unit cell · Face loop around the unit cell · \(p_c(\mathbb{Z}^2) < 1\) under a no-pinch hypothesis · Face walk along the first successors of a boundary dart · Face loop of a boundary orbit in the face-boundary graph · Face walk along a boundary orbit · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle

DefinitionDart from a site in a unit direction#✓fully proved

The dart from p to p + g, for a unit vector g.

def mkDart (p g : Site 2) (hg : unitWt g = 1) : Dart where
  tail := p
  head := p + g
  adj := by
    rw [adj_iff_unitWt_sub, show p - (p + g) = -g by abel, unitWt_neg]
    exact hg

Uses 4 · Used by 23

Statement usesDart of the square lattice · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)

Used bySuccessor of a boundary dart · Next boundary dart direction is rotated by the turn · Successor map on boundary darts · Base boundary dart of the domino · Downward domino dart at the left site · Leftward domino dart at the left site · Upward domino dart at the left site · Upward domino dart at the right site · Rightward domino dart at the right site · Downward domino dart at the right site · Face loop around the domino · Walk along the first iterates of a boundary dart · Base boundary dart of the unit cell · Rightward boundary dart of the unit cell · Downward boundary dart of the unit cell · Leftward boundary dart of the unit cell · Upward boundary dart of the unit cell · Face loop around the unit cell · Face walk along the first successors of a boundary dart · Face loop of a boundary orbit in the face-boundary graph · Face walk along a boundary orbit · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle

DefinitionBoundary dart of a set of sites#✓fully proved

e is a boundary dart of K: it points from a site of K to a site outside K.

def IsBoundaryDart (K : Set (Site 2)) (e : Dart) : Prop :=
  e.tail ∈ K ∧ e.head ∉ K

Uses 2 · Used by 43

Statement usesDart of the square lattice · Site of the hypercubic lattice

Used byTotal turning of a boundary orbit is bounded by its length · Successor map on boundary darts · Minimal period of a boundary dart · Closed walk around a boundary dart orbit · Successor graph on boundary darts · Base boundary dart of the domino · Face loop around the domino · Total turning over the minimal period is divisible by four · Boundary darts with heads in one component share an orbit · Face loop left of one period of a boundary orbit · Minimal-period orbit loop as a lattice walk · No diagonal touch along a boundary orbit · Boundary orbit face loop as a lattice walk · No-pinch condition for a boundary orbit · Orbit saturation by heads connected in the complement · Boundary orbits spread along king moves · Boundary orbit with a full revolution has length at least four · Site reached by a boundary orbit · Orbit saturation at reached sites · Walk along the first iterates of a boundary dart · Corner balance of a simple lattice polygon · Boundary orbit making exactly one full revolution · Base boundary dart of the unit cell · Face loop around the unit cell · Each face visited once per period by a boundary orbit · Local turn of a boundary orbit at a face · Faces visited by a boundary orbit in one period · \(p_c(\mathbb{Z}^2) < 1\) under a no-pinch hypothesis · Visit times of a boundary orbit to a face · Boundary darts of a component off a closed walk · Facial orbit of a boundary dart · Canonical contour of a finite origin cluster · Darts of the canonical contour · Canonical contour is longer than the exit index · Closed face walk of the canonical contour · Face walk along the first successors of a boundary dart · Face loop of a boundary orbit in the face-boundary graph · Face walk along a boundary orbit · Exit dart of a finite origin cluster · Minimal-period face loop of the exit orbit · Face loop of the exit orbit of a finite cluster · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle

DefinitionSuccessor of a boundary dart#✓fully proved

The successor of the dart e along the boundary of K. Write r for e.dir rotated clockwise by a quarter turn. If e.head + r ∈ K (a reflex corner of K), the successor shares the head of e; if only e.tail + r ∈ K, it is the translate of e by r; otherwise (a convex corner of K) it starts at e.tail in direction r.

noncomputable def dartNext (K : Set (Site 2)) (e : Dart) : Dart := by
  classical
  exact
    if e.head + (-rot90Fun e.dir) ∈ K then
      mkDart (e.head + (-rot90Fun e.dir)) (rot90Fun e.dir) (unitWt_rot90Fun_dir e)
    else if e.tail + (-rot90Fun e.dir) ∈ K then
      mkDart (e.tail + (-rot90Fun e.dir)) e.dir (unitWt_dir e)
    else
      mkDart e.tail (-rot90Fun e.dir) (unitWt_neg_rot90Fun_dir e)

Uses 7 · Used by 33

Statement usesDart of the square lattice · Direction of a lattice dart · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Dart from a site in a unit direction · Quarter-turn rotation of the square lattice · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)

Used byTotal turning of a boundary orbit is bounded by its length · Cumulative turn along a boundary-tracing orbit · Next boundary dart direction is rotated by the turn · Successor map on boundary darts · Dart direction after k steps is rotated by the cumulative turn · Face loop around the domino · Total turning over the minimal period is divisible by four · Total turning of a closed orbit segment is divisible by four · Boundary darts with heads in one component share an orbit · Number of convex corners in a boundary orbit · Face loop left of one period of a boundary orbit · No diagonal touch along a boundary orbit · No-pinch condition for a boundary orbit · Walk along the first iterates of a boundary dart · Number of reflex corners in a boundary orbit · Two darts in the same boundary orbit · Number of straight steps in a boundary orbit · Total signed turning along a boundary orbit · Face loop around the unit cell · Local turn of a boundary orbit at a face · Faces visited by a boundary orbit in one period · \(p_c(\mathbb{Z}^2) < 1\) under a no-pinch hypothesis · Visit times of a boundary orbit to a face · Darts of the canonical contour · Closed face walk of the canonical contour · Face walk along the first successors of a boundary dart · Face loop of a boundary orbit in the face-boundary graph · Face walk along a boundary orbit · Left and right exit darts lie in the same boundary orbit · Minimal-period face loop of the exit orbit · Simplicity of the exit orbit's face walk · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle

DefinitionSuccessor map on boundary darts#✓fully proved

The successor map restricted to boundary darts of K.

noncomputable def dartNextSub (K : Set (Site 2)) :
    {e : Dart // IsBoundaryDart K e} → {e : Dart // IsBoundaryDart K e} :=
  fun e => ⟨dartNext K e.1, dartNext_isBoundaryDart K e.1 e.2⟩

Uses 9 · Used by 12

Statement usesDart of the square lattice · Direction of a lattice dart · Boundary dart of a set of sites · Site of the hypercubic lattice · Successor of a boundary dart · Hypercubic lattice \(\mathbb{Z}^d\) · Dart from a site in a unit direction · Quarter-turn rotation of the square lattice · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)

Used byMinimal period of a boundary dart · Closed walk around a boundary dart orbit · Successor graph on boundary darts · Total turning over the minimal period is divisible by four · Face loop left of one period of a boundary orbit · Walk along the first iterates of a boundary dart · \(p_c(\mathbb{Z}^2) < 1\) under a no-pinch hypothesis · Closed face walk of the canonical contour · Face loop of a boundary orbit in the face-boundary graph · Minimal-period face loop of the exit orbit · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle

DefinitionSuccessor graph on boundary darts#✓fully proved

The graph on boundary darts of K in which each dart is adjacent to its successor.

noncomputable def dartSuccGraph (K : Set (Site 2)) :
    SimpleGraph {e : Dart // IsBoundaryDart K e} where
  Adj a b := a ≠ b ∧ (dartNextSub K a = b ∨ dartNextSub K b = a)
  symm := ⟨by rintro a b ⟨hne, h⟩; exact ⟨hne.symm, h.symm⟩⟩
  loopless := by refine ⟨?_⟩; rintro a ⟨hne, _⟩; exact hne rfl

Uses 4 · Used by 4

Statement usesDart of the square lattice · Boundary dart of a set of sites · Site of the hypercubic lattice · Successor map on boundary darts

Used byClosed walk around a boundary dart orbit · Walk along the first iterates of a boundary dart · Facial orbit of a boundary dart · Canonical contour of a finite origin cluster

DefinitionWalk along the first iterates of a boundary dart#✓fully proved

The walk a, next a, …, next^[n] a in dartSuccGraph K.

noncomputable def orbitWalkAux (K : Set (Site 2)) (a : {e : Dart // IsBoundaryDart K e}) :
    (n : ℕ) → (dartSuccGraph K).Walk a ((dartNextSub K)^[n] a)
  | 0 => SimpleGraph.Walk.nil
  | (n+1) =>
      (orbitWalkAux K a n).concat (by
        rw [Function.iterate_succ_apply']
        exact dartSuccGraph_adj_next K ((dartNextSub K)^[n] a))

Uses 12 · Used by 1

Statement usesDart of the square lattice · Direction of a lattice dart · Boundary dart of a set of sites · Site of the hypercubic lattice · Successor of a boundary dart · Successor map on boundary darts · Successor graph on boundary darts · Hypercubic lattice \(\mathbb{Z}^d\) · Dart from a site in a unit direction · Quarter-turn rotation as a permutation · Quarter-turn rotation of the square lattice · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)

Used byClosed walk around a boundary dart orbit

DefinitionMinimal period of a boundary dart#✓fully proved

The minimal period of the boundary dart a under the successor map.

noncomputable def dartOrbitPeriod (K : Set (Site 2)) (a : {e : Dart // IsBoundaryDart K e}) :
    ℕ := Function.minimalPeriod (dartNextSub K) a

Uses 4 · Used by 18

Statement usesDart of the square lattice · Boundary dart of a set of sites · Site of the hypercubic lattice · Successor map on boundary darts

Used byTotal turning of a boundary orbit is bounded by its length · Closed walk around a boundary dart orbit · Total turning over the minimal period is divisible by four · Face loop left of one period of a boundary orbit · No diagonal touch along a boundary orbit · No-pinch condition for a boundary orbit · Boundary orbit with a full revolution has length at least four · Corner balance of a simple lattice polygon · Boundary orbit making exactly one full revolution · Faces visited by a boundary orbit in one period · \(p_c(\mathbb{Z}^2) < 1\) under a no-pinch hypothesis · Visit times of a boundary orbit to a face · Darts of the canonical contour · Canonical contour is longer than the exit index · Closed face walk of the canonical contour · Minimal-period face loop of the exit orbit · Simplicity of the exit orbit's face walk · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits

DefinitionClosed walk around a boundary dart orbit#✓fully proved

The closed walk in dartSuccGraph K that runs once around the orbit of a.

noncomputable def dartOrbitWalk (K : Set (Site 2)) (a : {e : Dart // IsBoundaryDart K e}) :
    (dartSuccGraph K).Walk a a :=
  (orbitWalkAux K a (dartOrbitPeriod K a)).copy rfl (dartOrbitPeriod_iterate K a)

Uses 7 · Used by 1

Statement usesDart of the square lattice · Boundary dart of a set of sites · Site of the hypercubic lattice · Successor map on boundary darts · Minimal period of a boundary dart · Successor graph on boundary darts · Walk along the first iterates of a boundary dart

Used byCanonical contour of a finite origin cluster

TheoremIterates up to the minimal period are distinct#✓fully proved

The iterates f^[j] x for 1 ≤ j ≤ minimalPeriod f x are distinct. See also Mathlib's Function.iterate_injOn_Iio_minimalPeriod, the same statement for 0 ≤ j < minimalPeriod f x.

theorem iterate_inj_on_Icc_minimalPeriod {α : Type*} (f : α → α) (x : α) {j k : ℕ}
    (hpos : 0 < Function.minimalPeriod f x)
    (hj1 : 1 ≤ j) (hjp : j ≤ Function.minimalPeriod f x)
    (hk1 : 1 ≤ k) (hkp : k ≤ Function.minimalPeriod f x)
    (h : f^[j] x = f^[k] x) : j = k

DefinitionInner corner of a boundary dart#✓fully proved

The site e.head + r, with r the clockwise rotation of e.dir, lies in K; then the successor of e has the same head.

def IsInnerCorner (K : Set (Site 2)) (e : Dart) : Prop :=
  e.head + (-rot90Fun e.dir) ∈ K

Uses 4

Statement usesDart of the square lattice · Direction of a lattice dart · Site of the hypercubic lattice · Quarter-turn rotation of the square lattice

DefinitionTwo darts in the same boundary orbit#✓fully proved

The dart f is obtained from e by iterating the boundary successor map of K.

def SameOrbit (K : Set (Site 2)) (e f : Dart) : Prop := ∃ n : ℕ, (dartNext K)^[n] e = f

Uses 3 · Used by 3

Statement usesDart of the square lattice · Site of the hypercubic lattice · Successor of a boundary dart

Used byOrbit saturation by heads connected in the complement · Site reached by a boundary orbit · Orbit saturation at reached sites

DefinitionOrbit saturation by heads connected in the complement#✓fully proved

Boundary darts whose heads are connected in Kᶜ lie in the same orbit; a reformulation of StatMech.Lattice.InterfaceConnected.

def OrbitHeadsSaturate (K : Set (Site 2)) : Prop :=
  ∀ (e f : Dart), IsBoundaryDart K e → IsBoundaryDart K f →
    (∀ (he : IsBoundaryDart K e) (hf : IsBoundaryDart K f),
      ((hypercubicLattice 2).induce Kᶜ).Reachable ⟨e.head, he.2⟩ ⟨f.head, hf.2⟩) →
    SameOrbit K e f

Uses 5

Statement usesDart of the square lattice · Boundary dart of a set of sites · Two darts in the same boundary orbit · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

DefinitionKing adjacency on the square lattice#✓fully proved

King adjacency on ℤ²: distinct sites that differ by at most one in each coordinate.

def KingAdj (u v : Site 2) : Prop := u ≠ v ∧ ∀ i, (u i - v i).natAbs ≤ 1

Uses 1 · Used by 2

Statement usesSite of the hypercubic lattice

Used byKing-move graph on the complement of a set · Boundary orbits spread along king moves

DefinitionKing-move graph on the complement of a set#✓fully proved

The graph of king moves on the complement of K.

def boundaryKingGraph (K : Set (Site 2)) : SimpleGraph (↥(Kᶜ : Set (Site 2))) where
  Adj a b := KingAdj (a : Site 2) (b : Site 2)
  symm := ⟨fun _ _ h => h.symm⟩
  loopless := ⟨fun _ h => h.1 rfl⟩

Uses 2 · Used by 1

Statement usesKing adjacency on the square lattice · Site of the hypercubic lattice

Used byLattice connectivity in the complement implies king connectivity

DefinitionSite reached by a boundary orbit#✓fully proved

Some boundary dart in the orbit of e has head v.

def OrbitReached (K : Set (Site 2)) (e : Dart) (v : Site 2) : Prop :=
  ∃ d : Dart, IsBoundaryDart K d ∧ d.head = v ∧ SameOrbit K e d

Uses 4 · Used by 2

Statement usesDart of the square lattice · Boundary dart of a set of sites · Two darts in the same boundary orbit · Site of the hypercubic lattice

Used byBoundary orbits spread along king moves · Orbit saturation at reached sites

DefinitionBoundary orbits spread along king moves#✓fully proved

If the orbit of e reaches a site outside K, it reaches every king neighbour of that site outside K.

def OrbitKingTransport (K : Set (Site 2)) : Prop :=
  ∀ (e : Dart), IsBoundaryDart K e →
    ∀ {u v : Site 2}, u ∉ K → v ∉ K → KingAdj u v →
      OrbitReached K e u → OrbitReached K e v

Uses 5

Statement usesDart of the square lattice · Boundary dart of a set of sites · King adjacency on the square lattice · Site reached by a boundary orbit · Site of the hypercubic lattice

DefinitionOrbit saturation at reached sites#✓fully proved

Every boundary dart whose head is reached by the orbit of e lies in that orbit.

def OrbitVertexSaturate (K : Set (Site 2)) : Prop :=
  ∀ (e : Dart), IsBoundaryDart K e → ∀ {v : Site 2}, OrbitReached K e v →
    ∀ d : Dart, IsBoundaryDart K d → d.head = v → SameOrbit K e d

Uses 5

Statement usesDart of the square lattice · Boundary dart of a set of sites · Site reached by a boundary orbit · Two darts in the same boundary orbit · Site of the hypercubic lattice

DefinitionLattice connectivity in the complement implies king connectivity#✓fully proved

Sites connected by a lattice path in Kᶜ are connected by king moves in Kᶜ.

def BoundaryKingConnected (K : Set (Site 2)) : Prop :=
  ∀ {u w : Site 2} (hu : u ∉ K) (hw : w ∉ K),
    ((hypercubicLattice 2).induce Kᶜ).Reachable ⟨u, hu⟩ ⟨w, hw⟩ →
    (boundaryKingGraph K).Reachable ⟨u, hu⟩ ⟨w, hw⟩

Uses 3

Statement usesSite of the hypercubic lattice · King-move graph on the complement of a set · Hypercubic lattice \(\mathbb{Z}^d\)

DefinitionBoundary darts with heads in one component share an orbit#✓fully proved

Boundary darts of K whose heads lie in the same connected component of Kᶜ lie in the same boundary orbit.

def InterfaceConnected (K : Set (Site 2)) : Prop :=
  ∀ (e f : Dart) (he : IsBoundaryDart K e) (hf : IsBoundaryDart K f),
    ((hypercubicLattice 2).induce Kᶜ).Reachable ⟨e.head, he.2⟩ ⟨f.head, hf.2⟩ →
    ∃ n : ℕ, (dartNext K)^[n] e = f

Uses 5

Statement usesDart of the square lattice · Boundary dart of a set of sites · Site of the hypercubic lattice · Successor of a boundary dart · Hypercubic lattice \(\mathbb{Z}^d\)

DefinitionLower left corner of the unit face at \((a, b)\)#✓fully proved

The lower left corner (a, b) of the unit face [a, a + 1] × [b, b + 1].

def faceCorner00 (a b : ℤ) : Site 2 := ![a, b]

Uses 1 · Used by 21

Statement usesSite of the hypercubic lattice

Used byBoundary degree of a unit face · Bounded faces of a finite lattice graph are counted by its cycle rank · Consecutive left cells on a straight step are face-adjacent · Left and right cells of a step share that step · Three walk edges cannot meet at a vertex · Cells on either side of a step lie in different faces · Shared side of a cell and an adjacent face is an edge · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Face walk along the first successors of a boundary dart · Face walk along a boundary orbit · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · Finite face set containing the face-boundary support · Support of the face-boundary graph of a finite set · Face-boundary graph of a finite set as a planar subgraph · 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 · Finite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit · Finite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings

DefinitionLower right corner of the unit face at \((a, b)\)#✓fully proved

The lower right corner (a + 1, b) of the unit face [a, a + 1] × [b, b + 1].

def faceCorner10 (a b : ℤ) : Site 2 := ![a + 1, b]

Uses 1 · Used by 23

Statement usesSite of the hypercubic lattice

Used byBoundary degree of a unit face · Bounded faces of a finite lattice graph are counted by its cycle rank · Horizontally face-adjacent cells have the same ray parity · Consecutive left cells on a straight step are face-adjacent · Left and right cells of a step share that step · Three walk edges cannot meet at a vertex · Cells on either side of a step lie in different faces · Shared side of a cell and an adjacent face is an edge · Hopf's Umlaufsatz · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Face walk along the first successors of a boundary dart · Face walk along a boundary orbit · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · Finite face set containing the face-boundary support · Support of the face-boundary graph of a finite set · Face-boundary graph of a finite set as a planar subgraph · 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 · Finite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit · Finite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings

DefinitionUpper right corner of the unit face at \((a, b)\)#✓fully proved

The upper right corner (a + 1, b + 1) of the unit face [a, a + 1] × [b, b + 1].

def faceCorner11 (a b : ℤ) : Site 2 := ![a + 1, b + 1]

Uses 1 · Used by 19

Statement usesSite of the hypercubic lattice

Used byBoundary degree of a unit face · Bounded faces of a finite lattice graph are counted by its cycle rank · Horizontally face-adjacent cells have the same ray parity · Vertically face-adjacent cells have the same ray parity · Consecutive left cells on a straight step are face-adjacent · Left and right cells of a step share that step · Cells on either side of a step lie in different faces · Shared side of a cell and an adjacent face is an edge · Hopf's Umlaufsatz · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Finite face set containing the face-boundary support · Support of the face-boundary graph of a finite set · Face-boundary graph of a finite set as a planar subgraph · 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 · Finite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit · Finite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings

DefinitionUpper left corner of the unit face at \((a, b)\)#✓fully proved

The upper left corner (a, b + 1) of the unit face [a, a + 1] × [b, b + 1].

def faceCorner01 (a b : ℤ) : Site 2 := ![a, b + 1]

Uses 1 · Used by 23

Statement usesSite of the hypercubic lattice

Used byBoundary degree of a unit face · Bounded faces of a finite lattice graph are counted by its cycle rank · Vertically face-adjacent cells have the same ray parity · Consecutive left cells on a straight step are face-adjacent · Left and right cells of a step share that step · Three walk edges cannot meet at a vertex · Cells on either side of a step lie in different faces · Shared side of a cell and an adjacent face is an edge · Hopf's Umlaufsatz · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Face walk along the first successors of a boundary dart · Face walk along a boundary orbit · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · Finite face set containing the face-boundary support · Support of the face-boundary graph of a finite set · Face-boundary graph of a finite set as a planar subgraph · 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 · Finite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit · Finite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings

DefinitionBoundary indicator of an edge#✓fully proved

1 if exactly one of x and y lies in S, and 0 otherwise.

noncomputable def bdInd (S : Set (Site 2)) (x y : Site 2) : ℕ := by
  classical exact if (x ∈ S ↔ y ∉ S) then 1 else 0

Uses 1 · Used by 10

Statement usesSite of the hypercubic lattice

Used byBoundary degree of a unit face · Finite face set containing the face-boundary support · Support of the face-boundary graph of a finite set · Face-boundary graph of a finite set as a planar subgraph · 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 · Finite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit · Finite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings

DefinitionBoundary degree of a unit face#✓fully proved

The number of the four edges of the unit face at (a, b) that have exactly one endpoint in S.

noncomputable def faceBoundaryDegree (S : Set (Site 2)) (a b : ℤ) : ℕ :=
  bdInd S (faceCorner00 a b) (faceCorner10 a b)
    + bdInd S (faceCorner10 a b) (faceCorner11 a b)
    + bdInd S (faceCorner11 a b) (faceCorner01 a b)
    + bdInd S (faceCorner01 a b) (faceCorner00 a b)

Uses 6 · Used by 9

Statement usesSite of the hypercubic lattice · Boundary indicator of an edge · Lower left corner of the unit face at \((a, b)\) · Upper left corner of the unit face at \((a, b)\) · Lower right corner of the unit face at \((a, b)\) · Upper right corner of the unit face at \((a, b)\)

Used byFinite face set containing the face-boundary support · Support of the face-boundary graph of a finite set · Face-boundary graph of a finite set as a planar subgraph · 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 · Finite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit · Finite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings

DefinitionFace loop left of one period of a boundary orbit#✓fully proved

The closed walk of faces to the left of the darts in one period of the boundary orbit of a.

noncomputable def mpl_orbitFaceLoop (K : Set (Site 2)) (a : {e : Dart // IsBoundaryDart K e}) :
    (faceBoundaryGraph K).Walk (dartFace a.1) (dartFace a.1) :=
  (dartOrbitFaceWalk K a.1 a.2 (dartOrbitPeriod K a)).copy rfl
    (by rw [orbit_iterate_period_eq K a])

Uses 9 · Used by 1

Statement usesDart of the square lattice · Boundary dart of a set of sites · Site of the hypercubic lattice · Unit face to the left of a dart · Successor of a boundary dart · Successor map on boundary darts · Face walk along a boundary orbit · Minimal period of a boundary dart · Face-boundary graph of a set

Used byMinimal-period orbit loop as a lattice walk

DefinitionMinimal-period orbit loop as a lattice walk#✓fully proved

The closed face walk of one period of the orbit of a, as a walk in the square lattice.

noncomputable def mpl_orbitLoop (K : Set (Site 2)) (a : {e : Dart // IsBoundaryDart K e}) :
    (hypercubicLattice 2).Walk (dartFace a.1) (dartFace a.1) :=
  (mpl_orbitFaceLoop K a).mapLe (faceBoundaryGraph_le K)

Uses 9

Statement usesDart of the square lattice · Boundary dart of a set of sites · Site of the hypercubic lattice · Boundary edge of a set · Unit face to the left of a dart · Face-boundary graph of a set · Hypercubic lattice \(\mathbb{Z}^d\) · Face loop left of one period of a boundary orbit · Primal edge shared by adjacent faces

DefinitionLower left corner of a face \(f\)#✓fully proved

The lower left corner of the face f. This is StatMech.Lattice.faceCorner00 (f 0) (f 1).

def npd_P00 (f : Site 2) : Site 2 := ![f 0, f 1]

Uses 1 · Used by 4

Statement usesSite of the hypercubic lattice

Used byClosure under the diagonal fill rules · Membership in the star hull · Diagonal touch at a face · King-saturated set

DefinitionLower right corner of a face \(f\)#✓fully proved

The lower right corner of the face f.

def npd_P10 (f : Site 2) : Site 2 := ![f 0 + 1, f 1]

Uses 1 · Used by 4

Statement usesSite of the hypercubic lattice

Used byClosure under the diagonal fill rules · Membership in the star hull · Diagonal touch at a face · King-saturated set

DefinitionUpper right corner of a face \(f\)#✓fully proved

The upper right corner of the face f.

def npd_P11 (f : Site 2) : Site 2 := ![f 0 + 1, f 1 + 1]

Uses 1 · Used by 4

Statement usesSite of the hypercubic lattice

Used byClosure under the diagonal fill rules · Membership in the star hull · Diagonal touch at a face · King-saturated set

DefinitionUpper left corner of a face \(f\)#✓fully proved

The upper left corner of the face f.

def npd_P01 (f : Site 2) : Site 2 := ![f 0, f 1 + 1]

Uses 1 · Used by 4

Statement usesSite of the hypercubic lattice

Used byClosure under the diagonal fill rules · Membership in the star hull · Diagonal touch at a face · King-saturated set

DefinitionDiagonal touch at a face#✓fully proved

K contains exactly two opposite corners of the face f.

def npd_DiagTouch (K : Set (Site 2)) (f : Site 2) : Prop :=
  (npd_P00 f ∈ K ∧ npd_P11 f ∈ K ∧ npd_P10 f ∉ K ∧ npd_P01 f ∉ K) ∨
  (npd_P10 f ∈ K ∧ npd_P01 f ∈ K ∧ npd_P00 f ∉ K ∧ npd_P11 f ∉ K)

Uses 5 · Used by 2

Statement usesSite of the hypercubic lattice · Lower left corner of a face \(f\) · Upper left corner of a face \(f\) · Lower right corner of a face \(f\) · Upper right corner of a face \(f\)

Used bySet with no diagonal touches · No diagonal touch along a boundary orbit

DefinitionNo diagonal touch along a boundary orbit#✓fully proved

No face visited in one period of the orbit of a is a diagonal touch of K.

def npd_NoDiagTouchAlongOrbit (K : Set (Site 2)) (a : {e : Dart // IsBoundaryDart K e}) : Prop :=
  ∀ k ∈ Set.Iio (dartOrbitPeriod K a), ¬ npd_DiagTouch K (dartFace ((dartNext K)^[k] a.1))

Uses 7

Statement usesDart of the square lattice · Boundary dart of a set of sites · Site of the hypercubic lattice · Unit face to the left of a dart · Successor of a boundary dart · Minimal period of a boundary dart · Diagonal touch at a face

DefinitionSet with no diagonal touches#✓fully proved

K has no diagonal touch at any face.

def npd_NoDiagTouch (K : Set (Site 2)) : Prop := ∀ f : Site 2, ¬ npd_DiagTouch K f

Uses 2

Statement usesSite of the hypercubic lattice · Diagonal touch at a face

DefinitionKing-saturated set#✓fully proved

Whenever K contains two opposite corners of a face, it contains one of the other two corners.

def npm_KingSaturated (K : Set (Site 2)) : Prop :=
  ∀ f : Site 2,
    (npd_P00 f ∈ K → npd_P11 f ∈ K → (npd_P10 f ∈ K ∨ npd_P01 f ∈ K)) ∧
    (npd_P10 f ∈ K → npd_P01 f ∈ K → (npd_P00 f ∈ K ∨ npd_P11 f ∈ K))

Uses 5

Statement usesSite of the hypercubic lattice · Lower left corner of a face \(f\) · Upper left corner of a face \(f\) · Lower right corner of a face \(f\) · Upper right corner of a face \(f\)

DefinitionBoundary orbit face loop as a lattice walk#✓fully proved

The face loop of the boundary orbit of e, as a closed walk in the square lattice.

noncomputable def olb_orbitLoop (K : Set (Site 2)) (hK : K.Finite) (e : Dart)
    (he : IsBoundaryDart K e) : (hypercubicLattice 2).Walk (dartFace e) (dartFace e) :=
  (dartOrbitFaceLoop K hK e he).mapLe (faceBoundaryGraph_le K)

Uses 9

Statement usesDart of the square lattice · Boundary dart of a set of sites · Site of the hypercubic lattice · Boundary edge of a set · Unit face to the left of a dart · Face loop of a boundary orbit in the face-boundary graph · Face-boundary graph of a set · Hypercubic lattice \(\mathbb{Z}^d\) · Primal edge shared by adjacent faces

DefinitionProduct set of two coordinate sets in the plane#✓fully proved

The product set {x | x 0 ∈ A ∧ x 1 ∈ B}.

def ndt_product (A B : Set ℤ) : Set (Site 2) := {x | x 0 ∈ A ∧ x 1 ∈ B}

Uses 1

Statement usesSite of the hypercubic lattice

DefinitionSublevel set of a separable function#✓fully proved

The sublevel set {x | φ (x 0) + ψ (x 1) ≤ c} of a separable function.

def ndt_sublevel (φ ψ : ℤ → ℤ) (c : ℤ) : Set (Site 2) := {x | φ (x 0) + ψ (x 1) ≤ c}

Uses 1

Statement usesSite of the hypercubic lattice

InductiveMembership in the star hull#✓fully proved

Membership in the star hull of K: sites of K, closed under filling the lower right corner of a face whose lower left and upper right corners are members, and the lower left corner of a face whose lower right and upper left corners are members.

inductive ndt_StarHullMem (K : Set (Site 2)) : Site 2 → Prop
  | base {x : Site 2} (h : x ∈ K) : ndt_StarHullMem K x
  | fillBL {f : Site 2} (h00 : ndt_StarHullMem K (npd_P00 f))
      (h11 : ndt_StarHullMem K (npd_P11 f)) : ndt_StarHullMem K (npd_P10 f)
  | fillTL {f : Site 2} (h10 : ndt_StarHullMem K (npd_P10 f))
      (h01 : ndt_StarHullMem K (npd_P01 f)) : ndt_StarHullMem K (npd_P00 f)

Uses 5 · Used by 1

Statement usesSite of the hypercubic lattice · Lower left corner of a face \(f\) · Upper left corner of a face \(f\) · Lower right corner of a face \(f\) · Upper right corner of a face \(f\)

Used byStar hull of a set of lattice sites

DefinitionStar hull of a set of lattice sites#✓fully proved

The star hull of K: the smallest superset of K closed under the diagonal fill rules.

def ndt_StarHull (K : Set (Site 2)) : Set (Site 2) := {x | ndt_StarHullMem K x}

Uses 2

Statement usesSite of the hypercubic lattice · Membership in the star hull

DefinitionClosure under the diagonal fill rules#✓fully proved

S is closed under the two diagonal fill rules of StatMech.Lattice.ndt_StarHullMem.

def ndt_FillClosed (S : Set (Site 2)) : Prop :=
  (∀ f, npd_P00 f ∈ S → npd_P11 f ∈ S → npd_P10 f ∈ S) ∧
  (∀ f, npd_P10 f ∈ S → npd_P01 f ∈ S → npd_P00 f ∈ S)

Uses 5

Statement usesSite of the hypercubic lattice · Lower left corner of a face \(f\) · Upper left corner of a face \(f\) · Lower right corner of a face \(f\) · Upper right corner of a face \(f\)

TheoremFour quarter turns of the square lattice are the identity#✓fully proved

Four counterclockwise quarter turns are the identity, i.e. every site is a periodic point of rot90Fun of period 4.

theorem rot90Fun_iterate_four_eq (x : Site 2) : rot90Fun^[4] x = x

Uses 2 · Used by 1

Statement usesSite of the hypercubic lattice · Quarter-turn rotation of the square lattice

Used byQuarter-turn rotations form an action of \(\mathbb{Z}/4\)

DefinitionRotation of \(\mathbb{Z}^2\) by a number of quarter turns#✓fully proved

Rotation of ℤ² by s counterclockwise quarter turns, s : ZMod 4.

noncomputable def rotPow (s : ZMod 4) (x : Site 2) : Site 2 := rot90Fun^[s.val] x

Uses 2 · Used by 5

Statement usesSite of the hypercubic lattice · Quarter-turn rotation of the square lattice

Used byNext boundary dart direction is rotated by the turn · Dart direction after k steps is rotated by the cumulative turn · Total turning of a closed orbit segment is divisible by four · Quarter-turn rotations form an action of \(\mathbb{Z}/4\) · Nontrivial quarter-turn rotations fix no lattice direction

TheoremQuarter-turn rotations form an action of \(\mathbb{Z}/4\)#✓fully proved

rotPow is an action of the additive group ZMod 4.

theorem rotPow_add (a b : ZMod 4) (x : Site 2) :
    rotPow (a + b) x = rotPow a (rotPow b x)

Uses 4 · Used by 1

Statement usesSite of the hypercubic lattice · Rotation of \(\mathbb{Z}^2\) by a number of quarter turns

Proof usesQuarter-turn rotation of the square lattice · Four quarter turns of the square lattice are the identity

Used byDart direction after k steps is rotated by the cumulative turn

TheoremNontrivial quarter-turn rotations fix no lattice direction#✓fully proved

A nontrivial rotation moves every lattice direction: rotPow s fixes the direction of a dart only for s = 0.

theorem rotPow_dir_eq_iff (e : Dart) (s : ZMod 4) :
    rotPow s e.dir = e.dir ↔ s = 0

Uses 7 · Used by 1

Statement usesDart of the square lattice · Direction of a lattice dart · Site of the hypercubic lattice · Rotation of \(\mathbb{Z}^2\) by a number of quarter turns

Proof usesHypercubic lattice \(\mathbb{Z}^d\) · Quarter-turn rotation of the square lattice · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)

Used byTotal turning of a closed orbit segment is divisible by four

DefinitionQuarter turn between consecutive boundary darts modulo 4#✓fully proved

The quarter turn, as an element of ZMod 4, from the boundary dart e of K to its successor dartNext K e: 1 for a counterclockwise (left) turn, 0 for going straight, 3 for a clockwise (right) turn.

noncomputable def turn (K : Set (Site 2)) (e : Dart) : ZMod 4 := by
  classical
  exact
    if e.head + (-rot90Fun e.dir) ∈ K then 1
    else if e.tail + (-rot90Fun e.dir) ∈ K then 0
    else 3

Uses 4 · Used by 4

Statement usesDart of the square lattice · Direction of a lattice dart · Site of the hypercubic lattice · Quarter-turn rotation of the square lattice

Used byCumulative turn along a boundary-tracing orbit · Next boundary dart direction is rotated by the turn · Dart direction after k steps is rotated by the cumulative turn · Total turning of a closed orbit segment is divisible by four

DefinitionSigned quarter turn between consecutive boundary darts#✓fully proved

The signed quarter turn from e to dartNext K e: 1 counterclockwise, 0 straight, -1 clockwise. Its reduction mod 4 is turn K e.

noncomputable def turnZ (K : Set (Site 2)) (e : Dart) : ℤ := by
  classical
  exact
    if e.head + (-rot90Fun e.dir) ∈ K then 1
    else if e.tail + (-rot90Fun e.dir) ∈ K then 0
    else -1

Uses 4 · Used by 7

Statement usesDart of the square lattice · Direction of a lattice dart · Site of the hypercubic lattice · Quarter-turn rotation of the square lattice

Used byTotal turning of a boundary orbit is bounded by its length · Total turning of a closed orbit segment is divisible by four · Number of convex corners in a boundary orbit · Number of reflex corners in a boundary orbit · Number of straight steps in a boundary orbit · Total signed turning along a boundary orbit · Local turn of a boundary orbit at a face

TheoremNext boundary dart direction is rotated by the turn#✓fully proved

The direction of dartNext K e is the direction of e rotated by turn K e quarter turns.

theorem dartNext_dir_eq_rotPow_turn (K : Set (Site 2)) (e : Dart) :
    (dartNext K e).dir = rotPow (turn K e) e.dir

Uses 10 · Used by 1

Statement usesDart of the square lattice · Direction of a lattice dart · Site of the hypercubic lattice · Successor of a boundary dart · Rotation of \(\mathbb{Z}^2\) by a number of quarter turns · Quarter turn between consecutive boundary darts modulo 4

Proof usesHypercubic lattice \(\mathbb{Z}^d\) · Dart from a site in a unit direction · Quarter-turn rotation of the square lattice · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)

Used byDart direction after k steps is rotated by the cumulative turn

DefinitionCumulative turn along a boundary-tracing orbit#✓fully proved

The cumulative turn, in ZMod 4, over the first k steps of the dartNext K-orbit of e.

noncomputable def cumTurn (K : Set (Site 2)) (e : Dart) (k : ℕ) : ZMod 4 :=
  ∑ i ∈ Finset.range k, turn K ((dartNext K)^[i] e)

Uses 4 · Used by 2

Statement usesDart of the square lattice · Site of the hypercubic lattice · Successor of a boundary dart · Quarter turn between consecutive boundary darts modulo 4

Used byDart direction after k steps is rotated by the cumulative turn · Total turning of a closed orbit segment is divisible by four

TheoremDart direction after k steps is rotated by the cumulative turn#✓fully proved

After k boundary-tracing steps the direction of a dart is its initial direction rotated by the cumulative turn cumTurn K e k.

theorem dir_iterate_eq_rotPow_cumTurn (K : Set (Site 2)) (e : Dart) (k : ℕ) :
    ((dartNext K)^[k] e).dir = rotPow (cumTurn K e k) e.dir

Uses 9 · Used by 1

Statement usesDart of the square lattice · Direction of a lattice dart · Site of the hypercubic lattice · Cumulative turn along a boundary-tracing orbit · Successor of a boundary dart · Rotation of \(\mathbb{Z}^2\) by a number of quarter turns

Proof usesNext boundary dart direction is rotated by the turn · Quarter-turn rotations form an action of \(\mathbb{Z}/4\) · Quarter turn between consecutive boundary darts modulo 4

Used byTotal turning of a closed orbit segment is divisible by four

DefinitionTotal signed turning along a boundary orbit#✓fully proved

The total signed turning (in quarter turns) over the first p steps of the dartNext K-orbit of e.

noncomputable def totalTurnZ (K : Set (Site 2)) (e : Dart) (p : ℕ) : ℤ :=
  ∑ i ∈ Finset.range p, turnZ K ((dartNext K)^[i] e)

Uses 4 · Used by 5

Statement usesDart of the square lattice · Site of the hypercubic lattice · Successor of a boundary dart · Signed quarter turn between consecutive boundary darts

Used byTotal turning of a boundary orbit is bounded by its length · Total turning over the minimal period is divisible by four · Total turning of a closed orbit segment is divisible by four · Boundary orbit with a full revolution has length at least four · Boundary orbit making exactly one full revolution

TheoremTotal turning of a closed orbit segment is divisible by four#✓fully proved

If the orbit of e closes after p steps, the total signed turning over these steps is divisible by 4.

theorem four_dvd_totalTurnZ_of_iterate_eq (K : Set (Site 2)) (e : Dart) (p : ℕ)
    (hp : (dartNext K)^[p] e = e) : (4 : ℤ) ∣ totalTurnZ K e p

Uses 12 · Used by 1

Statement usesDart of the square lattice · Site of the hypercubic lattice · Successor of a boundary dart · Total signed turning along a boundary orbit

Proof usesDirection of a lattice dart · Cumulative turn along a boundary-tracing orbit · Dart direction after k steps is rotated by the cumulative turn · Quarter-turn rotation of the square lattice · Rotation of \(\mathbb{Z}^2\) by a number of quarter turns · Nontrivial quarter-turn rotations fix no lattice direction · Quarter turn between consecutive boundary darts modulo 4 · Signed quarter turn between consecutive boundary darts

Used byTotal turning over the minimal period is divisible by four

TheoremTotal turning over the minimal period is divisible by four#✓fully proved

The total signed turning around a boundary orbit, taken over its minimal period, is divisible by 4.

theorem four_dvd_orbit_totalTurnZ (K : Set (Site 2))
    (a : {e : Dart // IsBoundaryDart K e}) :
    (4 : ℤ) ∣ totalTurnZ K a.1 (dartOrbitPeriod K a)

Uses 8

Statement usesDart of the square lattice · Boundary dart of a set of sites · Site of the hypercubic lattice · Minimal period of a boundary dart · Total signed turning along a boundary orbit

Proof usesSuccessor of a boundary dart · Successor map on boundary darts · Total turning of a closed orbit segment is divisible by four

TheoremTotal turning of a boundary orbit is bounded by its length#✓fully proved

The total signed turning around a boundary orbit is at most the orbit length in absolute value.

theorem abs_orbit_totalTurnZ_le (K : Set (Site 2))
    (a : {e : Dart // IsBoundaryDart K e}) :
    |totalTurnZ K a.1 (dartOrbitPeriod K a)| ≤ (dartOrbitPeriod K a : ℤ)

Uses 9 · Used by 1

Statement usesDart of the square lattice · Boundary dart of a set of sites · Site of the hypercubic lattice · Minimal period of a boundary dart · Total signed turning along a boundary orbit

Proof usesDirection of a lattice dart · Successor of a boundary dart · Quarter-turn rotation of the square lattice · Signed quarter turn between consecutive boundary darts

Used byBoundary orbit with a full revolution has length at least four

DefinitionBoundary orbit making exactly one full revolution#✓fully proved

The boundary orbit through a turns by exactly one full revolution, i.e. its total signed turning is 4 or -4 quarter turns.

def TurningIsFullRevolution (K : Set (Site 2)) (a : {e : Dart // IsBoundaryDart K e}) :
    Prop :=
  totalTurnZ K a.1 (dartOrbitPeriod K a) = 4 ∨
    totalTurnZ K a.1 (dartOrbitPeriod K a) = -4

Uses 5 · Used by 1

Statement usesDart of the square lattice · Boundary dart of a set of sites · Site of the hypercubic lattice · Minimal period of a boundary dart · Total signed turning along a boundary orbit

Used byBoundary orbit with a full revolution has length at least four

TheoremBoundary orbit with a full revolution has length at least four#✓fully proved

A boundary orbit that makes a full revolution has length at least 4.

theorem orbitPeriod_ge_four_of_fullRevolution (K : Set (Site 2))
    (a : {e : Dart // IsBoundaryDart K e}) (h : TurningIsFullRevolution K a) :
    4 ≤ dartOrbitPeriod K a

Uses 7

Statement usesDart of the square lattice · Boundary dart of a set of sites · Site of the hypercubic lattice · Boundary orbit making exactly one full revolution · Minimal period of a boundary dart

Proof usesTotal turning of a boundary orbit is bounded by its length · Total signed turning along a boundary orbit

DefinitionNumber of reflex corners in a boundary orbit#✓fully proved

The number of steps i < p in the boundary orbit of e with turn turnZ = 1 (reflex corners of K).

noncomputable def rightCornerCount (K : Set (Site 2)) (e : Dart) (p : ℕ) : ℤ :=
  ((Finset.range p).filter (fun i => turnZ K ((dartNext K)^[i] e) = 1)).card

Uses 4 · Used by 1

Statement usesDart of the square lattice · Site of the hypercubic lattice · Successor of a boundary dart · Signed quarter turn between consecutive boundary darts

Used byCorner balance of a simple lattice polygon

DefinitionNumber of convex corners in a boundary orbit#✓fully proved

The number of steps i < p in the boundary orbit of e with turn turnZ = -1 (convex corners of K).

noncomputable def leftCornerCount (K : Set (Site 2)) (e : Dart) (p : ℕ) : ℤ :=
  ((Finset.range p).filter (fun i => turnZ K ((dartNext K)^[i] e) = -1)).card

Uses 4 · Used by 1

Statement usesDart of the square lattice · Site of the hypercubic lattice · Successor of a boundary dart · Signed quarter turn between consecutive boundary darts

Used byCorner balance of a simple lattice polygon

DefinitionUnit cell as a one-site set#✓fully proved

The one-site set {(0, 0)}.

noncomputable def unitCell : Set (Site 2) := {![0, 0]}

Uses 1 · Used by 2

Statement usesSite of the hypercubic lattice

Used byBase boundary dart of the unit cell · Face loop around the unit cell

DefinitionRightward boundary dart of the unit cell#✓fully proved

The boundary dart of the unit cell pointing right.

noncomputable def ucDart0 : Dart := mkDart ![0, 0] ![1, 0] unitWt_px

Uses 3 · Used by 2

Statement usesDart of the square lattice · Dart from a site in a unit direction · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)

Used byBase boundary dart of the unit cell · Face loop around the unit cell

DefinitionDownward boundary dart of the unit cell#✓fully proved

The boundary dart of the unit cell pointing down.

noncomputable def ucDart1 : Dart := mkDart ![0, 0] ![0, -1] unitWt_my

Uses 3 · Used by 1

Statement usesDart of the square lattice · Dart from a site in a unit direction · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)

Used byFace loop around the unit cell

DefinitionLeftward boundary dart of the unit cell#✓fully proved

The boundary dart of the unit cell pointing left.

noncomputable def ucDart2 : Dart := mkDart ![0, 0] ![-1, 0] unitWt_mx

Uses 3 · Used by 1

Statement usesDart of the square lattice · Dart from a site in a unit direction · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)

Used byFace loop around the unit cell

DefinitionUpward boundary dart of the unit cell#✓fully proved

The boundary dart of the unit cell pointing up.

noncomputable def ucDart3 : Dart := mkDart ![0, 0] ![0, 1] unitWt_py

Uses 3 · Used by 1

Statement usesDart of the square lattice · Dart from a site in a unit direction · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)

Used byFace loop around the unit cell

DefinitionBase boundary dart of the unit cell#✓fully proved

The rightward boundary dart of the unit cell, as an element of the subtype of boundary darts.

noncomputable def ucBase : {e : Dart // IsBoundaryDart unitCell e} :=
  ⟨ucDart0, ucDart0_boundary⟩

Uses 7

Statement usesDart of the square lattice · Boundary dart of a set of sites · Site of the hypercubic lattice · Dart from a site in a unit direction · Rightward boundary dart of the unit cell · Unit cell as a one-site set · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)

DefinitionNumber of straight steps in a boundary orbit#✓fully proved

The number of steps i < p in the boundary orbit of e with turn 0.

noncomputable def straightStepCount (K : Set (Site 2)) (e : Dart) (p : ℕ) : ℤ :=
  ((Finset.range p).filter (fun i => turnZ K ((dartNext K)^[i] e) = 0)).card

Uses 4

Statement usesDart of the square lattice · Site of the hypercubic lattice · Successor of a boundary dart · Signed quarter turn between consecutive boundary darts

DefinitionCorner balance of a simple lattice polygon#✓fully proved

The numbers of reflex and convex corners along the orbit of a differ by 4 or -4, the corner count of a simple lattice polygon.

def SimplePolygonCornerBalance (K : Set (Site 2)) (a : {e : Dart // IsBoundaryDart K e}) :
    Prop :=
  rightCornerCount K a.1 (dartOrbitPeriod K a) -
      leftCornerCount K a.1 (dartOrbitPeriod K a) = 4 ∨
    rightCornerCount K a.1 (dartOrbitPeriod K a) -
      leftCornerCount K a.1 (dartOrbitPeriod K a) = -4

Uses 6

Statement usesDart of the square lattice · Boundary dart of a set of sites · Site of the hypercubic lattice · Minimal period of a boundary dart · Number of convex corners in a boundary orbit · Number of reflex corners in a boundary orbit

DefinitionDomino as a two-site set#✓fully proved

The two-site set {(0, 0), (1, 0)}.

noncomputable def domino : Set (Site 2) := {![0, 0], ![1, 0]}

Uses 1 · Used by 2

Statement usesSite of the hypercubic lattice

Used byBase boundary dart of the domino · Face loop around the domino

DefinitionDownward domino dart at the left site#✓fully proved

The boundary dart of the domino from (0, 0) downwards.

noncomputable def dmD0 : Dart := mkDart ![0, 0] ![0, -1] unitWt_my

Uses 3 · Used by 2

Statement usesDart of the square lattice · Dart from a site in a unit direction · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)

Used byBase boundary dart of the domino · Face loop around the domino

DefinitionLeftward domino dart at the left site#✓fully proved

The boundary dart of the domino from (0, 0) to the left.

noncomputable def dmD1 : Dart := mkDart ![0, 0] ![-1, 0] unitWt_mx

Uses 3 · Used by 1

Statement usesDart of the square lattice · Dart from a site in a unit direction · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)

Used byFace loop around the domino

DefinitionUpward domino dart at the left site#✓fully proved

The boundary dart of the domino from (0, 0) upwards.

noncomputable def dmD2 : Dart := mkDart ![0, 0] ![0, 1] unitWt_py

Uses 3 · Used by 1

Statement usesDart of the square lattice · Dart from a site in a unit direction · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)

Used byFace loop around the domino

DefinitionUpward domino dart at the right site#✓fully proved

The boundary dart of the domino from (1, 0) upwards.

noncomputable def dmD3 : Dart := mkDart ![1, 0] ![0, 1] unitWt_py

Uses 3 · Used by 1

Statement usesDart of the square lattice · Dart from a site in a unit direction · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)

Used byFace loop around the domino

DefinitionRightward domino dart at the right site#✓fully proved

The boundary dart of the domino from (1, 0) to the right.

noncomputable def dmD4 : Dart := mkDart ![1, 0] ![1, 0] unitWt_px

Uses 3 · Used by 1

Statement usesDart of the square lattice · Dart from a site in a unit direction · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)

Used byFace loop around the domino

DefinitionDownward domino dart at the right site#✓fully proved

The boundary dart of the domino from (1, 0) downwards.

noncomputable def dmD5 : Dart := mkDart ![1, 0] ![0, -1] unitWt_my

Uses 3 · Used by 1

Statement usesDart of the square lattice · Dart from a site in a unit direction · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)

Used byFace loop around the domino

DefinitionBase boundary dart of the domino#✓fully proved

The boundary dart dmD0 of the domino, as an element of the subtype of boundary darts.

noncomputable def dmBase : {e : Dart // IsBoundaryDart domino e} := ⟨dmD0, dmD0_boundary⟩

Uses 7

Statement usesDart of the square lattice · Boundary dart of a set of sites · Site of the hypercubic lattice · Downward domino dart at the left site · Domino as a two-site set · Dart from a site in a unit direction · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)

DefinitionNo-pinch condition for a boundary orbit#✓fully proved

Darts in one period of the orbit of a that have the same face also have the same direction.

def OrbitFaceNoPinch (K : Set (Site 2)) (a : {e : Dart // IsBoundaryDart K e}) : Prop :=
  ∀ i ∈ Set.Iio (dartOrbitPeriod K a), ∀ j ∈ Set.Iio (dartOrbitPeriod K a),
    dartFace ((dartNext K)^[i] a.1) = dartFace ((dartNext K)^[j] a.1) →
      ((dartNext K)^[i] a.1).dir = ((dartNext K)^[j] a.1).dir

Uses 7 · Used by 1

Statement usesDart of the square lattice · Direction of a lattice dart · Boundary dart of a set of sites · Site of the hypercubic lattice · Unit face to the left of a dart · Successor of a boundary dart · Minimal period of a boundary dart

Used by\(p_c(\mathbb{Z}^2) < 1\) under a no-pinch hypothesis

DefinitionFace loop around the unit cell#✓fully proved

The closed walk of faces around the unit cell, of length four.

noncomputable def unitCellFaceLoop :
    (faceBoundaryGraph unitCell).Walk (dartFace ucDart0) (dartFace ucDart0) :=
  (dartOrbitFaceWalk unitCell ucDart0 ucDart0_boundary 4).copy rfl (by rw [iterate_ucDart_4])

Uses 17

Statement usesDart of the square lattice · Direction of a lattice dart · Boundary dart of a set of sites · Site of the hypercubic lattice · Unit face to the left of a dart · Successor of a boundary dart · Face walk along a boundary orbit · Face-boundary graph of a set · Hypercubic lattice \(\mathbb{Z}^d\) · Dart from a site in a unit direction · Quarter-turn rotation of the square lattice · Rightward boundary dart of the unit cell · Downward boundary dart of the unit cell · Leftward boundary dart of the unit cell · Upward boundary dart of the unit cell · Unit cell as a one-site set · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)

DefinitionFace loop around the domino#✓fully proved

The closed walk of faces around the domino, of length six.

noncomputable def dominoFaceLoop :
    (faceBoundaryGraph domino).Walk (dartFace dmD0) (dartFace dmD0) :=
  (dartOrbitFaceWalk domino dmD0 dmD0_boundary 6).copy rfl (by rw [iterate_dmD_6])

Uses 19

Statement usesDart of the square lattice · Direction of a lattice dart · Boundary dart of a set of sites · Site of the hypercubic lattice · Unit face to the left of a dart · Successor of a boundary dart · Face walk along a boundary orbit · Downward domino dart at the left site · Leftward domino dart at the left site · Upward domino dart at the left site · Upward domino dart at the right site · Rightward domino dart at the right site · Downward domino dart at the right site · Domino as a two-site set · Face-boundary graph of a set · Hypercubic lattice \(\mathbb{Z}^d\) · Dart from a site in a unit direction · Quarter-turn rotation of the square lattice · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)

DefinitionFour unit vectors of \(\mathbb{Z}^2\)#✓fully proved

The four unit vectors of ℤ².

noncomputable def usc_fourDirs : Finset (Site 2) :=
  {![1, 0], ![-1, 0], ![0, 1], ![0, -1]}

Uses 1

Statement usesSite of the hypercubic lattice

DefinitionVisit times of a boundary orbit to a face#✓fully proved

The times i in one period of the orbit of a at which the dart has face f.

noncomputable def usc_visitSet (K : Set (Site 2)) (a : {e : Dart // IsBoundaryDart K e})
    (f : Site 2) : Finset ℕ := by
  classical
  exact (Finset.range (dartOrbitPeriod K a)).filter
    (fun i => dartFace ((dartNext K)^[i] a.1) = f)

Uses 6 · Used by 2

Statement usesDart of the square lattice · Boundary dart of a set of sites · Site of the hypercubic lattice · Unit face to the left of a dart · Successor of a boundary dart · Minimal period of a boundary dart

Used byEach face visited once per period by a boundary orbit · Local turn of a boundary orbit at a face

DefinitionEach face visited once per period by a boundary orbit#✓fully proved

Every face visited by the orbit of a is visited exactly once per period.

def usc_FaceMultiplicityOne (K : Set (Site 2)) (a : {e : Dart // IsBoundaryDart K e}) : Prop :=
  ∀ f : Site 2, 1 ≤ (usc_visitSet K a f).card → (usc_visitSet K a f).card = 1

Uses 4

Statement usesDart of the square lattice · Boundary dart of a set of sites · Site of the hypercubic lattice · Visit times of a boundary orbit to a face

DefinitionLocal turn of a boundary orbit at a face#✓fully proved

The sum of the turns turnZ at the visits of the orbit of a to the face f.

noncomputable def usc_localTurn (K : Set (Site 2)) (a : {e : Dart // IsBoundaryDart K e})
    (f : Site 2) : ℤ :=
  ∑ i ∈ usc_visitSet K a f, turnZ K ((dartNext K)^[i] a.1)

Uses 6

Statement usesDart of the square lattice · Boundary dart of a set of sites · Site of the hypercubic lattice · Successor of a boundary dart · Signed quarter turn between consecutive boundary darts · Visit times of a boundary orbit to a face

DefinitionFaces visited by a boundary orbit in one period#✓fully proved

The set of faces visited in one period of the orbit of a.

noncomputable def usc_orbitFaces (K : Set (Site 2)) (a : {e : Dart // IsBoundaryDart K e}) :
    Finset (Site 2) := by
  classical
  exact (Finset.range (dartOrbitPeriod K a)).image (fun i => dartFace ((dartNext K)^[i] a.1))

Uses 6

Statement usesDart of the square lattice · Boundary dart of a set of sites · Site of the hypercubic lattice · Unit face to the left of a dart · Successor of a boundary dart · Minimal period of a boundary dart

Theorem\(p_c(\mathbb{Z}^2) < 1\) under a no-pinch hypothesis#✓fully proved

p_c(ℤ²) < 1, under the hypothesis that for every configuration with a finite origin cluster the boundary orbit of the exit dart has period at least three, has no pinch, and contains the left exit dart.

theorem usc_pc_lt_one_of_noPinch
    (h : ∀ (ω : ConfigSpace (Sym2 (Site 2))) (hfin : (cluster 2 ω (origin 2)).Finite),
        3 ≤ dartOrbitPeriod (cluster 2 ω (origin 2)) (exitBaseSub (ω := ω) hfin) ∧
        OrbitFaceNoPinch (cluster 2 ω (origin 2)) (exitBaseSub (ω := ω) hfin) ∧
        ExitDartsSameOrbit ω hfin) :
    (StatMech.Percolation.pc 2 : ℝ) < 1

Uses 22

Statement usesConfiguration space of a statistical-mechanics model · Left and right exit darts lie in the same boundary orbit · No-pinch condition for a boundary orbit · Site of the hypercubic lattice · Open cluster of a site · Minimal period of a boundary dart · Exit dart of a finite origin cluster · Origin of the hypercubic lattice · Critical probability of bond percolation on the hypercubic lattice

Proof usesDart of the square lattice · Direction of a lattice dart · Boundary dart of a set of sites · Simplicity of the exit orbit's face walk · Unit face to the left of a dart · Successor of a boundary dart · Successor map on boundary darts · Exit dart on the positive horizontal axis · Hypercubic lattice \(\mathbb{Z}^d\) · Negative part of an integer · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · Quarter-turn rotation of the square lattice · \(\ell^1\) norm of a vector in \(\mathbb{Z}^2\)

89 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.