Discrete Jordan curve theorem for the square lattice

DefinitionSquare lattice with a set of vertices removed#✓fully proved

The square lattice with every vertex of B removed (edges with an endpoint in B deleted).

def ffc_offSupportLattice (B : Set (Site 2)) : SimpleGraph (Site 2) where
  Adj x y := (hypercubicLattice 2).Adj x y ∧ x ∉ B ∧ y ∉ B
  symm := by
    refine ⟨?_⟩
    rintro x y ⟨hadj, hx, hy⟩
    exact ⟨hadj.symm, hy, hx⟩
  loopless := ⟨fun x h => (hypercubicLattice 2).irrefl h.1⟩

Uses 2 · Used by 4

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

Used byLattice off a closed walk · Flood fill avoiding a set of sites · Lattice walk avoiding a set, lifted to the reduced lattice · Boundary darts of a component off a closed walk

DefinitionLattice walk avoiding a set, lifted to the reduced lattice#✓fully proved

A lattice walk avoiding B, viewed as a walk in ffc_offSupportLattice B.

def ffc_lift_walk {B : Set (Site 2)} :
    ∀ {x y : Site 2} (p : (hypercubicLattice 2).Walk x y),
      (∀ z ∈ p.support, z ∉ B) → (ffc_offSupportLattice B).Walk x y
  | _, _, SimpleGraph.Walk.nil, _ => SimpleGraph.Walk.nil
  | _, _, SimpleGraph.Walk.cons hab p, hp =>
      SimpleGraph.Walk.cons
        ⟨hab, hp _ (by simp), hp _ (by
          rw [SimpleGraph.Walk.support_cons]; right; exact p.start_mem_support)⟩
        (ffc_lift_walk p (fun z hz => hp z (by
          rw [SimpleGraph.Walk.support_cons]; exact List.mem_cons_of_mem _ hz)))

Uses 3 · Used by 1

Statement usesSite of the hypercubic lattice · Square lattice with a set of vertices removed · Hypercubic lattice \(\mathbb{Z}^d\)

Used byBoundary darts of a component off a closed walk

DefinitionFlood fill avoiding a set of sites#✓fully proved

The flood fill of seed avoiding B: the sites reachable from seed in the lattice with B removed.

def ffc_floodFill (B : Set (Site 2)) (seed : Site 2) : Set (Site 2) :=
  {z | (ffc_offSupportLattice B).Reachable seed z}

Uses 2

Statement usesSite of the hypercubic lattice · Square lattice with a set of vertices removed

DefinitionSquare lattice with a closed walk's vertices removed#✓fully proved

The square lattice with the vertices of the closed walk Vc removed. It is the same graph as StatMech.Lattice.ffc_offSupportLattice {z | z ∈ Vc.support}.

noncomputable def offSupport {a : Site 2} (Vc : (hypercubicLattice 2).Walk a a) :
    SimpleGraph (Site 2) where
  Adj x y := (hypercubicLattice 2).Adj x y ∧ x ∉ Vc.support ∧ y ∉ Vc.support
  symm := by
    refine ⟨?_⟩
    intro x y ⟨hadj, hx, hy⟩
    exact ⟨hadj.symm, hy, hx⟩
  loopless := ⟨fun x h => (hypercubicLattice 2).irrefl h.1⟩

Uses 2 · Used by 2

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

Used byComponent off a closed walk containing a seed · Boundary darts of a component off a closed walk

DefinitionComponent off a closed walk containing a seed#✓fully proved

The sites reachable from seed in the lattice with the vertices of Vc removed.

def offSupportComponent {a : Site 2} (Vc : (hypercubicLattice 2).Walk a a) (seed : Site 2) :
    Set (Site 2) :=
  {z | (offSupport Vc).Reachable seed z}

Uses 3 · Used by 1

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Square lattice with a closed walk's vertices removed

Used byBoundary darts of a component off a closed walk

TheoremEvery edge of a finite even-degree graph lies on a cycle#✓fully proved

In a finite graph in which every vertex has even degree, every edge lies on a cycle. See also Mathlib's SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle, which this combines with StatMech.Lattice.reachable_deleteEdges_of_even.

theorem exists_cycle_through_edge_of_even (heven : ∀ x, Even (G.degree x))
    {v w : V} (hadj : G.Adj v w) :
    ∃ (u : V) (p : G.Walk u u), p.IsCycle ∧ s(v, w) ∈ p.edges

Used by 3

Used byEuler's theorem · Finite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit · Finite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings

DefinitionPrimal edge shared by adjacent faces#✓fully proved

The primal edge of ℤ² separating the adjacent unit faces with lower left corners f and g.

noncomputable def sharedPrimalEdge (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), f 1], ![max (f 0) (g 0), f 1 + 1])

Uses 1 · Used by 51

Statement usesSite of the hypercubic lattice

Used byMinimal-period orbit loop as a lattice walk · Boundary orbit face loop as a lattice walk · Face-boundary graph of a set · Cut set of a face coloring · Bounded faces of a finite lattice graph are counted by its cycle rank · Whitney cut-cycle duality for a planar lattice subgraph · Exterior of a box maps into the face-region graph · Keep-reconnect residue for finite graphs · The inner face component is finite · Face-adjacent cells have the same ray parity · 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 · Lattice Jordan curve theorem, even-odd form · Bounded face of a simple closed walk has no pinch points · Three walk edges cannot meet at a vertex · No right cell lies in the bounded face · A side between interior and exterior cells is a walk edge · Cells on either side of a step lie in different faces · Number of cells is at most the nullity of the skeleton · Adjacent cells have connected lower-left corners · The face of a cell is enclosed on all four sides · Shared side of a cell and an adjacent face is an edge · Interior cells have connected lower-left corners · Hopf's Umlaufsatz · Edge flip relation of an edge set · Whitney duality in the bridge direction · Whitney's cut–cycle duality · Face-region graph of a square-lattice subgraph · Number of edge crossings of a face walk · Primal edge between two faces lies in a subgraph · Event that a dual circuit is closed · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Primal edges crossed by a dual walk · 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 · \(p_c(\mathbb{Z}^2) < 1\) via boundary connectivity, assuming linked exits · Finite face set containing the face-boundary support · Support of the face-boundary graph of a finite set · Shift isomorphism: lattice minus barrier edges to face region graph · 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 · Closed-circuit event of a dual circuit · Finite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit · Finite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings

DefinitionBoundary edge of a set#✓fully proved

The edge e has exactly one endpoint in S.

def bdEdge (S : Set (Site 2)) (e : Sym2 (Site 2)) : Prop := by
  classical
  exact Sym2.lift ⟨fun x y => (x ∈ S ↔ y ∉ S), by
    intro x y
    simp only [eq_iff_iff]
    by_cases hx : x ∈ S <;> by_cases hy : y ∈ S <;> simp_all⟩ e

Uses 1 · Used by 29

Statement usesSite of the hypercubic lattice

Used byMinimal-period orbit loop as a lattice walk · Boundary orbit face loop as a lattice walk · Number of boundary crossings of a walk · Face-boundary graph of a set · Open vertical crossings separate the sides of a rectangle · Square lattice with the boundary edges of a set removed · Vertical overlap crossings separate the sides of a rectangle · RSW gluing from side separation · Separating set for a lattice rectangle · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Face walk along the first successors of a boundary dart · Open cluster maps into the lattice minus its boundary edges · Face walk along a boundary orbit · Discrete Jordan separation for finite open clusters · Box exterior maps into the lattice minus boundary edges · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · \(p_c(\mathbb{Z}^2) < 1\) via boundary connectivity, assuming linked exits · Set and walk interior share boundary edges · Finite face set containing the face-boundary support · Support of the face-boundary graph of a finite set · Shift isomorphism: lattice minus barrier edges to face region graph · 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-boundary graph of a set#✓fully proved

The face-boundary graph of S: two adjacent faces are joined when the primal edge between them has exactly one endpoint in S. Its edges are the dual edges crossing the boundary of S.

def faceBoundaryGraph (S : Set (Site 2)) : SimpleGraph (Site 2) where
  Adj f g := (hypercubicLattice 2).Adj f g ∧ bdEdge S (sharedPrimalEdge f g)
  symm := by
    refine ⟨fun f g ⟨hadj, hbd⟩ => ?_⟩
    refine ⟨hadj.symm, ?_⟩
    rwa [← sharedPrimalEdge_comm_of_adj hadj]
  loopless := by
    refine ⟨fun f h => ?_⟩
    exact (hypercubicLattice 2).irrefl h.1

Uses 4 · Used by 38

Statement usesSite of the hypercubic lattice · Boundary edge of a set · Hypercubic lattice \(\mathbb{Z}^d\) · Primal edge shared by adjacent faces

Used byFace loop around the domino · Face loop left of one period of a boundary orbit · Minimal-period orbit loop as a lattice walk · Boundary orbit face loop as a lattice walk · Face loop around the unit cell · Anchored dual-circuit enclosure property · \(p_c(2) < 1\) from anchored dual-circuit enclosure · Existence of an anchored dual cycle around the origin cluster · Closed face walk of the canonical contour · Face walk along the first successors of a boundary dart · Canonical orbit cycle condition · Dual cycle reaching the left half-plane · Face loop of a boundary orbit in the face-boundary graph · Face walk along a boundary orbit · Origin cluster's enclosing contour links the two axis exits · Minimal-period face loop of the exit orbit · Face loop of the exit orbit of a finite cluster · Anchored dual cycles give the anchored enclosure property · \(p_c(\mathbb{Z}^2) < 1\) assuming simple exit orbits · \(p_c(\mathbb{Z}^2) < 1\) assuming a canonical orbit cycle · \(p_c(\mathbb{Z}^2) < 1\) via boundary connectivity, assuming linked exits · Component of a face in the face-boundary graph · Faces of a set reachable from a face in the face-boundary graph · Tight axis circuit data: contour edges in one axis-face component · Finite face set containing the face-boundary support · Connectedness of the face-boundary graph on a face set · Hole-free connected cluster through the origin · Winding hypothesis for outer contours on \(\mathbb{Z}^2\) · Support of the face-boundary graph of a finite set · Shift isomorphism: lattice minus barrier edges to face region graph · Face-boundary graph of a finite set as a planar subgraph · 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 · Finite cluster in \(\mathbb{Z}^2\) gives a closed lattice circuit · Finite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings

DefinitionFour unit faces at a lattice site#✓fully proved

The four unit faces having the site c as a corner.

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

Uses 1 · Used by 9

Statement usesSite of the hypercubic lattice

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

DefinitionNumber of boundary crossings of a walk#✓fully proved

The number of edges of the walk w with exactly one endpoint in S.

