Contiguous top row of a walk to A closed walk crosses each horizontal line an even number of times

DefinitionContiguous top row of a walk#✓fully proved

The vertices of the walk at its maximal height cover every lattice point between any two of them, i.e. the top row of the walk is a contiguous horizontal segment.

def TopRowContiguous (d : Fin n → Fin 4) : Prop :=
  ∃ M : Fin n, (∀ j : Fin n, (pos d j).2 ≤ (pos d M).2) ∧
    ∀ a b : Fin n, (pos d a).2 = (pos d M).2 → (pos d b).2 = (pos d M).2 →
      ∀ x : ℤ, (pos d a).1 ≤ x → x ≤ (pos d b).1 →
        ∃ c : Fin n, pos d c = (x, (pos d M).2)

Uses 1 · Used by 2

Statement usesVertices of a lattice walk from its step directions

Used byTop row is contiguous when every top corner starts a single run · A single top run makes the top row contiguous

TheoremRecursion for the x-coordinate of a closed walk#✓fully proved

The x-coordinate recursion of a closed walk. See also StatMech.Onsager.WalkCrossing.fst_step.

theorem xco_succ (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) (k : Fin n) :
    (pos d (k + 1)).1 = (pos d k).1 + (stepOf (d k)).1

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 byNo east step leaves a rightmost vertex · No west step arrives at a rightmost vertex

TheoremRecursion for the y-coordinate of a closed walk#✓fully proved

The y-coordinate recursion of a closed walk. See also StatMech.Onsager.WalkCrossing.snd_step.

theorem yco_succ (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) (k : Fin n) :
    (pos d (k + 1)).2 = (pos d k).2 + (stepOf (d k)).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 byNo north step arrives at a lowest vertex · No south step leaves a lowest vertex

TheoremNo east step leaves a rightmost vertex#✓fully proved

No east step leaves a vertex of maximal x-coordinate.

theorem maxx_no_E_out (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) (k : Fin n)
    (hmax : ∀ j : Fin n, (pos d j).1 ≤ (pos d k).1) : d k ≠ 0

Uses 3

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

Proof usesRecursion for the x-coordinate of a closed walk

TheoremNo west step arrives at a rightmost vertex#✓fully proved

No west step arrives at a vertex of maximal x-coordinate.

theorem maxx_no_W_in (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) (k : Fin n)
    (hmax : ∀ j : Fin n, (pos d j).1 ≤ (pos d k).1) : d (k - 1) ≠ 2

Uses 3

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

Proof usesRecursion for the x-coordinate of a closed walk

TheoremNo south step leaves a lowest vertex#✓fully proved

No south step leaves a vertex of minimal y-coordinate.

theorem miny_no_S_out (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) (k : Fin n)
    (hmin : ∀ j : Fin n, (pos d k).2 ≤ (pos d j).2) : d k ≠ 3

Uses 3

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

Proof usesRecursion for the y-coordinate of a closed walk

TheoremNo north step arrives at a lowest vertex#✓fully proved

No north step arrives at a vertex of minimal y-coordinate.

theorem miny_no_N_in (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) (k : Fin n)
    (hmin : ∀ j : Fin n, (pos d k).2 ≤ (pos d j).2) : d (k - 1) ≠ 1

Uses 3

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

Proof usesRecursion for the y-coordinate of a closed walk

DefinitionNumber of left turns out of a given direction#✓fully proved

The number of left turns of d from direction c to direction c + 1.

def tcount (d : Fin n → Fin 4) (c : Fin 4) : ℕ :=
  (Finset.univ.filter (fun i : Fin n => d i = c ∧ d (i + 1) = c + 1)).card

Used by 3

Used byLeft turns are four times the north-to-west turns · Eight left turns give two north-then-west corners · Every direction is left by equally many left turns

DefinitionNumber of straight continuations in a given direction#✓fully proved

The number of straight continuations of d in direction c.

def scount (d : Fin n → Fin 4) (c : Fin 4) : ℕ :=
  (Finset.univ.filter (fun i : Fin n => d i = c ∧ d (i + 1) = c)).card

Used by 1

Used byEvery direction is left by equally many left turns

TheoremEvery direction is left by equally many left turns#✓fully proved

In a direction sequence without right turns, every direction is left by the same number of left turns.

theorem tcount_shift (d : Fin n → Fin 4)
    (hreflexfree : ∀ i : Fin n, d (i + 1) - d i = 0 ∨ d (i + 1) - d i = 1) (c : Fin 4) :
    tcount d c = tcount d (c + 1)

