Lattice Jordan curve theorem, even-odd form to Zero corner weight of the bounded face off the walk

TheoremLattice Jordan curve theorem, even-odd form#✓fully proved

Lattice Jordan curve theorem, even-odd form: a cell lies in the bounded face of a simple closed walk without right turns iff its ray parity is 1.

theorem mem_interiorCells_iff_rayParity (p : ℤ × ℤ) :
    p ∈ interiorCells d hclosed hsimple hreflexfree ↔ rayParity d p.1 p.2 = 1

Uses 30 · Used by 4

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Ray-crossing parity of a lattice cell · Cells of the bounded face of a simple closed walk

Proof 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\) · Every finite set of sites lies in a box · Hypercubic lattice \(\mathbb{Z}^d\) · Image of a planar lattice subgraph in the square lattice · Bounded regions of a planar lattice subgraph · Cycle rank one gives a unique bounded region · Outer face region of a planar lattice subgraph · Radius of a box containing a planar lattice subgraph · Setting a set of coordinates of a lattice site · Primal edge shared by adjacent faces · Face-region graph of a square-lattice subgraph · Subgraph of a simple closed lattice walk has cycle rank one · Unit cell as a face of the square lattice · Inner component of the face graph · The inner face component is finite · Face below-left of the inside top corner · The face below the inside top corner is inside · Membership in the bounded face · A face far outside the walk has ray parity zero · Ray parity is constant on face-graph components · Simple closed walk as a planar subgraph · Face graph of a closed walk

Used byZero corner weight of the bounded face off the walk · Every left cell lies in the bounded face · A side between interior and exterior cells is a walk edge · Ray-parity interior equals the bounded face

DefinitionFace-graph component of an interior cell#✓fully proved

The connected component of the walk's face graph containing an interior cell.

noncomputable def oddComponent (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d))
    (c : interiorCells d hclosed) :
    (walkRegionGraph d hclosed hsimple).ConnectedComponent :=
  (walkRegionGraph d hclosed hsimple).connectedComponentMk (cellFace c.1)

Uses 6 · Used by 1

Statement usesSite of the hypercubic lattice · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · Finite set of interior cells of a closed walk · Unit cell as a face of the square lattice · Face graph of a closed walk

Used byHopf's Umlaufsatz

TheoremA side between interior and exterior cells is a walk edge#✓fully proved

A side shared by an interior and an exterior cell is an edge of the walk.

theorem sharedPrimalEdge_mem_of_membership_diff (p q : ℤ × ℤ)
    (hlat : (hypercubicLattice 2).Adj (cellFace p) (cellFace q))
    (hdiff : (p ∈ S ∧ q ∉ S) ∨ (q ∈ S ∧ p ∉ S)) :
    sharedPrimalEdge (cellFace p) (cellFace q) ∈ (imageGraph P).edgeSet

Uses 13 · Used by 1

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Image of a planar lattice subgraph in the square lattice · Primal edge shared by adjacent faces · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · Unit cell as a face of the square lattice · Cells of the bounded face of a simple closed walk · Simple closed walk as a planar subgraph

Proof usesRay-crossing parity of a lattice cell · Lattice Jordan curve theorem, even-odd form · Face-adjacent cells have the same ray parity · Face graph of a closed walk

Used byBounded face of a simple closed walk has no pinch points

TheoremThree walk edges cannot meet at a vertex#✓fully proved

Three walk edges cannot meet at one vertex of a simple closed walk.

theorem pinch_four_edges_impossible (x y : ℤ)
    (hU : sharedPrimalEdge (cellFace (x, y)) (cellFace (x - 1, y)) ∈
      (imageGraph P).edgeSet)
    (hR : sharedPrimalEdge (cellFace (x, y)) (cellFace (x, y - 1)) ∈
      (imageGraph P).edgeSet)
    (hL : sharedPrimalEdge (cellFace (x - 1, y)) (cellFace (x - 1, y - 1)) ∈
      (imageGraph P).edgeSet) : False

Uses 13 · Used by 1

Statement usesSite of the hypercubic lattice · Image of a planar lattice subgraph in the square lattice · Primal edge shared by adjacent faces · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · Unit cell as a face of the square lattice · Simple closed walk as a planar subgraph

Proof usesPlanar lattice subgraph of the square lattice · 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)\) · Vertex of a walk as a lattice site · Neighbours in the image graph are walk predecessor and successor

Used byBounded face of a simple closed walk has no pinch points

TheoremBounded face of a simple closed walk has no pinch points#✓fully proved

The bounded face of the walk has no pinch points.

