Interior cells by the even-odd rule to Horizontal neighbours of different parity are separated by a vertical step

DefinitionInterior cells by the even-odd rule#✓fully proved

The cells inside the walk by the even-odd rule: those with ray parity 1.

def interiorSet (d : Fin n → Fin 4) : Set (ℤ × ℤ) := {c | rayParity d c.1 c.2 = 1}

Uses 1 · Used by 6

Statement usesRay-crossing parity of a lattice cell

Used byCorner count of the interior counts inside cells around a point · Finite set of interior cells of a closed walk · Finiteness of the interior of a closed walk · Interior of a simple closed walk has no pinch points · Ray-parity interior equals the bounded face · Hopf's Umlaufsatz

DefinitionMinimal height of a walk#✓fully proved

The minimal height of a vertex of the walk.

noncomputable def yInf (d : Fin n → Fin 4) : ℤ :=
  Finset.univ.inf' Finset.univ_nonempty (fun k => (pos d k).2)

Uses 1 · Used by 2

Statement usesVertices of a lattice walk from its step directions

Used byFiniteness of the interior of a closed walk · Cells below a walk are outside

DefinitionMaximal height of a walk#✓fully proved

The maximal height of a vertex of the walk.

noncomputable def ySup (d : Fin n → Fin 4) : ℤ :=
  Finset.univ.sup' Finset.univ_nonempty (fun k => (pos d k).2)

Uses 1 · Used by 1

Statement usesVertices of a lattice walk from its step directions

Used byFiniteness of the interior of a closed walk

TheoremAn inside cell lies below a horizontal step#✓fully proved

An inside cell lies directly below some horizontal step of the walk.

theorem exists_edge_of_rayParity (d : Fin n → Fin 4) (a b : ℤ) (h : rayParity d a b = 1) :
    ∃ k : Fin n, isHorizEdge (d k) ∧ min ((pos d k).1) ((pos d (k + 1)).1) = a ∧
        b < (pos d k).2

Uses 4 · Used by 1

Statement usesVertices of a lattice walk from its step directions · Ray-crossing parity of a lattice cell · Horizontal lattice direction

Proof usesUpward ray crossings above a cell

Used byFiniteness of the interior of a closed walk

TheoremCells below a walk are outside#✓fully proved

Cells below the walk are outside.

