A lattice point lies on a walk step to Four left turns, given that two corners force a self-intersection

DefinitionA lattice point lies on a walk step#✓fully proved

The lattice point p lies on the closed segment traversed by step k.

def onEdge (d : Fin n → Fin 4) (k : Fin n) (p : ℤ × ℤ) : Prop :=
  (min (pos d k).1 (pos d (k + 1)).1 ≤ p.1 ∧ p.1 ≤ max (pos d k).1 (pos d (k + 1)).1) ∧
    (min (pos d k).2 (pos d (k + 1)).2 ≤ p.2 ∧ p.2 ≤ max (pos d k).2 (pos d (k + 1)).2)

Uses 1 · Used by 1

Statement usesVertices of a lattice walk from its step directions

Used byCrossing steps force a repeated vertex

TheoremCrossing steps force a repeated vertex#✓fully proved

If a horizontal and a vertical step that share no index endpoint meet at a point, the walk visits some vertex twice.

theorem edges_cross_not_injective (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (k j : Fin n) (hk : isHorizEdge (d k)) (hj : isVertEdge (d j))
    (hne1 : k ≠ j) (hne2 : k + 1 ≠ j) (hne3 : k ≠ j + 1) (hne4 : k + 1 ≠ j + 1)
    (p : ℤ × ℤ) (hpk : onEdge d k p) (hpj : onEdge d j p) :
    ¬ Function.Injective (pos d)

Uses 7

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Horizontal lattice direction · Vertical lattice direction · A lattice point lies on a walk step

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

DefinitionNumber of crossings of a horizontal ray#✓fully proved

The number of vertical steps crossing the line y = m + 1/2 strictly to the right of x = qx.

def rayCross (d : Fin n → Fin 4) (m qx : ℤ) : ℕ :=
  (Finset.univ.filter (fun k : Fin n =>
    isVertEdge (d k) ∧ qx < (pos d k).1 ∧
      min ((pos d k).2) ((pos d (k + 1)).2) = m)).card

Uses 2

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

DefinitionUpward ray crossings above a cell#✓fully proved

The number of horizontal steps of the walk on the column [a, a + 1] strictly above the cell (a, b): the crossings of the upward vertical ray from the center of that cell.

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

Uses 2 · Used by 14

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

Used byRay-crossing parity of a lattice cell · Ray parity is unchanged across a horizontal move · Cells above a walk are outside · Ray parity is unchanged across a vertical move · Upward crossing counts of horizontal neighbours sum to an even number · No upward crossings for cells above a walk · Upward crossing count is unchanged across a vertical move · Ray parity across a vertical segment counts separating steps · An odd number of horizontal steps flips the ray parity · Parity of upward crossings across a vertical segment · Upward crossings of vertically adjacent cells differ by separating steps · Some north-then-west corner has its below-left cell inside · An inside cell lies below a horizontal step · Cells below a walk are outside

DefinitionRay-crossing parity of a lattice cell#✓fully proved

The parity of the number of crossings of the upward ray from the center of cell (a, b) with the walk; cells with parity 1 are inside the walk.

def rayParity (d : Fin n → Fin 4) (a b : ℤ) : ZMod 2 := (upCross d a b : ZMod 2)

Uses 1 · Used by 49

Statement usesUpward ray crossings above a cell

Used byMoving horizontally inside a closed walk · Moving vertically inside a closed walk · Ray parity is unchanged across a horizontal move · Cells above a walk are outside · Ray parity is unchanged across a vertical move · 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 · An odd number of vertical steps flips the ray parity · Ray parity across a vertical segment counts separating steps · An odd number of horizontal steps flips the ray parity · Some north-then-west corner has its below-left cell inside · Corner count of the interior counts inside cells around a point · 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 · Zero corner weight where the walk continues horizontally · Zero corner weight where the walk continues vertically · An inside cell lies below a horizontal step · Interior cells by the even-odd rule · Finiteness of the interior of a closed walk · Ray parity is constant around a non-vertex point · Cells below a walk are outside · Horizontal neighbours of different parity are separated by a vertical step · Ray-parity interior equals the bounded face components · Corner weights at the turns of a walk without right turns · Zero corner weight of the interior off the walk · Vertical neighbours of different parity are separated by a horizontal step · Interior of a simple closed walk has no pinch points · The inner face component is finite · The face below the inside top corner is inside · Top corner with an inside cell below it · Defining property of the inside top corner · A face far outside the walk has ray parity zero · 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 · Ray parity is constant on face-graph components · Zero corner weight of the bounded face off the walk · 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 · Lattice Jordan curve theorem, even-odd form · A side between interior and exterior cells is a walk edge · Ray-parity interior equals the bounded face · A walk without right turns is positively oriented · Hopf's Umlaufsatz

LemmaUpward crossing count is unchanged across a vertical move#✓fully proved

The upward crossing count is the same for cells (a, b) and (a, b + 1) when no horizontal step lies between them.

lemma upCross_vstep (d : Fin n → Fin 4) (a b : ℤ)
    (h : ∀ k : Fin n, isHorizEdge (d k) →
      min ((pos d k).1) ((pos d (k+1)).1) = a → (pos d k).2 ≠ b + 1) :
    upCross d a b = upCross d a (b + 1)

Uses 3 · Used by 1

Statement usesVertices of a lattice walk from its step directions · Upward ray crossings above a cell · Horizontal lattice direction

Used byRay parity is unchanged across a vertical move

LemmaRay parity is unchanged across a vertical move#✓fully proved

The ray parity is the same for cells (a, b) and (a, b + 1) when no horizontal step lies between them.

lemma rayParity_vstep (d : Fin n → Fin 4) (a b : ℤ)
    (h : ∀ k : Fin n, isHorizEdge (d k) →
      min ((pos d k).1) ((pos d (k+1)).1) = a → (pos d k).2 ≠ b + 1) :
    rayParity d a b = rayParity d a (b + 1)

Uses 5 · Used by 9

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 · Upward crossing count is unchanged across a vertical move

Used byMoving vertically inside a closed walk · Left cells keep their ray parity on a straight step · 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 west direction · Zero corner weight where the walk continues vertically · Ray parity is constant around a non-vertex point · Vertical neighbours of different parity are separated by a horizontal step · Vertically face-adjacent cells have the same ray parity

LemmaNo upward crossings for cells above a walk#✓fully proved

Cells at or above the top height of the walk have no upward crossings.

lemma upCross_topOutside (d : Fin n → Fin 4) (a b T : ℤ)
    (hT : ∀ j : Fin n, (pos d j).2 ≤ T) (hb : T ≤ b) :
    upCross d a b = 0

Uses 3 · Used by 1

Statement usesVertices of a lattice walk from its step directions · Upward ray crossings above a cell

Proof usesHorizontal lattice direction

Used byCells above a walk are outside

LemmaCells above a walk are outside#✓fully proved

Cells at or above the top height of the walk are outside.

lemma rayParity_topOutside (d : Fin n → Fin 4) (a b T : ℤ)
    (hT : ∀ j : Fin n, (pos d j).2 ≤ T) (hb : T ≤ b) :
    rayParity d a b = 0

Uses 4 · Used by 2

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

Proof usesUpward ray crossings above a cell · No upward crossings for cells above a walk

Used byA face far outside the walk has ray parity zero · Hopf's Umlaufsatz

LemmaUpward crossing counts of horizontal neighbours sum to an even number#✓fully proved

When no vertical step separates the cells (a, b) and (a + 1, b), their upward crossing counts add up to an even number.

lemma upCross_hstep (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) (a b : ℤ)
    (hstr : ∀ 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))) :
    upCross d a b + upCross d (a + 1) b
      = 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 8 · 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 lattice direction