Uses 2 · Used by 1

Statement usesNumber of left turns out of a given direction

Proof usesNumber of straight continuations in a given direction

Used byLeft turns are four times the north-to-west turns

TheoremLeft turns are four times the north-to-west turns#✓fully proved

In a direction sequence without right turns, the number of left turns is four times the number of north-to-west turns.

theorem cc_eq_four_mul_tcount (d : Fin n → Fin 4)
    (hreflexfree : ∀ i : Fin n, d (i + 1) - d i = 0 ∨ d (i + 1) - d i = 1) :
    cc d = 4 * tcount d 1

Uses 3 · Used by 1

Statement usesNumber of left turns of a direction sequence · Number of left turns out of a given direction

Proof usesEvery direction is left by equally many left turns

Used byEight left turns give two north-then-west corners

TheoremEight left turns give two north-then-west corners#✓fully proved

Eight or more left turns, without right turns, give two distinct north-then-west corners.

theorem exists_two_top_corners (d : Fin n → Fin 4)
    (hreflexfree : ∀ i : Fin n, d (i + 1) - d i = 0 ∨ d (i + 1) - d i = 1)
    (h8 : 8 ≤ cc d) :
    ∃ i j : Fin n, i ≠ j ∧ d i = 1 ∧ d (i + 1) = 2 ∧ d j = 1 ∧ d (j + 1) = 2

Uses 3 · Used by 2

Statement usesNumber of left turns of a direction sequence

Proof usesLeft turns are four times the north-to-west turns · Number of left turns out of a given direction

Used byA unique top corner forces fewer than eight left turns · Four left turns, given that two corners force a self-intersection

TheoremA unique top corner forces fewer than eight left turns#✓fully proved

If the north-then-west corner is unique, a direction sequence without right turns has fewer than eight left turns.

theorem cc_lt_eight_of_uniqueTopCorner (d : Fin n → Fin 4)
    (hreflexfree : ∀ i : Fin n, d (i + 1) - d i = 0 ∨ d (i + 1) - d i = 1)
    (huniq : ∀ i j : Fin n, d i = 1 → d (i + 1) = 2 → d j = 1 → d (j + 1) = 2 → i = j) :
    cc d < 8

Uses 2

Statement usesNumber of left turns of a direction sequence

Proof usesEight left turns give two north-then-west corners

DefinitionVertical lattice direction#✓fully proved

The direction w is vertical (north or south).

def isVertEdge (w : Fin 4) : Prop := w = 1 ∨ w = 3

Used by 31

Used byNumber of crossings of a horizontal line · A closed walk crosses each horizontal line an even number of times · Crossing steps force a repeated vertex · Moving horizontally inside a closed walk · The north step at a corner blocks horizontal movement · Number of crossings of a horizontal ray · Ray parity is unchanged across a horizontal move · Upward crossing counts of horizontal neighbours sum to an even number · Left cells keep their ray parity on a straight step · No vertical step through a non-vertex point · Vertical steps separating two horizontal neighbour cells · Parity of upward crossings across a vertical segment · Index of a vertical step above a walk vertex · Index of a vertical step below a walk vertex · Steps on a vertical unit segment join its endpoints · A closed walk crosses each vertical line an even number of times · 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 · A vertical direction is not horizontal · A horizontal direction is not vertical · Ray parity is constant around a non-vertex point · Horizontal neighbours of different parity are separated by a vertical step · Face-graph adjacency as absence of a walk step between cells · Interior of a simple closed walk has no pinch points · Horizontally face-adjacent cells have the same ray parity · Hopf's Umlaufsatz

DefinitionHorizontal lattice direction#✓fully proved

The direction w is horizontal (east or west).

def isHorizEdge (w : Fin 4) : Prop := w = 0 ∨ w = 2

Used by 39

Used byA closed walk crosses each horizontal line an even number of times · Crossing steps force a repeated vertex · Moving vertically inside a closed walk · The west step at a corner blocks vertical movement · Ray parity is unchanged across a vertical move · Upward ray crossings above a cell · 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 · Index of a horizontal step right of a walk vertex · Index of a horizontal step left of a walk vertex · Left cells keep their ray parity on a straight step · Horizontal steps on a unit segment · No horizontal step starts at a non-vertex point · 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 · Steps on a horizontal unit segment join its endpoints · A west step on the top row is followed by west or south · Number of crossings of a vertical line · A closed walk crosses each vertical line an even number of times · 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 · An inside cell lies below a horizontal step · Finiteness of the interior of a closed walk · A vertical direction is not horizontal · A horizontal direction is not vertical · Ray parity is constant around a non-vertex point · Cells below a walk are outside · Face-graph adjacency as absence of a walk step between cells · Vertical neighbours of different parity are separated by a horizontal step · Interior of a simple closed walk has no pinch points · Vertically face-adjacent cells have the same ray parity · Hopf's Umlaufsatz