noncomputable def crossCount (S : Set (Site 2)) {x y : Site 2}
    (w : (hypercubicLattice 2).Walk x y) : ℕ := by
  classical
  exact w.edges.countP (fun e => decide (bdEdge S e))

Uses 3 · Used by 3

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

Used byOpen vertical crossings separate the sides of a rectangle · RSW gluing from side separation · Finite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings

DefinitionSquare lattice with the boundary edges of a set removed#✓fully proved

The square lattice with every edge having exactly one endpoint in S removed.

noncomputable def latticeMinusBarrier (S : Set (Site 2)) : SimpleGraph (Site 2) where
  Adj x y := (hypercubicLattice 2).Adj x y ∧ ¬ bdEdge S s(x, y)
  symm := by
    refine ⟨?_⟩
    intro x y ⟨hadj, hbd⟩
    refine ⟨hadj.symm, ?_⟩
    rwa [Sym2.eq_swap]
  loopless := ⟨fun x h => (hypercubicLattice 2).irrefl h.1⟩

Uses 3 · Used by 10

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

Used byInside and outside of a closed walk are connected · Jordan region of the cut lattice · Open cluster maps into the lattice minus its boundary edges · Discrete Jordan separation for finite open clusters · Box exterior maps into the lattice minus boundary edges · 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 · Finite cluster in \(\mathbb{Z}^2\): closed circuit, separated point, odd crossings

DefinitionExterior of a box maps into the face-region graph#✓fully proved

For H and f0g0 inside [-R, R]², the lattice on the exterior of [-(R + 1), R + 1]² maps into the face-region graph of H with f0g0 deleted.

noncomputable def jfd_extToDeletedHom (H : SimpleGraph (Site 2)) (R : ℕ) (f0 g0 : Site 2)
    (hHR : ∀ v ∈ H.support, v ∈ box 2 R) (hf0 : f0 ∈ box 2 R) (hg0 : g0 ∈ box 2 R) :
    (hypercubicLattice 2).induce (exterior 2 (R + 1)) →g
      (whb_faceRegion H).deleteEdges {s(f0, g0)} where
  toFun v := (v : Site 2)
  map_rel' := by
    intro a b hab
    exact jfd_deleted_adj_of_exterior H R f0 g0 hHR hf0 hg0 a.2 b.2 hab

Uses 6

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Exterior of a box in \(\mathbb{Z}^d\) · Hypercubic lattice \(\mathbb{Z}^d\) · Primal edge shared by adjacent faces · Face-region graph of a square-lattice subgraph

TheoremJordan curve theorem for cycles: face count two#✓fully proved