Proof usesCoordinates of the four lattice steps · Recursion for the x-coordinate of a walk step · Horizontal lattice direction · Recursion for the y-coordinate of a walk step

Used byRay parity is unchanged across a horizontal move

LemmaRay parity is unchanged across a horizontal move#✓fully proved

The ray parity is the same for cells (a, b) and (a + 1, b) when no vertical step lies between them.

lemma rayParity_hstep (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) (a b : ℤ)
    (hstr : ∀ 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))) :
    rayParity d a b = rayParity d (a + 1) b

Uses 6 · Used by 8

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

Proof usesUpward ray crossings above a cell · Upward crossing counts of horizontal neighbours sum to an even number

Used byMoving horizontally inside a closed walk · Left cells keep their ray parity on a straight step · 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 · Ray parity is constant around a non-vertex point · Horizontal neighbours of different parity are separated by a vertical step · Horizontally face-adjacent cells have the same ray parity

TheoremMoving horizontally inside a closed walk#✓fully proved

If cell (a, b) is inside and no vertical step separates it from (a + 1, b), then (a + 1, b) is inside.

theorem inside_climb_x (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) (a b : ℤ)
    (hinside : rayParity d a b = 1)
    (hstr : ∀ 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))) :
    rayParity d (a + 1) b = 1

Uses 5

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

Proof usesRay parity is unchanged across a horizontal move

TheoremMoving vertically inside a closed walk#✓fully proved

If cell (a, b) is inside and no horizontal step separates it from (a, b + 1), then (a, b + 1) is inside.