theorem not_pinchAt_interiorCells (v : ℤ × ℤ) : ¬ pinchAt S v

Uses 12 · Used by 2

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Pinch point of a set of unit cells · Cells of the bounded face of a simple closed walk

Proof usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Image of a planar lattice subgraph in the square lattice · Primal edge shared by adjacent faces · Three walk edges cannot meet at a vertex · A side between interior and exterior cells is a walk edge · Unit cell as a face of the square lattice · Simple closed walk as a planar subgraph

Used byCorner count of the bounded face at a walk vertex · Pinch count of the bounded face is zero

TheoremPinch count of the bounded face is zero#✓fully proved

The bounded face of the walk has pinch count 0. See also StatMech.Onsager.PinchFree.pinchCount_eq_zero.

theorem pinchCount_interiorCells_eq_zero : pinchCount S = 0

Uses 8

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Number of pinch points · Cells of the bounded face of a simple closed walk

Proof usesVertices of a cell complex · Pinch point of a set of unit cells · Pinch point indicator · Bounded face of a simple closed walk has no pinch points

DefinitionCell to the left of a walk step#✓fully proved

The cell to the left of step k of the walk. See also StatMech.Onsager.Orientation.leftCell; they agree by StatMech.Onsager.UmlaufsatzFinal.leftCell_bridge.

def leftCell (d : Fin (m + 3) → Fin 4) (k : Fin (m + 3)) : ℤ × ℤ :=
  match d k with
  | 0 => ((pos d k).1, (pos d k).2)
  | 1 => ((pos d k).1 - 1, (pos d k).2)
  | 2 => ((pos d k).1 - 1, (pos d k).2 - 1)
  | 3 => ((pos d k).1, (pos d k).2 - 1)

Uses 1 · Used by 11

Statement usesVertices of a lattice walk from its step directions

Used byCorner count of the bounded face at a walk vertex · Consecutive left cells on a straight step are face-adjacent · Every left cell lies in the bounded face · All left cells have the same ray parity · Every left cell has ray parity one · Consecutive left cells have the same ray parity · Left and right cells of a step share that step · No right cell lies in the bounded face · Connectedness of the skeleton of the interior · Agreement of the two definitions of the left cell · A walk without right turns is positively oriented

DefinitionCell to the right of a walk step#✓fully proved

The cell to the right of step k of the walk.

def rightCell (d : Fin (m + 3) → Fin 4) (k : Fin (m + 3)) : ℤ × ℤ :=
  match d k with
  | 0 => ((pos d k).1, (pos d k).2 - 1)
  | 1 => ((pos d k).1, (pos d k).2)
  | 2 => ((pos d k).1 - 1, (pos d k).2)
  | 3 => ((pos d k).1 - 1, (pos d k).2 - 1)

Uses 1 · Used by 3

Statement usesVertices of a lattice walk from its step directions

Used byCorner count of the bounded face at a walk vertex · Left and right cells of a step share that step · No right cell lies in the bounded face

TheoremVertices of a walk's image graph are adjacent only to walk neighbours#✓fully proved

In the image graph of a simple closed walk, a vertex is adjacent only to its walk neighbours.

theorem imageGraph_not_adj_of_neighbours (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d))
    (k : Fin (m + 3)) (q : Site 2)
    (hpred : q ≠ posSite d (k - 1)) (hsucc : q ≠ posSite d (k + 1)) :
    ¬ (imageGraph (walkP d hclosed hsimple)).Adj (posSite d k) q

Uses 7

Statement usesSite of the hypercubic lattice · Image of a planar lattice subgraph in the square lattice · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · Vertex of a walk as a lattice site · Simple closed walk as a planar subgraph

Proof usesNeighbours in the image graph are walk predecessor and successor

TheoremConsecutive left cells on a straight step are face-adjacent#✓fully proved

Going straight, consecutive left cells are adjacent in the face graph of the walk.

theorem leftCell_faceAdj_of_straight (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d))
    (k : Fin (m + 3)) (hstraight : d (k + 1) = d k) :
    (walkRegionGraph d hclosed hsimple).Adj (cellFace (leftCell d k))
      (cellFace (leftCell d (k + 1)))

Uses 18 · Used by 1

Statement usesSite of the hypercubic lattice · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · Cell to the left of a walk step · Unit cell as a face of the square lattice · Face graph of a closed walk

Proof usesPlanar lattice subgraph of the square lattice · 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)\) · Hypercubic lattice \(\mathbb{Z}^d\) · Image of a planar lattice subgraph in the square lattice · Primal edge shared by adjacent faces · Vertex of a walk as a lattice site · Forward vertex recursion of a closed lattice walk · Neighbours in the image graph are walk predecessor and successor · Simple closed walk as a planar subgraph