A cycle, as a graph on its own vertices, has face count two: the combinatorial form of the Jordan curve theorem for cycles (C. Jordan, Cours d'analyse, 1887).

theorem jcs_cycle_faceCount_eq_two {V : Type*} {G : SimpleGraph V} {v : V}
    (c : G.Walk v v) (hc : c.IsCycle) :
    faceCount c.toSubgraph.coe = 2

Uses 2

Statement usesFace count of a finite graph from its cycle rank

Proof usesCycle rank of a finite graph

DefinitionJordan region of the cut lattice#✓fully proved

S and its complement are nonempty, and any two sites on the same side of S are connected in the lattice with the boundary edges of S removed.

def jcs_JordanRegion (S : Set (Site 2)) : Prop :=
  (∃ x, x ∈ S) ∧ (∃ y, y ∉ S) ∧
    (∀ a b : Site 2, a ∈ S → b ∈ S → (latticeMinusBarrier S).Reachable a b) ∧
    (∀ a b : Site 2, a ∉ S → b ∉ S → (latticeMinusBarrier S).Reachable a b)

Uses 2

Statement usesSite of the hypercubic lattice · Square lattice with the boundary edges of a set removed

DefinitionBounded region count as cycle rank#✓fully proved

The number of bounded regions of a finite graph, defined as its cycle rank nullity G.

noncomputable def jes_boundedRegionCount [Finite V] [DecidableEq V] (G : SimpleGraph V) : ℕ :=
  nullity G

Uses 1

Statement usesCycle rank of a finite graph

DefinitionQuadrant below and left of a site#✓fully proved

The quadrant of sites p with p 0 ≤ z 0 - 1 and p 1 ≤ z 1 - 1.

def jec_quad (z : Site 2) : Set (Site 2) := {p | p 0 ≤ z 0 - 1 ∧ p 1 ≤ z 1 - 1}

Uses 1 · Used by 1

Statement usesSite of the hypercubic lattice

Used byOpen vertical crossings separate the sides of a rectangle

DefinitionRay edges left of a site#✓fully proved

The vertical lattice edges in a column left of z joining rows z 1 - 1 and z 1: the edges crossed by a horizontal ray going left from the face corner of z.

def jec_rayEdge (z : Site 2) (e : Sym2 (Site 2)) : Prop := by
  classical
  exact Sym2.lift ⟨fun x y =>
      (x 0 = y 0 ∧ x 0 ≤ z 0 - 1) ∧
      ((x 1 = z 1 - 1 ∧ y 1 = z 1) ∨ (y 1 = z 1 - 1 ∧ x 1 = z 1)), by
    intro x y; simp only [eq_iff_iff]
    constructor
    · rintro ⟨⟨h1, h2⟩, h3⟩; exact ⟨⟨h1.symm, h1 ▸ h2⟩, by tauto⟩
    · rintro ⟨⟨h1, h2⟩, h3⟩; exact ⟨⟨h1.symm, h1 ▸ h2⟩, by tauto⟩⟩ e

Uses 1 · Used by 2

Statement usesSite of the hypercubic lattice

Used byOpen vertical crossings separate the sides of a rectangle · Ray-crossing count of a walk

DefinitionWall edges below a site#✓fully proved

The horizontal lattice edges in a row below z joining columns z 0 - 1 and z 0: the edges crossed by a vertical ray going down from the face corner of z.

def jec_wallEdge (z : Site 2) (e : Sym2 (Site 2)) : Prop := by
  classical
  exact Sym2.lift ⟨fun x y =>
      (x 1 = y 1 ∧ x 1 ≤ z 1 - 1) ∧
      ((x 0 = z 0 - 1 ∧ y 0 = z 0) ∨ (y 0 = z 0 - 1 ∧ x 0 = z 0)), by
    intro x y; simp only [eq_iff_iff]
    constructor
    · rintro ⟨⟨h1, h2⟩, h3⟩; exact ⟨⟨h1.symm, h1 ▸ h2⟩, by tauto⟩
    · rintro ⟨⟨h1, h2⟩, h3⟩; exact ⟨⟨h1.symm, h1 ▸ h2⟩, by tauto⟩⟩ e

Uses 1 · Used by 2

Statement usesSite of the hypercubic lattice

Used byOpen vertical crossings separate the sides of a rectangle · Wall-crossing count of a walk

DefinitionRay-crossing count of a walk#✓fully proved

The number of ray edges of z traversed by the walk w.

noncomputable def jec_rayCount (z : Site 2) {x y : Site 2}
    (w : (hypercubicLattice 2).Walk x y) : ℕ :=
  w.edges.countP (fun e => decide (jec_rayEdge z e))

Uses 3 · Used by 3

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Ray edges left of a site

Used bySet of sites is the inside of a closed lattice walk · Open vertical crossings separate the sides of a rectangle · Inside of a closed walk by the even-odd rule

DefinitionWall-crossing count of a walk#✓fully proved

The number of wall edges of z traversed by the walk w.

noncomputable def jec_wallCount (z : Site 2) {x y : Site 2}
    (w : (hypercubicLattice 2).Walk x y) : ℕ :=
  w.edges.countP (fun e => decide (jec_wallEdge z e))

Uses 3 · Used by 1

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Wall edges below a site

Used byOpen vertical crossings separate the sides of a rectangle

DefinitionInside of a closed walk by the even-odd rule#✓fully proved

The inside of a closed walk Vc by the even–odd rule: sites whose ray count with respect to Vc is odd.

def jec_leftRegion {a : Site 2} (Vc : (hypercubicLattice 2).Walk a a) : Set (Site 2) :=
  {z | ¬ Even (jec_rayCount z Vc)}

Uses 3 · Used by 4

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Ray-crossing count of a walk

Used byInside and outside of a closed walk are connected · Jordan region property off a closed walk · Open vertical crossings separate the sides of a rectangle · Set and walk interior share boundary edges

DefinitionVertical lattice path upward#✓fully proved

The vertical lattice path from (col, r) up to (col, r + k).

def jec_vsegUp (col : ℤ) : (r : ℤ) → (k : ℕ) →
    (hypercubicLattice 2).Walk ![col, r] ![col, r + (k:ℤ)]
  | r, 0 => (SimpleGraph.Walk.nil).copy rfl (by norm_num)
  | r, (k+1) => by
      have hadj : (hypercubicLattice 2).Adj ![col, r] ![col, r+1] := by
        simp [hypercubicLattice_adj, Fin.sum_univ_two]
      exact (SimpleGraph.Walk.cons hadj (jec_vsegUp col (r+1) k)).copy rfl (by push_cast; ring_nf)

Uses 2 · Used by 2

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

Used byOpen vertical crossings separate the sides of a rectangle · Return path around a rectangle

DefinitionHorizontal lattice path rightward#✓fully proved

The horizontal lattice path from (t, row) right to (t + k, row).

def jec_hsegRight (row : ℤ) : (t : ℤ) → (k : ℕ) →
    (hypercubicLattice 2).Walk ![t, row] ![t + (k:ℤ), row]
  | t, 0 => (SimpleGraph.Walk.nil).copy rfl (by norm_num)
  | t, (k+1) => by
      have hadj : (hypercubicLattice 2).Adj ![t, row] ![t+1, row] := by
        simp [hypercubicLattice_adj, Fin.sum_univ_two]
      exact (SimpleGraph.Walk.cons hadj (jec_hsegRight row (t+1) k)).copy rfl
        (by push_cast; ring_nf)

Uses 2 · Used by 2

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

Used byOpen vertical crossings separate the sides of a rectangle · Return path around a rectangle

DefinitionReturn path around a rectangle#✓fully proved

A lattice path from (b0, d) back to (a0, c) running outside the rectangle [α, β] × [c, d]: up, left to column α - 1, down to row c - 1, right, and up.

StatMech.Lattice.jec_retPath · 16 lines

def jec_retPath (α a0 b0 c d : ℤ) (_ha : α ≤ a0) (_hb : α ≤ b0) (_hcd : c ≤ d) :
    (hypercubicLattice 2).Walk ![b0, d] ![a0, c] :=
  let s1 : (hypercubicLattice 2).Walk ![b0, d] ![b0, d+1] :=
    (jec_vsegUp b0 d 1).copy rfl (by ext i; fin_cases i <;> simp)
  let s2 : (hypercubicLattice 2).Walk ![b0, d+1] ![α-1, d+1] :=
    ((jec_hsegRight (d+1) (α-1) (b0-(α-1)).toNat).copy rfl
      (by ext i; fin_cases i <;> (simp; try omega))).reverse
  let s3 : (hypercubicLattice 2).Walk ![α-1, d+1] ![α-1, c-1] :=
    ((jec_vsegUp (α-1) (c-1) (d+1-(c-1)).toNat).copy rfl
      (by ext i; fin_cases i <;> (simp; try omega))).reverse
  let s4 : (hypercubicLattice 2).Walk ![α-1, c-1] ![a0, c-1] :=
    (jec_hsegRight (c-1) (α-1) (a0-(α-1)).toNat).copy rfl
      (by ext i; fin_cases i <;> (simp; try omega))
  let s5 : (hypercubicLattice 2).Walk ![a0, c-1] ![a0, c] :=
    (jec_vsegUp a0 (c-1) 1).copy rfl (by ext i; fin_cases i <;> simp)
  s1.append (s2.append (s3.append (s4.append s5)))

Uses 4 · Used by 1

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Horizontal lattice path rightward · Vertical lattice path upward

Used byOpen vertical crossings separate the sides of a rectangle

DefinitionHalf-plane below a row#✓fully proved

The half-plane of sites in rows below y.

def jec_belowSet (y : ℤ) : Set (Site 2) := {p | p 1 ≤ y - 1}

Uses 1 · Used by 1

Statement usesSite of the hypercubic lattice

Used byOpen vertical crossings separate the sides of a rectangle

TheoremOpen vertical crossings separate the sides of a rectangle#✓fully proved

For every configuration, every overlap rectangle, and every α < β, c ≤ d, the arc-side property StatMech.Universality.CrossingArcSides holds: an open vertical crossing of the overlap separates the left side of [α, β] × [c, d] from its right side.

theorem jec_crossingArcSides (ω : ConfigSpace (Sym2 (Site 2))) {α β m m' c d : ℤ}
    (hαβ : α < β) (hcd : c ≤ d) :
    StatMech.Universality.CrossingArcSides ω α β m m' c d

Uses 25

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Vertical overlap crossings separate the sides of a rectangle

Proof usesSeparating set for a lattice rectangle · Connection by an open path within a set · Boundary edge of a set · Number of boundary crossings of a walk · Hypercubic lattice \(\mathbb{Z}^d\) · Half-plane below a row · Horizontal lattice path rightward · Inside of a closed walk by the even-odd rule · Quadrant below and left of a site · Ray-crossing count of a walk · Ray edges left of a site · Return path around a rectangle · Vertical lattice path upward · Wall-crossing count of a walk · Wall edges below a site · Open subgraph induced on a set of sites · Bottom side of a general lattice rectangle · Integer rectangle in the plane lattice · Top side of a general lattice rectangle · Walk in an induced open subgraph as a lattice walk · Open cluster inside the overlap rectangle · Projection of an induced open subgraph to the lattice

DefinitionSet of sites is the inside of a closed lattice walk#✓fully proved

Some closed lattice walk has odd ray count exactly at the sites of K, so K is the inside of that walk.

def ccs_OrbitIsLoop (K : Set (Site 2)) : Prop :=
  ∃ (a : Site 2) (Vc : (hypercubicLattice 2).Walk a a),
    (∀ z, z ∈ K → ¬ Even (jec_rayCount z Vc)) ∧
    (∀ z, z ∉ K → Even (jec_rayCount z Vc))

Uses 3

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Ray-crossing count of a walk

DefinitionInside and outside of a closed walk are connected#✓fully proved

The inside and the outside of Vc are nonempty and each is connected in the lattice with the boundary edges of the inside removed. This is StatMech.Lattice.jcs_JordanRegion (jec_leftRegion Vc).

def egf_LoopFloodFill {a : Site 2} (Vc : (hypercubicLattice 2).Walk a a) : Prop :=
  (∃ x, x ∈ jec_leftRegion Vc) ∧ (∃ y, y ∉ jec_leftRegion Vc) ∧
    (∀ p q : Site 2, p ∈ jec_leftRegion Vc → q ∈ jec_leftRegion Vc →
        (latticeMinusBarrier (jec_leftRegion Vc)).Reachable p q) ∧
    (∀ p q : Site 2, p ∉ jec_leftRegion Vc → q ∉ jec_leftRegion Vc →
        (latticeMinusBarrier (jec_leftRegion Vc)).Reachable p q)

Uses 4

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Inside of a closed walk by the even-odd rule · Square lattice with the boundary edges of a set removed

DefinitionLattice off a closed walk#✓fully proved

The subgraph of the square lattice induced on the sites not visited by Vc.

noncomputable def fcb_offComplGraph {a : Site 2} (Vc : (hypercubicLattice 2).Walk a a) :
    SimpleGraph {z : Site 2 // z ∉ Vc.support} :=
  (ffc_offSupportLattice {z | z ∈ Vc.support}).induce {z : Site 2 | z ∉ Vc.support}

Uses 3 · Used by 2

Statement usesSite of the hypercubic lattice · Square lattice with a set of vertices removed · Hypercubic lattice \(\mathbb{Z}^d\)

Used byBoundary darts of a component off a closed walk · Facial orbits cover the components of the complement

DefinitionJordan region property off a closed walk#✓fully proved

Both sides of Vc contain sites off Vc, and any two sites off Vc on the same side are joined by a lattice path avoiding Vc.

def fcb_OffComplJordanRegion {a : Site 2} (Vc : (hypercubicLattice 2).Walk a a) : Prop :=
  (∃ x, x ∈ jec_leftRegion Vc ∧ x ∉ Vc.support) ∧
    (∃ y, y ∉ jec_leftRegion Vc ∧ y ∉ Vc.support) ∧
    (∀ s t : Site 2, s ∈ jec_leftRegion Vc → t ∈ jec_leftRegion Vc →
        s ∉ Vc.support → t ∉ Vc.support →
        ∃ p : (hypercubicLattice 2).Walk s t, ∀ z ∈ p.support, z ∉ Vc.support) ∧
    (∀ s t : Site 2, s ∉ jec_leftRegion Vc → t ∉ jec_leftRegion Vc →
        s ∉ Vc.support → t ∉ Vc.support →
        ∃ p : (hypercubicLattice 2).Walk s t, ∀ z ∈ p.support, z ∉ Vc.support)

Uses 3

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Inside of a closed walk by the even-odd rule

TheoremVeblen's theorem step for unions of cycles#✓fully proved

One step of Veblen's theorem (O. Veblen, 1912) for graphs whose vertices all have degree zero or two: a nonempty such graph has a subgraph of the same kind with fewer edges and face count one less (obtained by deleting a cycle).

theorem jvp_isCycles_veblenStep {V : Type*} [Finite V]
    (K : SimpleGraph V) [LocallyFinite K] (hcyc : K.IsCycles) (hne : K.edgeSet.Nonempty) :
    ∃ K' : SimpleGraph V, K' ≤ K ∧ K'.IsCycles ∧
      K'.edgeSet.ncard < K.edgeSet.ncard ∧ faceCount K' + 1 = faceCount K

Uses 5

Statement usesFace count of a finite graph from its cycle rank

Proof usesEdgeless graph has one component per vertex · Adding a new edge increases the edge count by one · Removing one element lowers cardinality by one · Cycle rank of a finite graph

DefinitionAdjacency relation of the cut horizontal axis#✓fully proved

Both sites lie on the horizontal axis and the pair is not {(0, 0), (1, 0)}.

def jkr_lineRel (a b : Site 2) : Prop :=
  a 1 = 0 ∧ b 1 = 0 ∧ ¬ ({a 0, b 0} = ({0, 1} : Finset ℤ))

Uses 1 · Used by 1

Statement usesSite of the hypercubic lattice

Used byHorizontal axis with one edge removed

DefinitionHorizontal axis with one edge removed#✓fully proved

The horizontal axis of ℤ² with the edge from (0, 0) to (1, 0) removed.

def jkr_lineH : SimpleGraph (Site 2) where
  Adj a b := (hypercubicLattice 2).Adj a b ∧ jkr_lineRel a b
  symm := by
    refine ⟨?_⟩
    rintro a b ⟨hadj, h0, h1, hne⟩
    refine ⟨hadj.symm, h1, h0, ?_⟩
    rwa [Finset.pair_comm]
  loopless := ⟨fun a h => (hypercubicLattice 2).irrefl h.1⟩

Uses 3

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Adjacency relation of the cut horizontal axis

DefinitionKeep-reconnect residue for finite graphs#✓fully proved

For every graph H of ℤ² with finitely many edges and every lattice edge pq outside H with dual edge f0g0: if p and q are disconnected in H, then f0 and g0 are connected in the face-region graph of H with f0g0 deleted.

def jkr_FiniteKeepReconnectResidue : Prop :=
  ∀ (H : SimpleGraph (Site 2)) (p q f0 g0 : Site 2),
    H.edgeSet.Finite →
    (hypercubicLattice 2).Adj p q → s(p, q) ∉ H.edgeSet →
    (hypercubicLattice 2).Adj f0 g0 → sharedPrimalEdge f0 g0 = s(p, q) →
    ¬ H.Reachable p q →
    ((whb_faceRegion H).deleteEdges {s(f0, g0)}).Reachable f0 g0

Uses 4 · Used by 1

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Primal edge shared by adjacent faces · Face-region graph of a square-lattice subgraph

Used byBounded faces of a finite lattice graph are counted by its cycle rank

DefinitionRotated region graph of a lattice subgraph#✓fully proved

The square lattice with the edge crossEdge e removed for every edge e of G. Since crossEdge is a global rotation, this is not the faithful dual complement; see StatMech.Lattice.whb_faceRegion for the version using sharedPrimalEdge.

def regionGraph (G : SimpleGraph (Site 2)) : SimpleGraph (Site 2) where
  Adj f g := (hypercubicLattice 2).Adj f g ∧ crossEdge.symm s(f, g) ∉ G.edgeSet
  symm := by
    refine ⟨?_⟩
    intro f g ⟨hadj, hcross⟩
    exact ⟨hadj.symm, by rwa [Sym2.eq_swap]⟩
  loopless := ⟨fun f h => (hypercubicLattice 2).irrefl h.1⟩

Uses 3 · Used by 5

Statement usesSite of the hypercubic lattice · Quarter-turn rotation of unordered site pairs · Hypercubic lattice \(\mathbb{Z}^d\)

Used byBounded regions are the components other than the outer one · Box exterior embeds in the region graph · Geometric count of bounded regions · Quarter-turn isomorphism onto the region graph · Outer region of the rotated region graph

StructurePlanar lattice subgraph of the square lattice#✓fully proved

A finite graph together with an injective map into ℤ² that sends edges to lattice edges.

structure PlanarZ2Subgraph where
  /-- The vertex type. -/
  V : Type
  /-- The vertex type is finite. -/
  finV : Finite V
  /-- Equality of vertices is decidable. -/
  decV : DecidableEq V
  /-- The abstract graph. -/
  G : SimpleGraph V
  /-- The embedding of the vertices into `ℤ²`. -/
  emb : V ↪ Site 2
  /-- Edges are mapped to lattice edges. -/
  isSub : ∀ ⦃x y : V⦄, G.Adj x y → (hypercubicLattice 2).Adj (emb x) (emb y)

Uses 2 · Used by 54

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

Used byBounded regions are the components other than the outer one · Box exterior embeds in the region graph · Geometric count of bounded regions · Image of a planar lattice subgraph in the square lattice · Disconnected sites are joined in the lattice minus a bridged graph · Unit square as a planar lattice subgraph · Bounded regions of a planar lattice subgraph · Bounded regions indexed by the cycle rank · 8-cycle around the L-tromino as a planar lattice subgraph · Jordan curve theorem · Cycle rank one gives a unique bounded region · Two corner-sharing unit squares as a planar lattice subgraph · Even-degree subgraphs have as many regions as their face count · Peeling a cycle from an even-degree subgraph · Bounded faces of a finite lattice graph are counted by its cycle rank · Pushforward of a subgraph into the square lattice · Whitney duality for even-degree planar lattice subgraphs · Pushed-forward subgraphs are locally finite · Outer face region of a planar lattice subgraph · Whitney cut-cycle duality for a planar lattice subgraph · Unit square with a pendant edge as a planar lattice subgraph · Number of face regions of a subgraph's image · Two disjoint unit squares as a planar lattice subgraph · 3 by 3 grid as a planar lattice subgraph · Region step property for even-degree subgraphs · Veblen step property for even-degree subgraphs · Radius of a box containing a planar lattice subgraph · Outer region of the rotated region graph · Lattice Jordan curve theorem for simple closed walks · Simple closed walk as an embedded cycle graph · Subgraph of a simple closed lattice walk has cycle rank one · Neighbours in the image graph are walk predecessor and successor · The inner face component is finite · A face far outside the walk has ray parity zero · Each walk step is an edge of the image graph · Simple closed walk as a planar subgraph · Consecutive left cells on a straight step are face-adjacent · Lattice Jordan curve theorem, even-odd form · Three walk edges cannot meet at a vertex · Cells on either side of a step lie in different faces · Number of cells is at most the nullity of the skeleton · 1-skeleton of a cell complex as a planar subgraph · Euler characteristic at most 1 for a connected skeleton · Cell complex edges lie in the embedded skeleton · Hopf's Umlaufsatz · Even-degree image of a planar lattice subgraph · Faithful discrete Jordan property for even-degree subgraphs · Whitney duality in the bridge direction · Faithful discrete Jordan statement for the face count · Number of bounded faces of a lattice subgraph · Face-boundary graph of a finite set as a planar subgraph · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionImage of a planar lattice subgraph in the square lattice#✓fully proved

The image of a PlanarZ2Subgraph as a subgraph of the square lattice.

noncomputable def imageGraph (P : PlanarZ2Subgraph) : SimpleGraph (Site 2) where
  Adj a b := ∃ x y : P.V, P.G.Adj x y ∧ P.emb x = a ∧ P.emb y = b
  symm := by
    refine ⟨?_⟩
    rintro a b ⟨x, y, hadj, rfl, rfl⟩
    exact ⟨y, x, hadj.symm, rfl, rfl⟩
  loopless := ⟨by
    rintro a ⟨x, y, hadj, hx, hy⟩
    have : x = y := P.emb.injective (hx.trans hy.symm)
    exact P.G.irrefl (this ▸ hadj)⟩

Uses 2 · Used by 43

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice

Used byBounded regions are the components other than the outer one · Box exterior embeds in the region graph · Geometric count of bounded regions · Bounded regions of a planar lattice subgraph · Bounded regions indexed by the cycle rank · Bounded faces of a finite lattice graph are counted by its cycle rank · Interior region of the unit square · Outer face region of a planar lattice subgraph · Outer region of the rotated region graph · Face-graph adjacency as absence of a walk step between cells · Ray-parity interior equals the bounded face components · Lattice Jordan curve theorem for simple closed walks · Neighbours in the image graph are walk predecessor and successor · The inner face component is finite · Face-adjacent cells have the same ray parity · Horizontally face-adjacent cells have the same ray parity · Vertically face-adjacent cells have the same ray parity · Each walk step is an edge of the image graph · Face graph of a closed walk · Vertices of a walk's image graph are adjacent only to walk neighbours · Consecutive left cells on a straight step are face-adjacent · Lattice Jordan curve theorem, even-odd form · Bounded face of a simple closed walk has no pinch points · Three walk edges cannot meet at a vertex · A side between interior and exterior cells is a walk edge · Cells on either side of a step lie in different faces · Number of cells is at most the nullity of the skeleton · Bounded face formed by a cell · Distinct cells form distinct bounded faces · Face component containing a cell · The face component of a cell is bounded · The face of a cell is enclosed on all four sides · The face of a cell is alone in its component · Cell complex edges lie in the embedded skeleton · Interior cells have connected lower-left corners · Hopf's Umlaufsatz · Even-degree image of a planar lattice subgraph · Faithful discrete Jordan statement for the face count · Number of bounded faces of a lattice subgraph · Unit square with its bottom edge removed · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionGeometric count of bounded regions#✓fully proved

The number of finite connected components of the region graph of P.

noncomputable def geometricRegionCount (P : PlanarZ2Subgraph) : ℕ :=
  Nat.card {c : (regionGraph (imageGraph P)).ConnectedComponent // c.supp.Finite}

Uses 4

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Image of a planar lattice subgraph in the square lattice · Rotated region graph of a lattice subgraph

DefinitionBox exterior embeds in the region graph#✓fully proved

Outside a box containing the image of P, the lattice embeds in the region graph.

noncomputable def exteriorToRegionHom (P : PlanarZ2Subgraph) (R : ℕ)
    (hR : ∀ v : P.V, P.emb v ∈ box 2 R) :
    ((hypercubicLattice 2).induce (exterior 2 R)) →g (regionGraph (imageGraph P)) where
  toFun := Subtype.val
  map_rel' := by
    intro a b hab
    exact regionGraph_adj_of_exterior P R hR (mem_box_compl_of_exterior a.2) hab

Uses 11 · Used by 1

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Quarter-turn rotation of unordered site pairs · Exterior of a box in \(\mathbb{Z}^d\) · Hypercubic lattice \(\mathbb{Z}^d\) · Image of a planar lattice subgraph in the square lattice · Rotated region graph of a lattice subgraph · Quarter-turn rotation as a permutation · Quarter-turn rotation of the square lattice · Inverse quarter-turn rotation

Used byBounded regions are the components other than the outer one

DefinitionEven-degree condition on a subgraph#✓fully proved

Every vertex of K has even degree.

def jcx_IsEven {V : Type*} (K : SimpleGraph V) : Prop :=
  ∀ v : V, Even (Nat.card (K.neighborSet v))

Used by 3

Used byEven-peelable graph · Bounded faces of a finite lattice graph are counted by its cycle rank · Cells on either side of a step lie in different faces

InductiveEven-peelable graph#✓fully proved

K reduces to the empty graph by repeatedly deleting a cycle through a base vertex v such that, after the deletion, the other vertices of the cycle are isolated.

inductive jcx_IsEvenPeelable {V : Type*} : SimpleGraph V → Prop where
  | bot : jcx_IsEvenPeelable (⊥ : SimpleGraph V)
  | cycle {K : SimpleGraph V} (hev : jcx_IsEven K) {v : V} (p : K.Walk v v) (hp : p.IsCycle)
      (hiso : ∀ u ∈ p.support, u ≠ v → ∀ w, ¬ (K.deleteEdges p.toSubgraph.edgeSet).Adj u w)
      (hrec : jcx_IsEvenPeelable (K.deleteEdges p.toSubgraph.edgeSet)) : jcx_IsEvenPeelable K

Uses 1

Statement usesEven-degree condition on a subgraph

DefinitionVertices of two unit squares sharing a corner#✓fully proved

The vertices of two unit squares [0, 1]² and [1, 2]² sharing the corner (1, 1).

def jcx_cross_emb (i : Fin 7) : Site 2 :=
  match i with
  | 0 => ![0, 0] | 1 => ![1, 0] | 2 => ![1, 1] | 3 => ![0, 1]
  | 4 => ![2, 1] | 5 => ![2, 2] | 6 => ![1, 2]

Uses 1 · Used by 1

Statement usesSite of the hypercubic lattice

Used byTwo corner-sharing unit squares as a planar lattice subgraph

DefinitionAdjacency relation of two corner-sharing squares#✓fully proved

Adjacency of the two squares sharing a corner, as a Boolean relation.

def jcx_cross_rel (i j : Fin 7) : Bool :=
  (i == 0 && j == 1) || (i == 1 && j == 0) || (i == 1 && j == 2) || (i == 2 && j == 1) ||
  (i == 2 && j == 3) || (i == 3 && j == 2) || (i == 3 && j == 0) || (i == 0 && j == 3) ||
  (i == 2 && j == 4) || (i == 4 && j == 2) || (i == 4 && j == 5) || (i == 5 && j == 4) ||
  (i == 5 && j == 6) || (i == 6 && j == 5) || (i == 6 && j == 2) || (i == 2 && j == 6)

Used by 3

Used byUpper 4-cycle based at the shared vertex · Two 4-cycles sharing a vertex · Two corner-sharing unit squares as a planar lattice subgraph

DefinitionTwo 4-cycles sharing a vertex#✓fully proved

Two 4-cycles sharing the vertex 2, on Fin 7.

def jcx_cross_G : SimpleGraph (Fin 7) where
  Adj i j := jcx_cross_rel i j
  symm := ⟨by intro i j h; revert h; revert i j; decide⟩
  loopless := ⟨by intro i h; revert h; revert i; decide⟩

Uses 1 · Used by 2

Statement usesAdjacency relation of two corner-sharing squares

Used byUpper 4-cycle based at the shared vertex · Two corner-sharing unit squares as a planar lattice subgraph

DefinitionTwo corner-sharing unit squares as a planar lattice subgraph#✓fully proved

Two unit squares sharing a corner as a PlanarZ2Subgraph.

noncomputable def jcx_cross_P : PlanarZ2Subgraph where
  V := Fin 7
  finV := inferInstance
  decV := inferInstance
  G := jcx_cross_G
  emb := ⟨jcx_cross_emb, jcx_cross_emb_inj⟩
  isSub := jcx_cross_isSub

Uses 6

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Two 4-cycles sharing a vertex · Vertices of two unit squares sharing a corner · Adjacency relation of two corner-sharing squares

DefinitionUpper 4-cycle based at the shared vertex#✓fully proved

The 4-cycle of the upper square, based at the shared vertex.

def jcx_cross_cycB : jcx_cross_G.Walk 2 2 :=
  Walk.cons (by rw [jcx_cross_G_adj]; decide : jcx_cross_G.Adj 2 4)
    (Walk.cons (by rw [jcx_cross_G_adj]; decide : jcx_cross_G.Adj 4 5)
      (Walk.cons (by rw [jcx_cross_G_adj]; decide : jcx_cross_G.Adj 5 6)
        (Walk.cons (by rw [jcx_cross_G_adj]; decide : jcx_cross_G.Adj 6 2) Walk.nil)))

Uses 2

Statement usesTwo 4-cycles sharing a vertex · Adjacency relation of two corner-sharing squares

DefinitionAdjacency relation of the lower 4-cycle#✓fully proved

Adjacency of the lower 4-cycle, as a Boolean relation.

def jcx_cross_A_rel (i j : Fin 7) : Bool :=
  (i == 0 && j == 1) || (i == 1 && j == 0) || (i == 1 && j == 2) || (i == 2 && j == 1) ||
  (i == 2 && j == 3) || (i == 3 && j == 2) || (i == 3 && j == 0) || (i == 0 && j == 3)

Used by 1

Used byLower 4-cycle left after deleting the upper one

DefinitionLower 4-cycle left after deleting the upper one#✓fully proved

The lower 4-cycle, which remains after deleting the upper one.

def jcx_cross_A : SimpleGraph (Fin 7) where
  Adj i j := jcx_cross_A_rel i j
  symm := ⟨by intro i j h; revert h; revert i j; decide⟩
  loopless := ⟨by intro i h; revert h; revert i; decide⟩

Uses 1

Statement usesAdjacency relation of the lower 4-cycle

DefinitionPushforward of a subgraph into the square lattice#✓fully proved

The image in ℤ² of a subgraph K of a PlanarZ2Subgraph P.

noncomputable def jei_pushGraph (P : PlanarZ2Subgraph) (K : SimpleGraph P.V) :
    SimpleGraph (Site 2) where
  Adj a b := ∃ x y : P.V, K.Adj x y ∧ P.emb x = a ∧ P.emb y = b
  symm := ⟨by rintro a b ⟨x, y, hadj, rfl, rfl⟩; exact ⟨y, x, hadj.symm, rfl, rfl⟩⟩
  loopless := ⟨by
    rintro a ⟨x, y, hadj, hx, hy⟩
    have : x = y := P.emb.injective (hx.trans hy.symm)
    exact K.irrefl (this ▸ hadj)⟩

Uses 2 · Used by 11

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice

Used byDisconnected sites are joined in the lattice minus a bridged graph · Even-degree subgraphs have as many regions as their face count · Peeling a cycle from an even-degree subgraph · Bounded faces of a finite lattice graph are counted by its cycle rank · Pushed-forward subgraphs are locally finite · Whitney cut-cycle duality for a planar lattice subgraph · Number of face regions of a subgraph's image · Region step property for even-degree subgraphs · Veblen step property for even-degree subgraphs · Cells on either side of a step lie in different faces · Whitney duality in the bridge direction

DefinitionEven-degree subgraphs have as many regions as their face count#✓fully proved

Every subgraph K of P whose image has all degrees even has exactly faceCount K face-region components.

def jcx_EvenCountResidue (P : PlanarZ2Subgraph) : Prop :=
  ∀ (K : SimpleGraph P.V), K ≤ P.G →
    jce_ClosedContour (jei_pushGraph P K).edgeSet →
    Nat.card (whb_faceRegion (jei_pushGraph P K)).ConnectedComponent = faceCount K

Uses 6

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Face count of a finite graph from its cycle rank · Closed contour as an even-degree edge set · Pushforward of a subgraph into the square lattice · Face-region graph of a square-lattice subgraph

DefinitionPeeling a cycle from an even-degree subgraph#✓fully proved

Every nonempty subgraph K of P whose image has all degrees even contains a subgraph of the same kind with fewer edges, face count one less, and one fewer face-region component.

def jcx_EvenPeel (P : PlanarZ2Subgraph) : Prop :=
  ∀ (K : SimpleGraph P.V), K ≤ P.G → jce_ClosedContour (jei_pushGraph P K).edgeSet →
    K ≠ ⊥ →
    ∃ K' : SimpleGraph P.V, K' ≤ P.G ∧ jce_ClosedContour (jei_pushGraph P K').edgeSet ∧
      K'.edgeSet.ncard < K.edgeSet.ncard ∧
      faceCount K' + 1 = faceCount K ∧
      Nat.card (whb_faceRegion (jei_pushGraph P K)).ConnectedComponent
        = Nat.card (whb_faceRegion (jei_pushGraph P K')).ConnectedComponent + 1

Uses 6

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Face count of a finite graph from its cycle rank · Closed contour as an even-degree edge set · Pushforward of a subgraph into the square lattice · Face-region graph of a square-lattice subgraph

DefinitionSquare lattice minus the edges of a graph#✓fully proved

The square lattice with the edges of H deleted.

noncomputable def jbc_latticeMinusEdges (H : SimpleGraph (Site 2)) : SimpleGraph (Site 2) :=
  (hypercubicLattice 2).deleteEdges H.edgeSet

Uses 2 · Used by 2

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

Used byDisconnected sites are joined in the lattice minus a bridged graph · Quarter-turn isomorphism onto the region graph

DefinitionQuarter-turn isomorphism onto the region graph#✓fully proved

The quarter-turn rotation is an isomorphism from the lattice minus the edges of H onto the region graph of H.

noncomputable def jbc_rotIso (H : SimpleGraph (Site 2)) :
    jbc_latticeMinusEdges H ≃g regionGraph H where
  toEquiv := rot90Equiv
  map_rel_iff' := by
    intro a b
    rw [rot90Equiv_apply, rot90Equiv_apply, jbc_regionGraph_rot_adj]

Uses 8

Statement usesSite of the hypercubic lattice · Quarter-turn rotation of unordered site pairs · Hypercubic lattice \(\mathbb{Z}^d\) · Square lattice minus the edges of a graph · Rotated region graph of a lattice subgraph · Quarter-turn rotation as a permutation · Quarter-turn rotation of the square lattice · Inverse quarter-turn rotation

DefinitionDisconnected sites are joined in the lattice minus a bridged graph#✓fully proved

If x and y are not connected in K, they are connected in the lattice minus the image of K ⊔ edge x y.

def jbc_BridgeDirection (P : PlanarZ2Subgraph) : Prop :=
  ∀ (K : SimpleGraph P.V), K ≤ P.G → ∀ {x y : P.V}, P.G.Adj x y → ¬ K.Adj x y →
    ¬ K.Reachable x y →
      (jbc_latticeMinusEdges (jei_pushGraph P (K ⊔ edge x y))).Reachable (P.emb x) (P.emb y)

Uses 4

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Square lattice minus the edges of a graph · Pushforward of a subgraph into the square lattice

DefinitionCorners of the unit square in cyclic order#✓fully proved

The four corners (0, 0), (1, 0), (1, 1), (0, 1) of the unit square, in cyclic order.

def jbc_csq (i : Fin 4) : Site 2 :=
  match i with
  | 0 => ![0, 0] | 1 => ![1, 0] | 2 => ![1, 1] | 3 => ![0, 1]

Uses 1 · Used by 1

Statement usesSite of the hypercubic lattice

Used byUnit square as a planar lattice subgraph

DefinitionAdjacency relation of the 4-cycle#✓fully proved

Adjacency of the 4-cycle 0 – 1 – 2 – 3 – 0, as a Boolean relation.

def jbc_cyc4Rel (i j : Fin 4) : Bool :=
  (i == 0 && j == 1) || (i == 1 && j == 0) || (i == 1 && j == 2) || (i == 2 && j == 1) ||
    (i == 2 && j == 3) || (i == 3 && j == 2) || (i == 3 && j == 0) || (i == 0 && j == 3)

Used by 2

Used byThe 4-cycle graph · Unit square as a planar lattice subgraph

DefinitionThe 4-cycle graph#✓fully proved

The 4-cycle on Fin 4.

def jbc_cyc4 : SimpleGraph (Fin 4) where
  Adj i j := jbc_cyc4Rel i j
  symm := ⟨by intro i j h; revert h; revert i j; decide⟩
  loopless := ⟨by intro i h; revert h; revert i; decide⟩

Uses 1 · Used by 1

Statement usesAdjacency relation of the 4-cycle

Used byUnit square as a planar lattice subgraph

DefinitionVertex 0 of the 4-cycle#✓fully proved

The vertex 0 of the 4-cycle.

def jbc_v0 : Fin 4 := 0

DefinitionVertex 1 of the 4-cycle#✓fully proved

The vertex 1 of the 4-cycle.

def jbc_v1 : Fin 4 := 1

DefinitionUnit square as a planar lattice subgraph#✓fully proved

The unit square: the 4-cycle embedded on the corners of [0, 1]².

noncomputable def jbc_Pce : PlanarZ2Subgraph where
  V := Fin 4
  finV := inferInstance
  decV := inferInstance
  G := jbc_cyc4
  emb := ⟨jbc_csq, jbc_csq_inj⟩
  isSub := jbc_csq_isSub

Uses 6 · Used by 2

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Corners of the unit square in cyclic order · The 4-cycle graph · Adjacency relation of the 4-cycle

Used byInterior region of the unit square · Unit square with its bottom edge removed

InductiveCactus graph, defined by peeling leaves and cycles#✓fully proved

K reduces to the empty graph by repeatedly deleting a leaf edge or, when K is a union of cycles, one of its cycles.

inductive jgc_IsCactus {V : Type*} : SimpleGraph V → Prop where
  | bot : jgc_IsCactus (⊥ : SimpleGraph V)
  | leaf {K : SimpleGraph V} {x z : V} (hadj : K.Adj x z) (huniq : ∀ w, K.Adj x w → w = z)
      (hrec : jgc_IsCactus (K.deleteEdges {s(x, z)})) : jgc_IsCactus K
  | cycle {K : SimpleGraph V} (hcyc : K.IsCycles) {v : V} (p : K.Walk v v) (hp : p.IsCycle)
      (hrec : jgc_IsCactus (K.deleteEdges p.toSubgraph.edgeSet)) : jgc_IsCactus K

DefinitionUnit square corners with a pendant site#✓fully proved

The corners of the unit square together with the site (-1, 0).

def jgc_pend_emb (i : Fin 5) : Site 2 :=
  match i with
  | 0 => ![0, 0] | 1 => ![1, 0] | 2 => ![1, 1] | 3 => ![0, 1] | 4 => ![-1, 0]

Uses 1 · Used by 1

Statement usesSite of the hypercubic lattice

Used byUnit square with a pendant edge as a planar lattice subgraph

DefinitionAdjacency relation of a 4-cycle with a pendant edge#✓fully proved

Adjacency of the 4-cycle on 0, 1, 2, 3 with the pendant edge {0, 4}, as a Boolean relation.

def jgc_pend_rel (i j : Fin 5) : Bool :=
  (i == 0 && j == 1) || (i == 1 && j == 0) || (i == 1 && j == 2) || (i == 2 && j == 1) ||
  (i == 2 && j == 3) || (i == 3 && j == 2) || (i == 3 && j == 0) || (i == 0 && j == 3) ||
  (i == 0 && j == 4) || (i == 4 && j == 0)

Used by 2

Used by4-cycle with a pendant edge · Unit square with a pendant edge as a planar lattice subgraph

Definition4-cycle with a pendant edge#✓fully proved

The 4-cycle with a pendant edge, on Fin 5.

def jgc_pend_G : SimpleGraph (Fin 5) where
  Adj i j := jgc_pend_rel i j
  symm := ⟨by intro i j h; revert h; revert i j; decide⟩
  loopless := ⟨by intro i h; revert h; revert i; decide⟩

Uses 1 · Used by 1

Statement usesAdjacency relation of a 4-cycle with a pendant edge

Used byUnit square with a pendant edge as a planar lattice subgraph

DefinitionUnit square with a pendant edge as a planar lattice subgraph#✓fully proved

The unit square with a pendant edge as a PlanarZ2Subgraph.

noncomputable def jgc_pend_P : PlanarZ2Subgraph where
  V := Fin 5
  finV := inferInstance
  decV := inferInstance
  G := jgc_pend_G
  emb := ⟨jgc_pend_emb, jgc_pend_emb_inj⟩
  isSub := jgc_pend_isSub

Uses 6

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · 4-cycle with a pendant edge · Unit square corners with a pendant site · Adjacency relation of a 4-cycle with a pendant edge

Definition4-cycle core of the pendant example#✓fully proved

The 4-cycle on 0, 1, 2, 3 inside Fin 5.

def jgc_pend_core : SimpleGraph (Fin 5) where
  Adj i j :=
    ((i == 0 && j == 1) || (i == 1 && j == 0) || (i == 1 && j == 2) || (i == 2 && j == 1) ||
     (i == 2 && j == 3) || (i == 3 && j == 2) || (i == 3 && j == 0) || (i == 0 && j == 3) : Bool)
  symm := ⟨by intro i j h; revert h; revert i j; decide⟩
  loopless := ⟨by intro i h; revert h; revert i; decide⟩

DefinitionNumber of face regions of a subgraph's image#✓fully proved

The number of connected components of the face-region graph of the image of K.

noncomputable def jic_tc (P : PlanarZ2Subgraph) (K : SimpleGraph P.V) : ℕ :=
  Nat.card (whb_faceRegion (jei_pushGraph P K)).ConnectedComponent

Uses 4

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Pushforward of a subgraph into the square lattice · Face-region graph of a square-lattice subgraph

DefinitionCorners of two distant unit squares#✓fully proved

The corners of the unit squares at (0, 0) and (10, 0).

def jic_twoSq_emb (i : Fin 8) : Site 2 :=
  match i with
  | 0 => ![0, 0] | 1 => ![1, 0] | 2 => ![1, 1] | 3 => ![0, 1]
  | 4 => ![10, 0] | 5 => ![11, 0] | 6 => ![11, 1] | 7 => ![10, 1]

Uses 1 · Used by 1

Statement usesSite of the hypercubic lattice

Used byTwo disjoint unit squares as a planar lattice subgraph

DefinitionAdjacency relation of two disjoint 4-cycles#✓fully proved

Adjacency of two disjoint 4-cycles on Fin 8, as a Boolean relation.

def jic_twoSq_rel (i j : Fin 8) : Bool :=
  (i == 0 && j == 1) || (i == 1 && j == 0) || (i == 1 && j == 2) || (i == 2 && j == 1) ||
  (i == 2 && j == 3) || (i == 3 && j == 2) || (i == 3 && j == 0) || (i == 0 && j == 3) ||
  (i == 4 && j == 5) || (i == 5 && j == 4) || (i == 5 && j == 6) || (i == 6 && j == 5) ||
  (i == 6 && j == 7) || (i == 7 && j == 6) || (i == 7 && j == 4) || (i == 4 && j == 7)

Used by 2

Used byTwo disjoint 4-cycles · Two disjoint unit squares as a planar lattice subgraph

DefinitionTwo disjoint 4-cycles#✓fully proved

Two disjoint 4-cycles on Fin 8.

def jic_twoSq_G : SimpleGraph (Fin 8) where
  Adj i j := jic_twoSq_rel i j
  symm := ⟨by intro i j h; revert h; revert i j; decide⟩
  loopless := ⟨by intro i h; revert h; revert i; decide⟩

Uses 1 · Used by 1

Statement usesAdjacency relation of two disjoint 4-cycles

Used byTwo disjoint unit squares as a planar lattice subgraph

DefinitionTwo disjoint unit squares as a planar lattice subgraph#✓fully proved

Two disjoint unit squares as a PlanarZ2Subgraph.

noncomputable def jic_twoSq_P : PlanarZ2Subgraph where
  V := Fin 8
  finV := inferInstance
  decV := inferInstance
  G := jic_twoSq_G
  emb := ⟨jic_twoSq_emb, jic_twoSq_emb_inj⟩
  isSub := jic_twoSq_isSub

Uses 6

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Two disjoint 4-cycles · Corners of two distant unit squares · Adjacency relation of two disjoint 4-cycles

DefinitionRadius of a box containing a planar lattice subgraph#✓fully proved

A radius R such that the image of P lies in box 2 R.

noncomputable def outerBoxRadius (P : PlanarZ2Subgraph) : ℕ := (image_subset_box P).choose

Uses 4 · Used by 11

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Every finite set of sites lies in a box

Used byBounded regions are the components other than the outer one · Bounded faces of a finite lattice graph are counted by its cycle rank · Outer face region of a planar lattice subgraph · Outer region of the rotated region graph · The inner face component is finite · A face far outside the walk has ray parity zero · Lattice Jordan curve theorem, even-odd form · Hopf's Umlaufsatz · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionOuter region of the rotated region graph#✓fully proved

The outer region: the component of the region graph containing the far site beacon 2 R.

noncomputable def outerRegion (P : PlanarZ2Subgraph) :
    (regionGraph (imageGraph P)).ConnectedComponent :=
  (regionGraph (imageGraph P)).connectedComponentMk (beacon 2 (outerBoxRadius P))

Uses 6 · Used by 1

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Base point of the exterior of a box · Image of a planar lattice subgraph in the square lattice · Radius of a box containing a planar lattice subgraph · Rotated region graph of a lattice subgraph

Used byBounded regions are the components other than the outer one

DefinitionBounded regions are the components other than the outer one#✓fully proved

The finite components of the region graph are exactly the components other than the outer region.

def boundedRegionEquivNeOuter (P : PlanarZ2Subgraph) :
    {C : (regionGraph (imageGraph P)).ConnectedComponent // C.supp.Finite} ≃
      {C : (regionGraph (imageGraph P)).ConnectedComponent // C ≠ outerRegion P} :=
  Equiv.subtypeEquivRight (boundedRegion_iff_ne_outer P)

Uses 13

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Base point of the exterior of a box · Box \((-n, n)^d\) in the hypercubic lattice · Exterior of a box in \(\mathbb{Z}^d\) · Box exterior embeds in the region graph · Every finite set of sites lies in a box · Hypercubic lattice \(\mathbb{Z}^d\) · Image of a planar lattice subgraph in the square lattice · Radius of a box containing a planar lattice subgraph · Outer region of the rotated region graph · Rotated region graph of a lattice subgraph · Setting a set of coordinates of a lattice site

DefinitionWhitney cut-cycle duality for a planar lattice subgraph#✓fully proved

Whitney's cut–cycle duality for P: for every subgraph K of P and edge xy of P not in K, with f0g0 the dual edge across it, x and y are connected in K iff f0 and g0 are disconnected in the face-region graph of K with f0g0 deleted.

def jfc_WhbSync (P : PlanarZ2Subgraph) : Prop :=
  ∀ (K : SimpleGraph P.V), K ≤ P.G → ∀ {x y : P.V}, P.G.Adj x y → ¬ K.Adj x y →
    ∀ {f0 g0 : Site 2}, (hypercubicLattice 2).Adj f0 g0 →
      sharedPrimalEdge f0 g0 = s(P.emb x, P.emb y) →
      (K.Reachable x y ↔
        ¬ ((whb_faceRegion (jei_pushGraph P K)).deleteEdges {s(f0, g0)}).Reachable f0 g0)

Uses 6 · Used by 2

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Pushforward of a subgraph into the square lattice · Primal edge shared by adjacent faces · Face-region graph of a square-lattice subgraph

Used byBounded faces of a finite lattice graph are counted by its cycle rank · Whitney duality for even-degree planar lattice subgraphs

DefinitionOuter face region of a planar lattice subgraph#✓fully proved

The outer region: the component of the face-region graph of P containing a face far from P.

noncomputable def jfc_whb_outerRegion (P : PlanarZ2Subgraph) :
    (whb_faceRegion (imageGraph P)).ConnectedComponent :=
  (whb_faceRegion (imageGraph P)).connectedComponentMk (beacon 2 (outerBoxRadius P + 1))

Uses 6 · Used by 7

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Base point of the exterior of a box · Image of a planar lattice subgraph in the square lattice · Radius of a box containing a planar lattice subgraph · Face-region graph of a square-lattice subgraph

Used byBounded faces of a finite lattice graph are counted by its cycle rank · The inner face component is finite · Lattice Jordan curve theorem, even-odd form · Hopf's Umlaufsatz · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionPushed-forward subgraphs are locally finite#✓fully proved

The image of a subgraph of a PlanarZ2Subgraph is locally finite.

@[instance_reducible]
noncomputable def jfc_pushGraph_locallyFinite (P : PlanarZ2Subgraph) (K : SimpleGraph P.V)
    (hKle : K ≤ P.G) : SimpleGraph.LocallyFinite (jei_pushGraph P K) := fun _v =>
  Set.Finite.fintype (Set.Finite.subset (Set.toFinite _) (fun _w hw =>
    (SimpleGraph.mem_neighborSet _ _ _).mpr (jfc_pushGraph_le_lattice P K hKle hw)))

Uses 8 · Used by 2

Statement usesNearest neighbours in \(\mathbb{Z}^d\) · Planar lattice subgraph of the square lattice · Site of the hypercubic lattice · Nearest neighbours of a lattice site · Neighbour of a site in a coordinate direction · Hypercubic lattice \(\mathbb{Z}^d\) · Pushforward of a subgraph into the square lattice · Shift of a site along a coordinate

Used byBounded faces of a finite lattice graph are counted by its cycle rank · Cells on either side of a step lie in different faces

DefinitionWhitney duality for even-degree planar lattice subgraphs#✓fully proved

Every PlanarZ2Subgraph whose image has all degrees even satisfies jfc_WhbSync.

def jfc_EvenDegreeThreading : Prop :=
  ∀ (P : PlanarZ2Subgraph), jeb_EvenDegreeSubgraph P → jfc_WhbSync P

Uses 3

Statement usesPlanar lattice subgraph of the square lattice · Even-degree image of a planar lattice subgraph · Whitney cut-cycle duality for a planar lattice subgraph

DefinitionInterior region of the unit square#✓fully proved

The component of the face (0, 0) in the face-region graph of the unit square.

noncomputable def jfc_sq_interior : (whb_faceRegion (imageGraph jbc_Pce)).ConnectedComponent :=
  (whb_faceRegion (imageGraph jbc_Pce)).connectedComponentMk ![0, 0]

Uses 4

Statement usesSite of the hypercubic lattice · Image of a planar lattice subgraph in the square lattice · Unit square as a planar lattice subgraph · Face-region graph of a square-lattice subgraph

DefinitionVeblen step property for even-degree subgraphs#✓fully proved

Every nonempty subgraph K of P with even-degree image contains an even-degree subgraph with fewer edges and face count one less.

def jvp_VeblenStep (P : PlanarZ2Subgraph) : Prop :=
  ∀ (K : SimpleGraph P.V), K ≤ P.G → jce_ClosedContour (jei_pushGraph P K).edgeSet → K ≠ ⊥ →
    ∃ K' : SimpleGraph P.V, K' ≤ K ∧ jce_ClosedContour (jei_pushGraph P K').edgeSet ∧
      K'.edgeSet.ncard < K.edgeSet.ncard ∧ faceCount K' + 1 = faceCount K

Uses 5

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Face count of a finite graph from its cycle rank · Closed contour as an even-degree edge set · Pushforward of a subgraph into the square lattice

DefinitionRegion step property for even-degree subgraphs#✓fully proved

Whenever K' ≤ K are even-degree subgraphs of P with fewer edges and face count one less, the face-region graph of K has one more component than that of K'.

def jvp_RegionStep (P : PlanarZ2Subgraph) : Prop :=
  ∀ (K K' : SimpleGraph P.V), K ≤ P.G → K' ≤ K →
    jce_ClosedContour (jei_pushGraph P K).edgeSet →
    jce_ClosedContour (jei_pushGraph P K').edgeSet →
    K'.edgeSet.ncard < K.edgeSet.ncard → faceCount K' + 1 = faceCount K →
    Nat.card (whb_faceRegion (jei_pushGraph P K)).ConnectedComponent
      = Nat.card (whb_faceRegion (jei_pushGraph P K')).ConnectedComponent + 1

Uses 6

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Face count of a finite graph from its cycle rank · Closed contour as an even-degree edge set · Pushforward of a subgraph into the square lattice · Face-region graph of a square-lattice subgraph

DefinitionNine sites of a 3 by 3 grid#✓fully proved

The nine sites of [0, 2]², indexed row by row.

def jkd_gr9emb (i : Fin 9) : Site 2 :=
  match i with
  | 0 => ![0, 0] | 1 => ![1, 0] | 2 => ![2, 0]
  | 3 => ![0, 1] | 4 => ![1, 1] | 5 => ![2, 1]
  | 6 => ![0, 2] | 7 => ![1, 2] | 8 => ![2, 2]

Uses 1 · Used by 1

Statement usesSite of the hypercubic lattice

Used by3 by 3 grid as a planar lattice subgraph

DefinitionAdjacency relation of the 3 by 3 grid#✓fully proved

Adjacency of the 3 × 3 grid on Fin 9, as a Boolean relation.

def jkd_gr9rel (i j : Fin 9) : Bool :=
  let ci := (i : ℕ) % 3; let ri := (i : ℕ) / 3
  let cj := (j : ℕ) % 3; let rj := (j : ℕ) / 3
  (ci == cj && (ri == rj + 1 || rj == ri + 1)) || (ri == rj && (ci == cj + 1 || cj == ci + 1))

Used by 2

Used byThe 3 by 3 grid graph · 3 by 3 grid as a planar lattice subgraph

DefinitionThe 3 by 3 grid graph#✓fully proved

The 3 × 3 grid graph on Fin 9.

def jkd_gr9G : SimpleGraph (Fin 9) where
  Adj i j := jkd_gr9rel i j
  symm := ⟨by intro i j h; revert h; revert i j; decide⟩
  loopless := ⟨by intro i h; revert h; revert i; decide⟩

Uses 1 · Used by 1

Statement usesAdjacency relation of the 3 by 3 grid

Used by3 by 3 grid as a planar lattice subgraph

Definition3 by 3 grid as a planar lattice subgraph#✓fully proved

The 3 × 3 grid as a PlanarZ2Subgraph.

noncomputable def jkd_ringP : PlanarZ2Subgraph where
  V := Fin 9
  finV := inferInstance
  decV := inferInstance
  G := jkd_gr9G
  emb := ⟨jkd_gr9emb, jkd_gr9emb_inj⟩
  isSub := jkd_gr9_isSub

Uses 6

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · The 3 by 3 grid graph · Nine sites of a 3 by 3 grid · Adjacency relation of the 3 by 3 grid

DefinitionGrid vertex \((0, 0)\)#✓fully proved

The vertex (0, 0) of the grid.

def jkd_r0 : Fin 9 := 0

DefinitionGrid vertex \((1, 0)\)#✓fully proved

The vertex (1, 0) of the grid.

def jkd_r1 : Fin 9 := 1

TheoremAdding an edge between two components merges them#✓fully proved

Adding an edge between two components merges them. This assumes only finitely many components; see also StatMech.Lattice.card_components_sup_edge_of_not_reachable for finite vertex types.

theorem jsf_card_components_sup_edge_merge {V : Type*}
    (G : SimpleGraph V) [Finite G.ConnectedComponent] {a b : V} (hab : ¬ G.Reachable a b) :
    Nat.card (G ⊔ edge a b).ConnectedComponent + 1 = Nat.card G.ConnectedComponent

Uses 1 · Used by 1

Proof usesRemoving one element lowers cardinality by one

Used byBounded faces of a finite lattice graph are counted by its cycle rank

DefinitionCut set of a face coloring#✓fully proved

The primal edges sharedPrimalEdge a b between adjacent faces a, b on which T takes different values.

def jed_cutSet (T : Site 2 → Prop) : Set (Sym2 (Site 2)) :=
  {e | ∃ a b : Site 2, (hypercubicLattice 2).Adj a b ∧ e = sharedPrimalEdge a b ∧ (T a ↔ ¬ T b)}

Uses 3 · Used by 1

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Primal edge shared by adjacent faces

Used byBounded faces of a finite lattice graph are counted by its cycle rank

DefinitionLattice graph spanned by an edge set#✓fully proved

The graph on ℤ² whose edges are the lattice edges in E.

def jed_primalGraph (E : Set (Sym2 (Site 2))) : SimpleGraph (Site 2) where
  Adj u w := (hypercubicLattice 2).Adj u w ∧ s(u, w) ∈ E
  symm := ⟨by rintro u w ⟨h1, h2⟩; exact ⟨h1.symm, by rwa [Sym2.eq_swap]⟩⟩
  loopless := ⟨fun u h => (hypercubicLattice 2).irrefl h.1⟩

Uses 2 · Used by 2

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

Used byBoundary of a 3 by 3 rectangle as a graph · Bounded faces of a finite lattice graph are counted by its cycle rank

TheoremBounded faces of a finite lattice graph are counted by its cycle rank#✓fully proved

For a PlanarZ2Subgraph P, the finite components of the face-region graph whb_faceRegion of its image (faces of ℤ², two adjacent faces joined unless the primal edge between them lies in P) are equinumerous with Fin (nullity P.G), so the number of bounded faces is |E| - |V| + c. This is a count: it does not identify each bounded face with the interior of a particular cycle of P. References: H. Whitney, Planar graphs (1933); C. Thomassen, The Jordan–Schönflies theorem and the classification of surfaces (1992).

theorem jed_faithfulDiscreteJordan (P : PlanarZ2Subgraph) : whc_FaithfulDiscreteJordan P

Uses 57 · Used by 5

Statement usesPlanar lattice subgraph of the square lattice · Faithful discrete Jordan statement for the face count

Proof usesNearest neighbours in \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Base point of the exterior of a box · Box \((-n, n)^d\) in the hypercubic lattice · Nearest neighbours of a lattice site · Neighbour of a site in a coordinate direction · Edgeless graph has one component per vertex · Adding a new edge increases the edge count by one · Removing one element lowers cardinality by one · Exterior of a box in \(\mathbb{Z}^d\) · 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)\) · Face count of a finite graph from its cycle rank · Every finite set of sites lies in a box · Hypercubic lattice \(\mathbb{Z}^d\) · Square lattice is connected · Image of a planar lattice subgraph in the square lattice · Closed contour as an even-degree edge set · Number of horizontal contour edges below a height · Parity coloring changes across vertical contour edges · Degree of a site in an edge set · Edge flip relation of an edge set · Horizontal edges below a face in its column · Four nearest neighbours of a site · Parity coloring of faces by an edge set · Even-degree condition on a subgraph · Two odd-degree vertices lie in one component · Cut set of a face coloring · Lattice graph spanned by an edge set · Pushforward of a subgraph into the square lattice · Whitney cut-cycle duality for a planar lattice subgraph · Pushed-forward subgraphs are locally finite · Outer face region of a planar lattice subgraph · Keep-reconnect residue for finite graphs · Adding an edge between two components merges them · Whitney duality in the bridge direction · Spanning subgraph formed by a path · Closed face walk around a lattice vertex · Cycle rank of a finite graph · Radius of a box containing a planar lattice subgraph · Setting a set of coordinates of a lattice site · Primal edge shared by adjacent faces · Shift of a site along a coordinate · Even-flip condition on closed lattice walks · Symmetry of a flip relation on lattice edges · Chosen lattice walk between two faces · Cut flip relation of a lattice graph and a dual edge · Number of flips along a lattice walk · Face coloring by parity of flips · Face-region graph of a square-lattice subgraph · Cut coloring of a subgraph with an extra dual edge · Number of bounded faces of a lattice subgraph · Primal edge between two faces lies in a subgraph

Used byBounded regions indexed by the cycle rank · Lattice Jordan curve theorem for simple closed walks · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionTwelve boundary edges of a 3 by 3 rectangle#✓fully proved

The twelve lattice edges of the boundary of the rectangle [-1, 2] × [-2, 1].

noncomputable def jed_boxEdges : Finset (Sym2 (Site 2)) :=
  { s(![(-1:ℤ), -2], ![0, -2]), s(![(0:ℤ), -2], ![1, -2]), s(![(1:ℤ), -2], ![2, -2]),
    s(![(-1:ℤ), 1], ![0, 1]), s(![(0:ℤ), 1], ![1, 1]), s(![(1:ℤ), 1], ![2, 1]),
    s(![(-1:ℤ), -2], ![-1, -1]), s(![(-1:ℤ), -1], ![-1, 0]), s(![(-1:ℤ), 0], ![-1, 1]),
    s(![(2:ℤ), -2], ![2, -1]), s(![(2:ℤ), -1], ![2, 0]), s(![(2:ℤ), 0], ![2, 1]) }

Uses 1 · Used by 1

Statement usesSite of the hypercubic lattice

Used byBoundary of a 3 by 3 rectangle as a graph

DefinitionBoundary of a 3 by 3 rectangle as a graph#✓fully proved

The boundary of the rectangle [-1, 2] × [-2, 1] as a graph.

noncomputable def jed_boxH : SimpleGraph (Site 2) :=
  jed_primalGraph (jed_boxEdges : Set (Sym2 (Site 2)))

Uses 3

Statement usesSite of the hypercubic lattice · Twelve boundary edges of a 3 by 3 rectangle · Lattice graph spanned by an edge set

AbbreviationBounded regions of a planar lattice subgraph#✓fully proved

The bounded (finite) connected components of the face-region graph of P.

abbrev jcb_BoundedRegion (P : PlanarZ2Subgraph) : Type :=
  {c : (whb_faceRegion (imageGraph P)).ConnectedComponent // c.supp.Finite}

Uses 4 · Used by 8

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Image of a planar lattice subgraph in the square lattice · Face-region graph of a square-lattice subgraph

Used byBounded regions indexed by the cycle rank · Jordan curve theorem · Cycle rank one gives a unique bounded region · Lattice Jordan curve theorem, even-odd form · Number of cells is at most the nullity of the skeleton · Bounded face formed by a cell · Distinct cells form distinct bounded faces · Hopf's Umlaufsatz

DefinitionBounded regions indexed by the cycle rank#✓fully proved

The bijection between bounded regions of P and Fin (nullity P.G) given by the discrete Jordan–Euler theorem.

noncomputable def jcb_boundedRegionEquiv (P : PlanarZ2Subgraph) :
    jcb_BoundedRegion P ≃ Fin (nullity P.G) :=
  (jed_faithfulDiscreteJordan P).some

Uses 7 · Used by 3

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Image of a planar lattice subgraph in the square lattice · Bounded regions of a planar lattice subgraph · Bounded faces of a finite lattice graph are counted by its cycle rank · Cycle rank of a finite graph · Face-region graph of a square-lattice subgraph

Used byCycle rank one gives a unique bounded region · Number of cells is at most the nullity of the skeleton · Hopf's Umlaufsatz

DefinitionCycle rank one gives a unique bounded region#✓fully proved

A PlanarZ2Subgraph of cycle rank one has exactly one bounded region.

@[reducible] noncomputable def jcb_uniqueBoundedRegion_of_nullity_one (P : PlanarZ2Subgraph)
    (h1 : nullity P.G = 1) : Unique (jcb_BoundedRegion P) := by
  have hcard : Nat.card (jcb_BoundedRegion P) = 1 := by
    rw [jcb_boundedRegion_card_eq_nullity, h1]
  obtain ⟨hsub, hne⟩ := Nat.card_eq_one_iff_unique.mp hcard
  exact ⟨⟨hne.some⟩, fun a => hsub.elim a hne.some⟩

Uses 4 · Used by 3

Statement usesPlanar lattice subgraph of the square lattice · Bounded regions of a planar lattice subgraph · Bounded regions indexed by the cycle rank · Cycle rank of a finite graph

Used byJordan curve theorem · Lattice Jordan curve theorem, even-odd form · Hopf's Umlaufsatz

DefinitionJordan curve theorem#✓fully proved

Jordan curve theorem for lattice cycles: a connected PlanarZ2Subgraph with as many edges as vertices has exactly one bounded region. Reference: C. Jordan, Cours d'analyse (1887); for the discrete form, C. Thomassen, The Jordan–Schönflies theorem and the classification of surfaces (1992).

@[reducible] noncomputable def jcb_uniqueBoundedRegion_of_connected_cycle (P : PlanarZ2Subgraph)
    (hconn : P.G.Connected) (hcard : P.G.edgeSet.ncard = Nat.card P.V) :
    Unique (jcb_BoundedRegion P) :=
  jcb_uniqueBoundedRegion_of_nullity_one P
    (jcb_nullity_eq_one_of_connected_card_eq P.G hconn hcard)

Uses 6

Statement usesPlanar lattice subgraph of the square lattice · Edgeless graph has one component per vertex · Removing one element lowers cardinality by one · Bounded regions of a planar lattice subgraph · Cycle rank one gives a unique bounded region · Cycle rank of a finite graph

DefinitionLattice points around the L-shaped tromino#✓fully proved

The eight lattice points around the L-shaped tromino, in cyclic order.

def jcb_Lemb (i : Fin 8) : Site 2 :=
  match i with
  | 0 => ![0, 0] | 1 => ![1, 0] | 2 => ![2, 0] | 3 => ![2, 1]
  | 4 => ![1, 1] | 5 => ![1, 2] | 6 => ![0, 2] | 7 => ![0, 1]

Uses 1 · Used by 1

Statement usesSite of the hypercubic lattice

Used by8-cycle around the L-tromino as a planar lattice subgraph

DefinitionAdjacency relation of the 8-cycle#✓fully proved

Adjacency of the 8-cycle on Fin 8, as a Boolean relation.

def jcb_LcycRel (i j : Fin 8) : Bool := (i + 1 == j) || (j + 1 == i)

Used by 2

Used byThe 8-cycle graph · 8-cycle around the L-tromino as a planar lattice subgraph

DefinitionThe 8-cycle graph#✓fully proved

The 8-cycle on Fin 8.

def jcb_Lcyc : SimpleGraph (Fin 8) where
  Adj i j := jcb_LcycRel i j
  symm := ⟨by intro i j h; revert h; revert i j; decide⟩
  loopless := ⟨by intro i h; revert h; revert i; decide⟩

Uses 1 · Used by 1

Statement usesAdjacency relation of the 8-cycle

Used by8-cycle around the L-tromino as a planar lattice subgraph

Definition8-cycle around the L-tromino as a planar lattice subgraph#✓fully proved

The 8-cycle around the L-shaped tromino as a PlanarZ2Subgraph.

noncomputable def jcb_LPce : PlanarZ2Subgraph where
  V := Fin 8
  finV := inferInstance
  decV := inferInstance
  G := jcb_Lcyc
  emb := ⟨jcb_Lemb, jcb_Lemb_inj⟩
  isSub := jcb_Lemb_isSub

Uses 6

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · The 8-cycle graph · Adjacency relation of the 8-cycle · Lattice points around the L-shaped tromino

DefinitionTwo diagonally touching sites#✓fully proved

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

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

Uses 1

Statement usesSite of the hypercubic lattice

DefinitionFacial orbit of a boundary dart#✓fully proved

The orbit of a boundary dart of C, as a connected component of the successor graph on boundary darts.

noncomputable def rsf_facialOrbit (C : Set (Site 2)) (e : {d : Dart // IsBoundaryDart C d}) :
    (dartSuccGraph C).ConnectedComponent :=
  (dartSuccGraph C).connectedComponentMk e

Uses 4

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

DefinitionBoundary darts of a component off a closed walk#✓fully proved

The set of boundary darts of a connected component of the sites off the support of Vc.

noncomputable def rsf_componentDarts {a : Site 2} (Vc : (hypercubicLattice 2).Walk a a) :
    (fcb_offComplGraph Vc).ConnectedComponent → Set Dart :=
  ConnectedComponent.lift
    (fun v => {e : Dart | IsBoundaryDart (offSupportComponent Vc (v : Site 2)) e})
    (by
      intro u v p _
      rw [rsf_fcb_reachable_offSupportComponent_eq Vc ⟨p⟩])

Uses 9 · Used by 1

Statement usesDart of the square lattice · Boundary dart of a set of sites · Site of the hypercubic lattice · Lattice off a closed walk · Lattice walk avoiding a set, lifted to the reduced lattice · Square lattice with a set of vertices removed · Hypercubic lattice \(\mathbb{Z}^d\) · Square lattice with a closed walk's vertices removed · Component off a closed walk containing a seed

Used byFacial orbits cover the components of the complement

DefinitionFacial orbits cover the components of the complement#✓fully proved

The boundary dart sets of the components of the complement of Vc are exactly the members of 𝓕.

def rsf_FacialOrbitsCoverComponents {a : Site 2} (Vc : (hypercubicLattice 2).Walk a a)
    (𝓕 : Set (Set Dart)) : Prop :=
  Set.range (rsf_componentDarts Vc) = 𝓕

Uses 5

Statement usesDart of the square lattice · Site of the hypercubic lattice · Lattice off a closed walk · Hypercubic lattice \(\mathbb{Z}^d\) · Boundary darts of a component off a closed walk

DefinitionSeparating side between inside and outside sites#✓fully proved

Some set S contains inside, misses outside, and every lattice edge between sites of D that leaves S has an endpoint in B.

def jcu_HasSeparatingSide (D B inside outside : Set (Site 2)) : Prop :=
  ∃ S : Set (Site 2),
    (∀ z ∈ inside, z ∈ S) ∧
    (∀ z ∈ outside, z ∉ S) ∧
    (∀ u v : Site 2, u ∈ D → v ∈ D → (hypercubicLattice 2).Adj u v →
      u ∈ S → v ∉ S → (u ∈ B ∨ v ∈ B))

Uses 2

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

107 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.