TheoremRecursion for the y-coordinate of a walk step#✓fully proved

The y-coordinate recursion of a closed walk. See also StatMech.Onsager.NoDoubleWind2.yco_succ.

theorem snd_step (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) (k : Fin n) :
    (pos d (k + 1)).2 = (pos d k).2 + (stepOf (d k)).2

Uses 3 · Used by 24

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 byA closed walk crosses each horizontal line an even number of times · Crossing steps force a repeated vertex · Upward crossing counts of horizontal neighbours sum to an even number · Index of a horizontal step right of a walk vertex · Index of a horizontal step left of a walk vertex · No horizontal step starts at a non-vertex point · No vertical step through a non-vertex point · Parity of upward crossings across a vertical segment · Index of a vertical step above a walk vertex · Index of a vertical step below a walk vertex · Some north-then-west corner has its below-left cell inside · Steps on a horizontal unit segment join its endpoints · Steps on a vertical unit segment join its endpoints · No north step leaves a highest vertex · A west step on the top row is followed by west or south · 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 · Ray parity is constant around a non-vertex point · Horizontally face-adjacent cells have the same ray parity · Vertically face-adjacent cells have the same ray parity

TheoremRecursion for the x-coordinate of a walk step#✓fully proved

The x-coordinate recursion of a closed walk. See also StatMech.Onsager.NoDoubleWind2.xco_succ.

theorem fst_step (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) (k : Fin n) :
    (pos d (k + 1)).1 = (pos d k).1 + (stepOf (d k)).1

Uses 3 · Used by 23

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 byCrossing steps force a repeated vertex · Upward crossing counts of horizontal neighbours sum to an even number · Index of a horizontal step right of a walk vertex · Index of a horizontal step left of a walk vertex · No horizontal step starts at a non-vertex point · No vertical step through a non-vertex point · Parity of upward crossings across a vertical segment · Index of a vertical step above a walk vertex · Index of a vertical step below a walk vertex · A step changes the x-coordinate by at most one · Some north-then-west corner has its below-left cell inside · Steps on a horizontal unit segment join its endpoints · Steps on a vertical unit segment join its endpoints · A closed walk crosses each vertical line an even number of times · 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 · Ray parity is constant around a non-vertex point · Horizontally face-adjacent cells have the same ray parity · Vertically face-adjacent cells have the same ray parity

DefinitionNumber of crossings of a horizontal line#✓fully proved

The number of vertical steps of the walk crossing the horizontal line y = m + 1/2, i.e. vertical steps between heights m and m + 1.

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

Uses 2 · Used by 1

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

Used byA closed walk crosses each horizontal line an even number of times

TheoremA closed walk crosses a horizontal line equally often up and down#✓fully proved

A closed walk crosses the line y = m + 1/2 upwards as often as downwards.

theorem upDown_card_eq (d : Fin n → Fin 4) (_hclosed : ∑ i, stepOf (d i) = 0) (m : ℤ) :
    (Finset.univ.filter
        (fun k : Fin n => (pos d k).2 ≤ m ∧ m + 1 ≤ (pos d (k + 1)).2)).card
      = (Finset.univ.filter
        (fun k : Fin n => m + 1 ≤ (pos d k).2 ∧ (pos d (k + 1)).2 ≤ m)).card

Uses 2 · Used by 1

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

Used byA closed walk crosses each horizontal line an even number of times

TheoremA closed walk crosses each horizontal line an even number of times#✓fully proved

A closed walk crosses each horizontal line y = m + 1/2 an even number of times.

theorem fullLineCross_even (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) (m : ℤ) :
    Even (fullLineCross d m)

Uses 8

Statement usesUnit lattice step in a given direction · Number of crossings of a horizontal line

Proof usesVertices of a lattice walk from its step directions · Coordinates of the four lattice steps · Horizontal lattice direction · Vertical lattice direction · Recursion for the y-coordinate of a walk step · A closed walk crosses a horizontal line equally often up and down

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.