Used byConsecutive left cells have the same ray parity

TheoremConsecutive left cells have the same ray parity#✓fully proved

Consecutive left cells of a simple closed walk without right turns have the same ray parity.

theorem leftCell_parity_succ (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d))
    (hreflexfree : ∀ i : Fin (m + 3), d (i + 1) - d i = 0 ∨ d (i + 1) - d i = 1)
    (k : Fin (m + 3)) :
    rayParity d (leftCell d k).1 (leftCell d k).2 =
      rayParity d (leftCell d (k + 1)).1 (leftCell d (k + 1)).2

Uses 10 · Used by 1

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Ray-crossing parity of a lattice cell · Cell to the left of a walk step

Proof usesSite of the hypercubic lattice · Forward vertex recursion of a closed lattice walk · Consecutive left cells on a straight step are face-adjacent · Unit cell as a face of the square lattice · Face-adjacent cells have the same ray parity · Face graph of a closed walk

Used byAll left cells have the same ray parity

TheoremAll left cells have the same ray parity#✓fully proved

All left cells of a simple closed walk without right turns have the same ray parity.

theorem leftCell_parity_eq_of_reachable (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d))
    (hreflexfree : ∀ i : Fin (m + 3), d (i + 1) - d i = 0 ∨ d (i + 1) - d i = 1)
    {i j : Fin (m + 3)} (hreach : (cycleGraph (m + 3)).Reachable i j) :
    rayParity d (leftCell d i).1 (leftCell d i).2 =
      rayParity d (leftCell d j).1 (leftCell d j).2

Uses 5 · Used by 1

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Ray-crossing parity of a lattice cell · Cell to the left of a walk step

Proof usesConsecutive left cells have the same ray parity

Used byEvery left cell has ray parity one

TheoremEvery left cell has ray parity one#✓fully proved

Every left cell of a simple closed walk without right turns is inside.

theorem leftCell_parity_one (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d))
    (hreflexfree : ∀ i : Fin (m + 3), d (i + 1) - d i = 0 ∨ d (i + 1) - d i = 1)
    (k : Fin (m + 3)) :
    rayParity d (leftCell d k).1 (leftCell d k).2 = 1

Uses 8 · Used by 2

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Ray-crossing parity of a lattice cell · Cell to the left of a walk step

Proof usesBackward vertex recursion of a closed lattice walk · All left cells have the same ray parity · Top corner with an inside cell below it · Defining property of the inside top corner

Used byEvery left cell lies in the bounded face · A walk without right turns is positively oriented

TheoremEvery left cell lies in the bounded face#✓fully proved

Every left cell of a simple closed walk without right turns lies in the bounded face.

theorem leftCell_mem_interiorCells (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d))
    (hreflexfree : ∀ i : Fin (m + 3), d (i + 1) - d i = 0 ∨ d (i + 1) - d i = 1)
    (k : Fin (m + 3)) :
    leftCell d k ∈ interiorCells d hclosed hsimple hreflexfree

Uses 7 · Used by 3

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Cell to the left of a walk step · Cells of the bounded face of a simple closed walk

Proof usesRay-crossing parity of a lattice cell · Every left cell has ray parity one · Lattice Jordan curve theorem, even-odd form

Used byCorner count of the bounded face at a walk vertex · No right cell lies in the bounded face · Connectedness of the skeleton of the interior

TheoremCells on either side of a step lie in different faces#✓fully proved

The two cells on either side of a walk step are in different face components.

theorem walkRegion_flanking_not_reachable (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d))
    (k : Fin (m + 3)) {f g : Site 2}
    (hlat : (hypercubicLattice 2).Adj f g)
    (hshared : sharedPrimalEdge f g = s(posSite d k, posSite d (k + 1))) :
    ¬ (walkRegionGraph d hclosed hsimple).Reachable f g

Uses 36 · Used by 1

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Primal edge shared by adjacent faces · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · Vertex of a walk as a lattice site · Face graph of a closed walk

Proof usesPlanar lattice subgraph of the square lattice · 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)\) · 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 · Pushforward of a subgraph into the square lattice · Pushed-forward subgraphs are locally finite · Closed face walk around a lattice vertex · 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 · Primal edge between two faces lies in a subgraph · Each walk step is an edge of the image graph · Simple closed walk as a planar subgraph

Used byNo right cell lies in the bounded face

TheoremLeft and right cells of a step share that step#✓fully proved

