Unit cell to the left of a lattice step to \(k + 2 \ne k\) in \(\mathrm{Fin}\, n\) for \(n \ge 3\)

DefinitionUnit cell to the left of a lattice step#✓fully proved

The unit cell to the left of the step in direction w starting at p (cells are named by their lower-left corners).

def leftCell : Fin 4 → ℤ × ℤ → ℤ × ℤ
  | 0, p => p
  | 1, p => (p.1 - 1, p.2)
  | 2, p => (p.1 - 1, p.2 - 1)
  | 3, p => (p.1, p.2 - 1)

Used by 12

Used bySteps around a left turn share their left cell · Left cells keep their ray parity on a straight step · Ray parity of the cell left of a step · Consecutive steps have the same left parity · 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 · Corner weights at the turns of a walk without right turns · Agreement of the two definitions of the left cell · A walk without right turns is positively oriented · Hopf's Umlaufsatz

TheoremSteps around a left turn share their left cell#✓fully proved

At a left turn, the steps before and after the turn have the same left cell.

theorem leftCell_eq_of_leftTurn (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) (k : Fin n)
    (hturn : d (k + 1) - d k = 1) :
    leftCell (d k) (pos d k) = leftCell (d (k + 1)) (pos d (k + 1))

Uses 4 · Used by 2

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Unit cell to the left of a lattice step

Proof usesForward vertex recursion of a closed lattice walk

Used byConsecutive steps have the same left parity · Hopf's Umlaufsatz

TheoremNo vertical step through a non-vertex point#✓fully proved

A vertical step through the point (c, h) has (c, h) as a vertex; if (c, h) is not a walk vertex, no vertical step straddles height h on the line x = c.