theorem rayParity_zero_of_lt_yInf (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (a b : ℤ) (hb : b < yInf d) : rayParity d a b = 0

Uses 8 · Used by 1

Statement usesUnit lattice step in a given direction · Minimal height of a walk · Ray-crossing parity of a lattice cell

Proof usesVertices of a lattice walk from its step directions · Upward ray crossings above a cell · Horizontal lattice direction · Number of crossings of a vertical line · A closed walk crosses each vertical line an even number of times

Used byFiniteness of the interior of a closed walk

TheoremFiniteness of the interior of a closed walk#✓fully proved

A closed walk has finitely many inside cells.

theorem interiorSet_finite (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) :
    (interiorSet d).Finite

Uses 9 · Used by 5

Statement usesUnit lattice step in a given direction · Interior cells by the even-odd rule

Proof usesVertices of a lattice walk from its step directions · An inside cell lies below a horizontal step · Cells below a walk are outside · Minimal height of a walk · Maximal height of a walk · Ray-crossing parity of a lattice cell · Horizontal lattice direction

Used byCorner count of the interior counts inside cells around a point · Finite set of interior cells of a closed walk · Interior of a simple closed walk has no pinch points · Ray-parity interior equals the bounded face · Hopf's Umlaufsatz

DefinitionFinite set of interior cells of a closed walk#✓fully proved

The finite set of cells inside a closed walk (ray parity 1). See also StatMech.Onsager.WalkCellRegion.interiorCells, the bounded face of the walk; the two agree for simple walks without right turns (StatMech.Onsager.UmlaufsatzFinal.interiorCells_bridge).

noncomputable def interiorCells (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) :
    Finset (ℤ × ℤ) := (interiorSet_finite d hclosed).toFinset

Uses 3 · Used by 20

Statement usesUnit lattice step in a given direction · Interior cells by the even-odd rule · Finiteness of the interior of a closed walk

Used byCorner count of the interior counts inside cells around a point · Even corner counts have zero corner weight · Corner weight at a left turn into the east direction · Corner weight at a left turn into the north direction · Corner weight at a left turn into the south direction · Corner weight at a left turn into the west direction · Straight steps of a simple closed walk carry no corner weight · Zero corner weight where the walk continues horizontally · Zero corner weight where the walk continues vertically · Four left turns from a pinch-free interior of Euler characteristic 1 · Corner defect of the interior is the number of left turns up to sign · Corner defect of the interior as a sum over walk vertices · Corner weights at the turns of a walk without right turns · Zero corner weight of the interior off the walk · Pinch count of the ray-parity interior is zero · Interior of a simple closed walk has no pinch points · Face-graph component of an interior cell · Discrete Umlaufsatz for walks of length at least three, shifted form · Ray-parity interior equals the bounded face · Hopf's Umlaufsatz

TheoremCorner count of the interior counts inside cells around a point#✓fully proved

The corner count of the interior at (vx, vy) counts the inside cells among the four cells around that point.

theorem cornerCount_interior_eq (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (vx vy : ℤ) :
    (cornerCount (interiorCells d hclosed) (vx, vy) : ℤ)
      = (if rayParity d vx vy = 1 then (1 : ℤ) else 0)
        + (if rayParity d (vx - 1) vy = 1 then 1 else 0)
        + (if rayParity d vx (vy - 1) = 1 then 1 else 0)
        + (if rayParity d (vx - 1) (vy - 1) = 1 then 1 else 0)

Uses 8 · Used by 8

Statement usesUnit lattice step in a given direction · Corner count of a lattice point · Finite set of interior cells of a closed walk · Ray-crossing parity of a lattice cell

Proof usesCardinality of an intersection as a sum of indicators · Corner count as a count of the four surrounding cells · Interior cells by the even-odd rule · Finiteness of the interior of a closed walk

Used byCorner weight at a left turn into the east direction · Corner weight at a left turn into the north direction · Corner weight at a left turn into the south direction · Corner weight at a left turn into the west direction · Zero corner weight where the walk continues horizontally · Zero corner weight where the walk continues vertically · Zero corner weight of the interior off the walk · Hopf's Umlaufsatz

TheoremRay parity is constant around a non-vertex point#✓fully proved

At a lattice point that is not a vertex of the walk, the four cells around it have the same ray parity.

theorem rayParity_const_of_not_vertex (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (vx vy : ℤ) (hv : ∀ k : Fin n, pos d k ≠ (vx, vy)) :
    rayParity d (vx - 1) vy = rayParity d vx vy
      ∧ rayParity d vx (vy - 1) = rayParity d vx vy
      ∧ rayParity d (vx - 1) (vy - 1) = rayParity d vx vy

Uses 9 · 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

Proof usesRay parity is unchanged across a horizontal move · Ray parity is unchanged across a vertical move · Recursion for the x-coordinate of a walk step · Horizontal lattice direction · Vertical lattice direction · Recursion for the y-coordinate of a walk step

Used byZero corner weight of the interior off the walk · Zero corner weight of the bounded face off the walk

TheoremCorner weight at a left turn into the east direction#✓fully proved

At a left turn made of a south step followed by an east step, the corner weight of the interior is 1 if the cell to the left of the walk is inside and -1 otherwise.

theorem cornerWeight_leftTurn_E (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (pos d)) (hn : 3 ≤ n) (i : Fin n)
    (hei : d i = 3) (he : d (i + 1) = 0) :
    cornerWeight (cornerCount (interiorCells d hclosed) (pos d (i + 1)))
      = if rayParity d (leftCell (d (i + 1)) (pos d (i + 1))).1
              (leftCell (d (i + 1)) (pos d (i + 1))).2 = 1 then (1 : ℤ) else -1

Uses 20 · Used by 2

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 · Finite set of interior cells of a closed walk · Ray-crossing parity of a lattice cell · Unit cell to the left of a lattice step

Proof usesA simple closed walk traverses each horizontal segment at most once · A simple closed walk traverses each vertical segment at most once · Ray parity is unchanged across a vertical move · Forward vertex recursion of a closed lattice walk · An odd number of vertical steps flips the ray parity · Vertical steps separating two horizontal neighbour cells · Horizontal steps on a unit segment · An odd number of horizontal steps flips the ray parity · Corner count of the interior counts inside cells around a point · Recursion for the x-coordinate of a walk step · Horizontal lattice direction · Vertical lattice direction · Recursion for the y-coordinate of a walk step

Used byCorner weights at the turns of a walk without right turns · Hopf's Umlaufsatz

TheoremCorner weight at a left turn into the north direction#✓fully proved

At a left turn made of an east step followed by a north step, the corner weight of the interior is 1 if the cell to the left of the walk is inside and -1 otherwise.

theorem cornerWeight_leftTurn_N (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (pos d)) (hn : 3 ≤ n) (i : Fin n)
    (hei : d i = 0) (he : d (i + 1) = 1) :
    cornerWeight (cornerCount (interiorCells d hclosed) (pos d (i + 1)))
      = if rayParity d (leftCell (d (i + 1)) (pos d (i + 1))).1
              (leftCell (d (i + 1)) (pos d (i + 1))).2 = 1 then (1 : ℤ) else -1

Uses 20 · Used by 2

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 · Finite set of interior cells of a closed walk · Ray-crossing parity of a lattice cell · Unit cell to the left of a lattice step

Proof usesA simple closed walk traverses each horizontal segment at most once · A simple closed walk traverses each vertical segment at most once · Ray parity is unchanged across a vertical move · Forward vertex recursion of a closed lattice walk · An odd number of vertical steps flips the ray parity · Vertical steps separating two horizontal neighbour cells · Horizontal steps on a unit segment · An odd number of horizontal steps flips the ray parity · Corner count of the interior counts inside cells around a point · Recursion for the x-coordinate of a walk step · Horizontal lattice direction · Vertical lattice direction · Recursion for the y-coordinate of a walk step

Used byCorner weights at the turns of a walk without right turns · Hopf's Umlaufsatz

TheoremCorner weight at a left turn into the south direction#✓fully proved

At a left turn made of a west step followed by a south step, the corner weight of the interior is 1 if the cell to the left of the walk is inside and -1 otherwise.

theorem cornerWeight_leftTurn_S (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (pos d)) (hn : 3 ≤ n) (i : Fin n)
    (hei : d i = 2) (he : d (i + 1) = 3) :
    cornerWeight (cornerCount (interiorCells d hclosed) (pos d (i + 1)))
      = if rayParity d (leftCell (d (i + 1)) (pos d (i + 1))).1
              (leftCell (d (i + 1)) (pos d (i + 1))).2 = 1 then (1 : ℤ) else -1

Uses 20 · Used by 2

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 · Finite set of interior cells of a closed walk · Ray-crossing parity of a lattice cell · Unit cell to the left of a lattice step

Proof usesA simple closed walk traverses each horizontal segment at most once · A simple closed walk traverses each vertical segment at most once · Ray parity is unchanged across a horizontal move · Forward vertex recursion of a closed lattice walk · An odd number of vertical steps flips the ray parity · Vertical steps separating two horizontal neighbour cells · Horizontal steps on a unit segment · An odd number of horizontal steps flips the ray parity · Corner count of the interior counts inside cells around a point · Recursion for the x-coordinate of a walk step · Horizontal lattice direction · Vertical lattice direction · Recursion for the y-coordinate of a walk step

Used byCorner weights at the turns of a walk without right turns · Hopf's Umlaufsatz

TheoremCorner weight at a left turn into the west direction#✓fully proved

At a left turn made of a north step followed by a west step, the corner weight of the interior is 1 if the cell to the left of the walk is inside and -1 otherwise.

theorem cornerWeight_leftTurn_W (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (pos d)) (hn : 3 ≤ n) (i : Fin n)
    (hei : d i = 1) (he : d (i + 1) = 2) :
    cornerWeight (cornerCount (interiorCells d hclosed) (pos d (i + 1)))
      = if rayParity d (leftCell (d (i + 1)) (pos d (i + 1))).1
              (leftCell (d (i + 1)) (pos d (i + 1))).2 = 1 then (1 : ℤ) else -1

Uses 18 · Used by 2

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 · Finite set of interior cells of a closed walk · Ray-crossing parity of a lattice cell · Unit cell to the left of a lattice step

Proof usesA simple closed walk traverses each vertical segment at most once · Ray parity is unchanged across a horizontal move · Ray parity is unchanged across a vertical move · Forward vertex recursion of a closed lattice walk · An odd number of vertical steps flips the ray parity · Vertical steps separating two horizontal neighbour cells · Corner count of the interior counts inside cells around a point · Recursion for the x-coordinate of a walk step · Horizontal lattice direction · Vertical lattice direction · Recursion for the y-coordinate of a walk step

Used byCorner weights at the turns of a walk without right turns · Hopf's Umlaufsatz

TheoremA horizontal direction is not vertical#✓fully proved

A horizontal direction is not vertical.

theorem not_isVert_of_isHoriz {w : Fin 4} (h : isHorizEdge w) : ¬ isVertEdge w

Uses 2 · Used by 2

Statement usesHorizontal lattice direction · Vertical lattice direction

Used byZero corner weight where the walk continues horizontally · Interior of a simple closed walk has no pinch points

TheoremA vertical direction is not horizontal#✓fully proved

A vertical direction is not horizontal.

theorem not_isHoriz_of_isVert {w : Fin 4} (h : isVertEdge w) : ¬ isHorizEdge w

Uses 2 · Used by 1

Statement usesHorizontal lattice direction · Vertical lattice direction

Used byZero corner weight where the walk continues vertically

TheoremEven corner counts have zero corner weight#✓fully proved

An even corner count has weight 0.

theorem cornerWeight_eq_zero_of_two_dvd
    (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) (v : ℤ × ℤ)
    (hdvd : 2 ∣ cornerCount (interiorCells d hclosed) v) :
    cornerWeight (cornerCount (interiorCells d hclosed) v) = 0

Uses 4 · Used by 2

Statement usesUnit lattice step in a given direction · Corner count of a lattice point · Corner weight of a vertex · Finite set of interior cells of a closed walk

Used byZero corner weight where the walk continues horizontally · Zero corner weight where the walk continues vertically

TheoremZero corner weight where the walk continues horizontally#✓fully proved

A vertex where the walk continues horizontally has weight 0.

theorem cornerWeight_straight_horiz (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (pos d)) (i : Fin n)
    (hstraight : d (i + 1) = d i) (hh : isHorizEdge (d i)) :
    cornerWeight (cornerCount (interiorCells d hclosed) (pos d (i + 1))) = 0

Uses 14 · 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 · Finite set of interior cells of a closed walk · Horizontal lattice direction

Proof usesRay-crossing parity of a lattice cell · Ray parity is unchanged across a horizontal move · Even corner counts have zero corner weight · A horizontal direction is not vertical · Corner count of the interior counts inside cells around a point · Recursion for the x-coordinate of a walk step · Vertical lattice direction · Recursion for the y-coordinate of a walk step

Used byStraight steps of a simple closed walk carry no corner weight

TheoremZero corner weight where the walk continues vertically#✓fully proved

A vertex where the walk continues vertically has weight 0.

theorem cornerWeight_straight_vert (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (pos d)) (i : Fin n)
    (hstraight : d (i + 1) = d i) (hv : isVertEdge (d i)) :
    cornerWeight (cornerCount (interiorCells d hclosed) (pos d (i + 1))) = 0

Uses 14 · 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 · Finite set of interior cells of a closed walk · Vertical lattice direction

Proof usesRay-crossing parity of a lattice cell · Ray parity is unchanged across a vertical move · Even corner counts have zero corner weight · A vertical direction is not horizontal · Corner count of the interior counts inside cells around a point · Recursion for the x-coordinate of a walk step · Horizontal lattice direction · Recursion for the y-coordinate of a walk step

Used byStraight steps of a simple closed walk carry no corner weight

TheoremStraight steps of a simple closed walk carry no corner weight#✓fully proved

A vertex where a simple closed walk goes straight has corner weight 0 for the interior.

theorem cornerWeight_straight (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (pos d)) (i : Fin n) (hstraight : d (i + 1) = d i) :
    cornerWeight (cornerCount (interiorCells d hclosed) (pos d (i + 1))) = 0

Uses 10 · Used by 2

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 · Finite set of interior cells of a closed walk

Proof usesCoordinates of the four lattice steps · Zero corner weight where the walk continues horizontally · Zero corner weight where the walk continues vertically · Horizontal lattice direction · Vertical lattice direction

Used byCorner weights at the turns of a walk without right turns · Hopf's Umlaufsatz

TheoremHorizontal neighbours of different parity are separated by a vertical step#✓fully proved

If cells (a, b) and (a + 1, b) have different ray parities, a vertical step separates them.

theorem straddle_nonempty_of_ne (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) (a b : ℤ)
    (h : rayParity d a b ≠ rayParity d (a + 1) b) : (straddleSet d a b).Nonempty

Uses 6 · Used by 1

Statement usesUnit lattice step in a given direction · Ray-crossing parity of a lattice cell · Vertical steps separating two horizontal neighbour cells

Proof usesVertices of a lattice walk from its step directions · Ray parity is unchanged across a horizontal move · Vertical lattice direction

Used byInterior of a simple closed walk has no pinch points

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.