The left and right cells of a step are adjacent faces sharing that step.

theorem left_right_flanking (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (k : Fin (m + 3)) :
    (hypercubicLattice 2).Adj (cellFace (leftCell d k)) (cellFace (rightCell d k)) ∧
      sharedPrimalEdge (cellFace (leftCell d k)) (cellFace (rightCell d k)) =
        s(posSite d k, posSite d (k + 1))

Uses 14 · Used by 1

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Primal edge shared by adjacent faces · Unit lattice step in a given direction · Vertex of a walk as a lattice site · Cell to the left of a walk step · Cell to the right of a walk step · Unit cell as a face of the square lattice

Proof usesLower 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)\) · Vertices of a lattice walk from its step directions · Forward vertex recursion of a closed lattice walk

Used byNo right cell lies in the bounded face

TheoremNo right cell lies in the bounded face#✓fully proved

No right cell of a simple closed walk without right turns lies in the bounded face.

theorem rightCell_not_mem_interiorCells (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d))
    (hreflexfree : ∀ i : Fin (m + 3), d (i + 1) - d i = 0 ∨ d (i + 1) - d i = 1)
    (k : Fin (m + 3)) :
    rightCell d k ∉ interiorCells d hclosed hsimple hreflexfree

Uses 16 · Used by 1

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Cell to the right of a walk step · Cells of the bounded face of a simple closed walk

Proof usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Primal edge shared by adjacent faces · Vertex of a walk as a lattice site · Cell to the left of a walk step · Every left cell lies in the bounded face · Left and right cells of a step share that step · Cells on either side of a step lie in different faces · Unit cell as a face of the square lattice · Inner component of the face graph · Membership in the bounded face · Face graph of a closed walk

Used byCorner count of the bounded face at a walk vertex

TheoremCorner count as a sum of four indicators#✓fully proved

The corner count at v as a sum of four indicators. See also StatMech.Onsager.CellEuler.cornerCount_eq_inter.

theorem cornerCount_eq_indicators (S : Finset (ℤ × ℤ)) (v : ℤ × ℤ) :
    cornerCount S v =
      (if v ∈ S then 1 else 0) +
      (if (v.1 - 1, v.2) ∈ S then 1 else 0) +
      (if (v.1, v.2 - 1) ∈ S then 1 else 0) +
      (if (v.1 - 1, v.2 - 1) ∈ S then 1 else 0)

Uses 3 · Used by 2

Statement usesCorner count of a lattice point

Proof usesCardinality of an intersection as a sum of indicators · Corner count as a count of the four surrounding cells

Used byCorner count of the bounded face at a walk vertex · Zero corner weight of the bounded face off the walk

TheoremCorner count of the bounded face at a walk vertex#✓fully proved

At the vertex after step k, the bounded face has one cell after a left turn and two after a straight step.

theorem cornerCount_at_walkVertex (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d))
    (hreflexfree : ∀ i : Fin (m + 3), d (i + 1) - d i = 0 ∨ d (i + 1) - d i = 1)
    (k : Fin (m + 3)) :
    cornerCount (interiorCells d hclosed hsimple hreflexfree) (pos d (k + 1)) =
      if d (k + 1) - d k = 1 then 1 else 2

Uses 12 · Used by 1

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Corner count of a lattice point · Cells of the bounded face of a simple closed walk

Proof usesPinch point of a set of unit cells · Forward vertex recursion of a closed lattice walk · Corner count as a sum of four indicators · Cell to the left of a walk step · Every left cell lies in the bounded face · Cell to the right of a walk step · No right cell lies in the bounded face · Bounded face of a simple closed walk has no pinch points

Used byCorner weight of the bounded face at a walk vertex

TheoremZero corner weight of the bounded face off the walk#✓fully proved

Points off the walk have corner weight 0 for the bounded face.

theorem cornerWeight_zero_of_not_walkVertex (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d))
    (hreflexfree : ∀ i : Fin (m + 3), d (i + 1) - d i = 0 ∨ d (i + 1) - d i = 1)
    (v : ℤ × ℤ) (hv : ∀ k : Fin (m + 3), pos d k ≠ v) :
    cornerWeight (cornerCount (interiorCells d hclosed hsimple hreflexfree) v) = 0

Uses 9 · Used by 1

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Corner count of a lattice point · Corner weight of a vertex · Cells of the bounded face of a simple closed walk

Proof usesRay-crossing parity of a lattice cell · Corner count as a sum of four indicators · Ray parity is constant around a non-vertex point · Lattice Jordan curve theorem, even-odd form

Used byCorner defect of the bounded face equals the number of left turns

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.