theorem no_vEdge_of_not_vertex (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (c h : ℤ) (hnv : ∀ k : Fin n, pos d k ≠ (c, h)) :
    ∀ k : Fin n, isVertEdge (d k) → (pos d k).1 = c →
      ¬ (min ((pos d k).2) ((pos d (k + 1)).2) ≤ h ∧
          h < max ((pos d k).2) ((pos d (k + 1)).2))

Uses 5

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Vertical lattice direction

Proof usesRecursion for the x-coordinate of a walk step · Recursion for the y-coordinate of a walk step

TheoremNo horizontal step starts at a non-vertex point#✓fully proved

If (c, h) is not a walk vertex, no horizontal step starts at x = c on height h.

theorem no_hEdge_of_not_vertex (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (c h : ℤ) (hnv : ∀ k : Fin n, pos d k ≠ (c, h)) :
    ∀ k : Fin n, isHorizEdge (d k) → min ((pos d k).1) ((pos d (k + 1)).1) = c →
      (pos d k).2 ≠ h

Uses 5

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Horizontal lattice direction

Proof usesRecursion for the x-coordinate of a walk step · Recursion for the y-coordinate of a walk step

TheoremIndex of a vertical step above a walk vertex#✓fully proved

In a simple walk, a vertical step on the segment above the vertex pos d m is step m or step m - 1.

theorem vEdge_lower_index (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (pos d)) (c h : ℤ) (m : Fin n) (hpm : pos d m = (c, h))
    (j : Fin n) (hvj : isVertEdge (d j)) (hxj : (pos d j).1 = c)
    (hstraddle : min ((pos d j).2) ((pos d (j + 1)).2) ≤ h ∧
      h < max ((pos d j).2) ((pos d (j + 1)).2)) :
    j = m ∨ j + 1 = m

Uses 5 · Used by 1

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Vertical lattice direction

Proof usesRecursion for the x-coordinate of a walk step · Recursion for the y-coordinate of a walk step

Used byLeft cells keep their ray parity on a straight step

TheoremIndex of a horizontal step right of a walk vertex#✓fully proved

In a simple walk, a horizontal step on the segment to the right of the vertex pos d m is step m or step m - 1.

theorem hEdge_left_index (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (pos d)) (c h : ℤ) (m : Fin n) (hpm : pos d m = (c, h))
    (j : Fin n) (hhj : isHorizEdge (d j)) (hxj : min ((pos d j).1) ((pos d (j + 1)).1) = c)
    (hyj : (pos d j).2 = h) :
    j = m ∨ j + 1 = m

Uses 5 · Used by 1

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Horizontal lattice direction

Proof usesRecursion for the x-coordinate of a walk step · Recursion for the y-coordinate of a walk step

Used byLeft cells keep their ray parity on a straight step

TheoremIndex of a vertical step below a walk vertex#✓fully proved

In a simple walk, a vertical step on the segment below the vertex pos d m is step m or step m - 1.

theorem vEdge_upper_index (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (pos d)) (c h : ℤ) (m : Fin n) (hpm : pos d m = (c, h + 1))
    (j : Fin n) (hvj : isVertEdge (d j)) (hxj : (pos d j).1 = c)
    (hstraddle : min ((pos d j).2) ((pos d (j + 1)).2) ≤ h ∧
      h < max ((pos d j).2) ((pos d (j + 1)).2)) :
    j = m ∨ j + 1 = m

Uses 5 · Used by 1

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Vertical lattice direction

Proof usesRecursion for the x-coordinate of a walk step · Recursion for the y-coordinate of a walk step

Used byLeft cells keep their ray parity on a straight step

TheoremIndex of a horizontal step left of a walk vertex#✓fully proved

In a simple walk, a horizontal step on the segment to the left of the vertex pos d m is step m or step m - 1.

theorem hEdge_right_index (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (pos d)) (c h : ℤ) (m : Fin n) (hpm : pos d m = (c + 1, h))
    (j : Fin n) (hhj : isHorizEdge (d j)) (hxj : min ((pos d j).1) ((pos d (j + 1)).1) = c)
    (hyj : (pos d j).2 = h) :
    j = m ∨ j + 1 = m

Uses 5 · Used by 1

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Horizontal lattice direction

Proof usesRecursion for the x-coordinate of a walk step · Recursion for the y-coordinate of a walk step

Used byLeft cells keep their ray parity on a straight step

TheoremLeft cells keep their ray parity on a straight step#✓fully proved

Going straight, consecutive left cells have the same ray parity.

theorem leftCell_parity_eq_of_straight (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (pos d)) (k : Fin n) (hst : d (k + 1) = d k) :
    rayParity d (leftCell (d k) (pos d k)).1 (leftCell (d k) (pos d k)).2
      = rayParity d (leftCell (d (k + 1)) (pos d (k + 1))).1
          (leftCell (d (k + 1)) (pos d (k + 1))).2

Uses 13 · 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 · Unit cell to the left of a lattice step

Proof usesRay parity is unchanged across a horizontal move · Ray parity is unchanged across a vertical move · Forward vertex recursion of a closed lattice walk · Index of a horizontal step right of a walk vertex · Index of a horizontal step left of a walk vertex · Index of a vertical step above a walk vertex · Index of a vertical step below a walk vertex · Horizontal lattice direction · Vertical lattice direction

Used byConsecutive steps have the same left parity · Hopf's Umlaufsatz

DefinitionRay parity of the cell left of a step#✓fully proved

The ray parity of the cell to the left of step k.

def leftParity (d : Fin n → Fin 4) (k : Fin n) : ZMod 2 :=
  rayParity d (leftCell (d k) (pos d k)).1 (leftCell (d k) (pos d k)).2

Uses 3 · Used by 8

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

Used byLeft parity is constant along a walk without right turns · Consecutive steps have the same left parity · 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 weights at the turns of a walk without right turns · Discrete Umlaufsatz for walks of length at least three, shifted form · A walk without right turns is positively oriented · Hopf's Umlaufsatz

TheoremConsecutive steps have the same left parity#✓fully proved

For a simple closed walk without right turns, consecutive steps have the same left parity.

theorem leftParity_step (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (pos d))
    (hreflexfree : ∀ i : Fin n, d (i + 1) - d i = 0 ∨ d (i + 1) - d i = 1) (k : Fin n) :
    leftParity d k = leftParity d (k + 1)

Uses 7 · Used by 1

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

Proof usesRay-crossing parity of a lattice cell · Unit cell to the left of a lattice step · Steps around a left turn share their left cell · Left cells keep their ray parity on a straight step

Used byLeft parity is constant along a walk without right turns

TheoremLeft parity is constant along a walk without right turns#✓fully proved

For a simple closed walk without right turns, the left parity is the same for every step.

theorem leftParity_const (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (pos d))
    (hreflexfree : ∀ i : Fin n, d (i + 1) - d i = 0 ∨ d (i + 1) - d i = 1) (k : Fin n) :
    leftParity d k = leftParity d 0

Uses 4 · Used by 1

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

Proof usesConsecutive steps have the same left parity

Used byCorner weights at the turns of a walk without right turns

DefinitionVertical steps separating two horizontal neighbour cells#✓fully proved

The vertical steps of the walk on the segment {a + 1} × [b, b + 1] separating the cells (a, b) and (a + 1, b).

def straddleSet (d : Fin n → Fin 4) (a b : ℤ) : Finset (Fin n) :=
  Finset.univ.filter (fun k : Fin n =>
    isVertEdge (d k) ∧ (pos d k).1 = a + 1 ∧
      min ((pos d k).2) ((pos d (k + 1)).2) ≤ b ∧ b < max ((pos d k).2) ((pos d (k + 1)).2))

Uses 2 · Used by 12

Statement usesVertices of a lattice walk from its step directions · Vertical lattice direction

Used byAn odd number of vertical steps flips the ray parity · Ray parity across a vertical segment counts separating steps · Parity of upward crossings across a vertical segment · A simple closed walk traverses each vertical segment at most once · Steps on a vertical unit segment join its endpoints · 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 · Horizontal neighbours of different parity are separated by a vertical step · Interior of a simple closed walk has no pinch points · Hopf's Umlaufsatz

TheoremParity of upward crossings across a vertical segment#✓fully proved

The upward crossing counts of cells (a, b) and (a + 1, b) plus the number of steps between them is even.

theorem upCross_hstep_gen (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) (a b : ℤ) :
    upCross d a b + upCross d (a + 1) b + (straddleSet d a b).card
      = 2 * (Finset.univ.filter (fun k : Fin n =>
          ¬ ((pos d k).1 = a + 1 ∧ b + 1 ≤ (pos d k).2) ∧
            ((pos d (k + 1)).1 = a + 1 ∧ b + 1 ≤ (pos d (k + 1)).2))).card

Uses 9 · Used by 1

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Upward ray crossings above a cell · Vertical steps separating two horizontal neighbour cells

Proof usesCoordinates of the four lattice steps · 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 byRay parity across a vertical segment counts separating steps

TheoremRay parity across a vertical segment counts separating steps#✓fully proved

The ray parities of cells (a, b) and (a + 1, b) add up to the number of separating vertical steps mod 2.

theorem rayParity_hstep_gen (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) (a b : ℤ) :
    rayParity d a b + rayParity d (a + 1) b = ((straddleSet d a b).card : ZMod 2)

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 · Upward ray crossings above a cell · Parity of upward crossings across a vertical segment

Used byAn odd number of vertical steps flips the ray parity

TheoremAn odd number of vertical steps flips the ray parity#✓fully proved

An odd number of vertical steps between cells (a, b) and (a + 1, b) flips the ray parity.

theorem rayParity_hflip (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) (a b : ℤ)
    (hodd : (straddleSet d a b).card % 2 = 1) :
    rayParity d a b = rayParity d (a + 1) b + 1

Uses 4 · Used by 5

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

Proof usesRay parity across a vertical segment counts separating steps

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 · Hopf's Umlaufsatz

DefinitionHorizontal steps on a unit segment#✓fully proved

The horizontal steps of the walk on the segment [a, a + 1] × {b}.

def midSet (d : Fin n → Fin 4) (a b : ℤ) : Finset (Fin n) :=
  Finset.univ.filter (fun k : Fin n =>
    isHorizEdge (d k) ∧ min ((pos d k).1) ((pos d (k + 1)).1) = a ∧ (pos d k).2 = b)

Uses 2 · Used by 10

Statement usesVertices of a lattice walk from its step directions · Horizontal lattice direction

Used byAn odd number of horizontal steps flips the ray parity · Upward crossings of vertically adjacent cells differ by separating steps · A simple closed walk traverses each horizontal segment at most once · Steps on a horizontal unit segment join its endpoints · 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 · Vertical neighbours of different parity are separated by a horizontal step · Interior of a simple closed walk has no pinch points · Hopf's Umlaufsatz

TheoremUpward crossings of vertically adjacent cells differ by separating steps#✓fully proved

The upward crossings from cell (a, b) are those from (a, b + 1) plus the horizontal steps between the two cells.

theorem upCross_vsplit (d : Fin n → Fin 4) (a b : ℤ) :
    upCross d a b = upCross d a (b + 1) + (midSet d a (b + 1)).card

Uses 4 · Used by 1

Statement usesUpward ray crossings above a cell · Horizontal steps on a unit segment

Proof usesVertices of a lattice walk from its step directions · Horizontal lattice direction

Used byAn odd number of horizontal steps flips the ray parity

TheoremAn odd number of horizontal steps flips the ray parity#✓fully proved

An odd number of horizontal steps between cells (a, b) and (a, b + 1) flips the ray parity.

theorem rayParity_vflip (d : Fin n → Fin 4) (a b : ℤ)
    (hodd : (midSet d a (b + 1)).card % 2 = 1) :
    rayParity d a b = rayParity d a (b + 1) + 1

Uses 4 · Used by 4

Statement usesRay-crossing parity of a lattice cell · Horizontal steps on a unit segment

Proof usesUpward ray crossings above a cell · Upward crossings of vertically adjacent cells differ by separating steps

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 · Hopf's Umlaufsatz

Theorem\(k + 2 \ne k\) in \(\mathrm{Fin}\, n\) for \(n \ge 3\)#✓fully proved

In Fin n with n ≥ 3, k + 2 ≠ k.

theorem not_add_two_self (hn : 3 ≤ n) (k : Fin n) : k + 1 + 1 ≠ k

Used by 2

Used byA simple closed walk traverses each horizontal segment at most once · A simple closed walk traverses each vertical segment at most once

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.