theorem inside_climb_y (d : Fin n → Fin 4) (a b : ℤ)
    (hinside : rayParity d a b = 1)
    (h : ∀ k : Fin n, isHorizEdge (d k) →
      min ((pos d k).1) ((pos d (k + 1)).1) = a → (pos d k).2 ≠ b + 1) :
    rayParity d a (b + 1) = 1

Uses 4

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

Proof usesRay parity is unchanged across a vertical move

TheoremCoordinates of the vertices around a north-then-west corner#✓fully proved

The vertices before and after a north-then-west corner.

theorem nw_corner_coords (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (i : Fin n) (hN : d i = 1) (hW : d (i + 1) = 2) :
    pos d i = ((pos d (i + 1)).1, (pos d (i + 1)).2 - 1) ∧
      pos d (i + 1 + 1) = ((pos d (i + 1)).1 - 1, (pos d (i + 1)).2)

Uses 3 · Used by 2

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

Proof usesForward vertex recursion of a closed lattice walk

Used byThe north step at a corner blocks horizontal movement · The west step at a corner blocks vertical movement

TheoremThe north step at a corner blocks horizontal movement#✓fully proved

At a north-then-west corner, the north step separates the cell below-left of the corner from its right neighbour.

theorem nw_corner_not_climbable_x (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (i : Fin n) (hN : d i = 1) (hW : d (i + 1) = 2) :
    ¬ (∀ k : Fin n, isVertEdge (d k) → (pos d k).1 = ((pos d (i + 1)).1 - 1) + 1 →
        ¬ (min ((pos d k).2) ((pos d (k + 1)).2) ≤ (pos d (i + 1)).2 - 1 ∧
           (pos d (i + 1)).2 - 1 < max ((pos d k).2) ((pos d (k + 1)).2)))

Uses 4

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

Proof usesCoordinates of the vertices around a north-then-west corner

TheoremThe west step at a corner blocks vertical movement#✓fully proved

At a north-then-west corner, the west step separates the cell below-left of the corner from its top neighbour.

theorem nw_corner_not_climbable_y (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (i : Fin n) (hN : d i = 1) (hW : d (i + 1) = 2) :
    ¬ (∀ k : Fin n, isHorizEdge (d k) →
        min ((pos d k).1) ((pos d (k + 1)).1) = (pos d (i + 1)).1 - 1 →
        (pos d k).2 ≠ ((pos d (i + 1)).2 - 1) + 1)

Uses 4

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

Proof usesCoordinates of the vertices around a north-then-west corner

TheoremUniqueness of the lexicographically largest vertex#✓fully proved

In a simple walk the lexicographically largest vertex is attained at a unique index.

theorem lexmax_unique (d : Fin n → Fin 4) (hsimple : Function.Injective (pos d))
    {M M' : Fin n} (hM : ∀ j : Fin n, toLex (pos d j) ≤ toLex (pos d M))
    (hM' : ∀ j : Fin n, toLex (pos d j) ≤ toLex (pos d M')) :
    M = M'

Uses 1

Statement usesVertices of a lattice walk from its step directions

TheoremExistence of a north-then-west corner#✓fully proved

A closed walk without right turns has a north-then-west corner.

theorem exists_lexmax_nw_corner (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hreflexfree : ∀ i : Fin n, d (i + 1) - d i = 0 ∨ d (i + 1) - d i = 1) :
    ∃ i : Fin n, d i = 1 ∧ d (i + 1) = 2

Uses 2

Statement usesUnit lattice step in a given direction

Proof usesNorth step followed by west step at the top corner of a walk

DefinitionTwo north-then-west corners force a self-intersection#✓fully proved

Any two distinct north-then-west corners of d force pos d to be non-injective.

def two_nw_corners_not_injective (d : Fin n → Fin 4) : Prop :=
  ∀ i j : Fin n, i ≠ j → d i = 1 → d (i + 1) = 2 → d j = 1 → d (j + 1) = 2 →
    ¬ Function.Injective (pos d)

Uses 1 · Used by 1

Statement usesVertices of a lattice walk from its step directions

Used byFour left turns, given that two corners force a self-intersection

TheoremFour left turns, given that two corners force a self-intersection#✓fully proved

A simple closed walk without right turns has four left turns, assuming that two distinct north-then-west corners force a self-intersection.

theorem cc_eq_four_of_selfAvoidanceWall (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)
    (hwall : two_nw_corners_not_injective d) :
    cc d = 4

Uses 7

Statement usesNumber of left turns of a direction sequence · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · Two north-then-west corners force a self-intersection

Proof usesWithout right turns, the number of left turns is divisible by four · A closed walk without right turns has at least four left turns · Eight left turns give two north-then-west corners

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.