Unit lattice step in a given direction to Distinct north-then-west corners sit at distinct vertices

DefinitionUnit lattice step in a given direction#✓fully proved

The unit step of ℤ² in direction w: 0 ↦ (1, 0) (east), 1 ↦ (0, 1) (north), 2 ↦ (-1, 0) (west), 3 ↦ (0, -1) (south).

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

Used by 140

Used byExactly four left turns when simplicity rules out eight · A closed walk without right turns turns at least once · A closed walk without right turns has at least four left turns · North step followed by west step at the top corner of a walk · Previous and next vertices of a north-then-west corner · Vertices of a lattice walk from its step directions · Backward vertex recursion of a closed lattice walk · Forward vertex recursion of a closed lattice walk · Closed lattice walk starts at the origin · Coordinates of the four lattice steps · North-then-west corner at the highest vertices · South-then-east corner at the lowest vertices · Recursion for the x-coordinate of a walk step · A closed walk crosses each horizontal line an even number of times · No east step leaves a rightmost vertex · No west step arrives at a rightmost vertex · No north step arrives at a lowest vertex · No south step leaves a lowest vertex · Recursion for the y-coordinate of a walk step · A closed walk crosses a horizontal line equally often up and down · Recursion for the x-coordinate of a closed walk · Recursion for the y-coordinate of a closed walk · Four left turns, given that two corners force a self-intersection · Crossing steps force a repeated vertex · Existence of a north-then-west corner · Moving horizontally inside a closed walk · Coordinates of the vertices around a north-then-west corner · The north step at a corner blocks horizontal movement · The west step at a corner blocks vertical movement · Ray parity is unchanged across a horizontal move · 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 · Steps around a left turn share their left cell · Left cells keep their ray parity on a straight step · Left parity is constant along a walk without right turns · Consecutive steps have the same left parity · No horizontal step starts at a non-vertex point · No vertical step through a non-vertex point · An 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 · Index of a vertical step above a walk vertex · Index of a vertical step below a walk vertex · A closed walk is not all west steps · A west run from a highest vertex ends in a south step · Position after a run of west steps · A step changes the x-coordinate by at most one · Some north-then-west corner has its below-left cell inside · A simple closed walk traverses each horizontal segment at most once · Steps on a horizontal unit segment join its endpoints · A simple closed walk traverses each vertical segment at most once · Steps on a vertical unit segment join its endpoints · A north step into a highest vertex is followed by a west step · No south step arrives at a highest vertex · No north step leaves a highest vertex · Top row is contiguous when every top corner starts a single run · A single top run makes the top row contiguous · A west step on the top row is followed by west or south · A closed walk crosses each vertical line an even number of times · Corner 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 · Finite set of interior cells of a closed walk · 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 · Face-graph adjacency as absence of a walk step between cells · Ray-parity interior equals the bounded face components · 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 · Each lattice step has \(\ell^1\)-length one · Consecutive walk vertices are adjacent in the square lattice · Lattice Jordan curve theorem for simple closed walks · Simple closed walk as an embedded cycle graph · Subgraph of a simple closed lattice walk has cycle rank one · Cells of the inner face component · The inner component has finitely many cells · Neighbours in the image graph are walk predecessor and successor · Inner component of the face graph · The inner face component is finite · Cells of the bounded face of a simple closed walk · Face below-left of the inside top corner · The face below the inside top corner is inside · Top corner with an inside cell below it · Defining property of the inside top corner · Membership in the bounded face · 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 · Each walk step is an edge of the image graph · Simple closed walk as a planar subgraph · Face graph of a closed walk · Corner count of the bounded face at a walk vertex · Zero corner weight of the bounded face off the walk · Vertices of a walk's image graph are adjacent only to walk neighbours · 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 · Lattice Jordan curve theorem, even-odd form · Bounded face of a simple closed walk has no pinch points · Face-graph component of an interior cell · Pinch count of the bounded face is zero · Three walk edges cannot meet at a vertex · No right cell lies in the bounded face · A side between interior and exterior cells is a walk edge · Cells on either side of a step lie in different faces · Corner defect of the bounded face equals the number of left turns · Corner weight of the bounded face at a walk vertex · Discrete Umlaufsatz for walks of length at least three, shifted form · Discrete Umlaufsatz for walks of length at least three · Discrete Umlaufsatz for lattice walks without right turns · Interior of a simple closed walk has Euler characteristic at most 1 · A simple closed walk without right turns has under eight left turns · Connectedness of the skeleton of the interior · Ray-parity interior equals the bounded face · Interior cells have connected lower-left corners · A walk without right turns is positively oriented · A closed walk without right turns has length at least three · Hopf's Umlaufsatz · Total displacement of a list of lattice directions · Lattice points visited by a path from the origin · Onsager's formula

DefinitionVertices of a lattice walk from its step directions#✓fully proved

The k-th vertex of the lattice walk with step directions d: the sum of the steps stepOf (d i) for i < k, so that pos d 0 = 0.

def pos {n : ℕ} [NeZero n] (d : Fin n → Fin 4) (k : Fin n) : ℤ × ℤ :=
  ∑ i ∈ Finset.filter (· < k) Finset.univ, stepOf (d i)

Uses 1 · Used by 158

Statement usesUnit lattice step in a given direction

Used byExactly four left turns when simplicity rules out eight · North step followed by west step at the top corner of a walk · Previous and next vertices of a north-then-west corner · Distinct north-then-west corners sit at distinct vertices · Backward vertex recursion of a closed lattice walk · Forward vertex recursion of a closed lattice walk · Closed lattice walk starts at the origin · North-then-west corner at the highest vertices · South-then-east corner at the lowest vertices · Recursion for the x-coordinate of a walk step · Number of crossings of a horizontal line · A closed walk crosses each horizontal line an even number of times · No east step leaves a rightmost vertex · No west step arrives at a rightmost vertex · No north step arrives at a lowest vertex · No south step leaves a lowest vertex · Recursion for the y-coordinate of a walk step · Contiguous top row of a walk · A closed walk crosses a horizontal line equally often up and down · Recursion for the x-coordinate of a closed walk · Recursion for the y-coordinate of a closed walk · Four left turns, given that two corners force a self-intersection · Crossing steps force a repeated vertex · Moving horizontally inside a closed walk · Moving vertically inside a closed walk · Uniqueness of the lexicographically largest vertex · Coordinates of the vertices around a north-then-west corner · The north step at a corner blocks horizontal movement · The west step at a corner blocks vertical movement · A lattice point lies on a walk step · Number of crossings of a horizontal ray · Ray parity is unchanged across a horizontal move · Cells above a walk are outside · Ray parity is unchanged across a vertical move · Two north-then-west corners force a self-intersection · 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 · Steps 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 · Left parity is constant along a walk without right turns · Consecutive steps have the same left parity · Horizontal steps on a unit segment · No horizontal step starts at a non-vertex point · No vertical step through a non-vertex point · Ray parity across a vertical segment counts separating steps · Vertical steps separating two horizontal neighbour cells · Parity of upward crossings across a vertical segment · Upward crossings of vertically adjacent cells differ by separating steps · Index of a vertical step above a walk vertex · Index of a vertical step below a walk vertex · A west run from a highest vertex ends in a south step · Position after a run of west steps · A step changes the x-coordinate by at most one · A closed walk crosses a vertical line equally often left and right · Some north-then-west corner has its below-left cell inside · A simple closed walk traverses each horizontal segment at most once · Steps on a horizontal unit segment join its endpoints · Single west run covering the top row · A west run covering the top row is a single top run · A simple closed walk traverses each vertical segment at most once · Steps on a vertical unit segment join its endpoints · A north step into a highest vertex is followed by a west step · No south step arrives at a highest vertex · No north step leaves a highest vertex · Top row is contiguous when every top corner starts a single run · A single top run makes the top row contiguous · 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 · 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 · Minimal height of a walk · Maximal height of a walk · Face-graph adjacency as absence of a walk step between cells · Ray-parity interior equals the bounded face components · 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 · Vertical neighbours of different parity are separated by a horizontal step · Pinch count of the ray-parity interior is zero · Interior of a simple closed walk has no pinch points · Vertex of a walk as a lattice site · Vertices of a simple walk are distinct sites · Consecutive walk vertices are adjacent in the square lattice · Lattice Jordan curve theorem for simple closed walks · Simple closed walk as an embedded cycle graph · Subgraph of a simple closed lattice walk has cycle rank one · Cells of the inner face component · The inner component has finitely many cells · Neighbours in the image graph are walk predecessor and successor · Inner component of the face graph · The inner face component is finite · Cells of the bounded face of a simple closed walk · Face below-left of the inside top corner · The face below the inside top corner is inside · Top corner with an inside cell below it · Defining property of the inside top corner · Membership in the bounded face · 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 · Each walk step is an edge of the image graph · Simple closed walk as a planar subgraph · Face graph of a closed walk · Corner count of the bounded face at a walk vertex · Zero corner weight of the bounded face off the walk · Vertices of a walk's image graph are adjacent only to walk neighbours · Cell to the left of a walk step · 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 · Lattice Jordan curve theorem, even-odd form · Bounded face of a simple closed walk has no pinch points · Face-graph component of an interior cell · Pinch count of the bounded face is zero · Three walk edges cannot meet at a vertex · Cell to the right of a walk step · No right cell lies in the bounded face · A side between interior and exterior cells is a walk edge · Cells on either side of a step lie in different faces · Corner defect of the bounded face equals the number of left turns · Corner weight of the bounded face at a walk vertex · Discrete Umlaufsatz for walks of length at least three, shifted form · Discrete Umlaufsatz for walks of length at least three · Discrete Umlaufsatz for lattice walks without right turns · Interior of a simple closed walk has Euler characteristic at most 1 · A simple closed walk without right turns has under eight left turns · Connectedness of the skeleton of the interior · Ray-parity interior equals the bounded face · Interior cells have connected lower-left corners · Agreement of the two definitions of the left cell · A walk without right turns is positively oriented · Hopf's Umlaufsatz · Lattice point of a period state · Points of the periodic lift of a torus loop · Onsager's formula

DefinitionNumber of left turns of a direction sequence#✓fully proved

The number of counterclockwise (left) quarter turns of the cyclic direction sequence d, i.e. of indices i with d (i + 1) - d i = 1.

def cc {n : ℕ} [NeZero n] (d : Fin n → Fin 4) : ℕ :=
  (Finset.univ.filter (fun i : Fin n => d (i + 1) - d i = 1)).card

Used by 15

Used byExactly four left turns when simplicity rules out eight · A closed walk without right turns turns at least once · Without right turns, the number of left turns is divisible by four · A closed walk without right turns has at least four left turns · Left turns are four times the north-to-west turns · A unique top corner forces fewer than eight left turns · Eight left turns give two north-then-west corners · Four left turns, given that two corners force a self-intersection · 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 bounded face equals the number of left turns · Discrete Umlaufsatz for walks of length at least three, shifted form · Discrete Umlaufsatz for walks of length at least three · Discrete Umlaufsatz for lattice walks without right turns · A simple closed walk without right turns has under eight left turns

TheoremTurns of a cyclic direction sequence sum to zero#✓fully proved

The turns of a cyclic direction sequence sum to zero in Fin 4.

theorem sum_turns_zero {n : ℕ} [NeZero n] (d : Fin n → Fin 4) :
    (∑ i : Fin n, (d (i + 1) - d i)) = 0

Used by 1

Used byWithout right turns, the number of left turns is divisible by four

TheoremWithout right turns, the number of left turns is divisible by four#✓fully proved

If every turn is straight or left, the number of left turns is divisible by 4.

theorem four_dvd_cc {n : ℕ} [NeZero n] (d : Fin n → Fin 4)
    (hreflexfree : ∀ i : Fin n, d (i + 1) - d i = 0 ∨ d (i + 1) - d i = 1) :
    4 ∣ cc d

Uses 2 · Used by 3

Statement usesNumber of left turns of a direction sequence

Proof usesTurns of a cyclic direction sequence sum to zero

Used byExactly four left turns when simplicity rules out eight · A closed walk without right turns has at least four left turns · Four left turns, given that two corners force a self-intersection

TheoremA closed walk without right turns turns at least once#✓fully proved

A closed walk with only straight steps and left turns turns at least once.

theorem cc_pos {n : ℕ} [NeZero n] (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) :
    0 < cc d

Uses 2 · Used by 1

Statement usesNumber of left turns of a direction sequence · Unit lattice step in a given direction

Used byA closed walk without right turns has at least four left turns

TheoremA closed walk without right turns has at least four left turns#✓fully proved

A closed walk with only straight steps and left turns has at least four left turns.

theorem four_le_cc {n : ℕ} [NeZero n] (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) :
    4 ≤ cc d

Uses 4 · Used by 4

Statement usesNumber of left turns of a direction sequence · Unit lattice step in a given direction

Proof usesA closed walk without right turns turns at least once · Without right turns, the number of left turns is divisible by four

Used byExactly four left turns when simplicity rules out eight · Four left turns, given that two corners force a self-intersection · Four left turns from a pinch-free interior of Euler characteristic 1 · Discrete Umlaufsatz for walks of length at least three, shifted form

TheoremExactly four left turns when simplicity rules out eight#✓fully proved

A closed walk with only straight steps and left turns has exactly four left turns, provided simplicity rules out eight or more.

theorem base_cc_eq_four {n : ℕ} [NeZero n] (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)
    (hnodbl : Function.Injective (pos d) → cc d < 8) :
    cc d = 4

Uses 5

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

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

DefinitionReverse of a dart#✓fully proved

The reverse of a dart: it starts at the head of d and points in the opposite direction.

def ons_dartRev (L : ℕ) (d : ons_Dart L) : ons_Dart L :=
  (ons_dirStep L d.2 d.1, d.2 + 2)

Uses 2 · Used by 60

Statement usesDarts of the square-lattice torus · Neighbouring site in a given direction on the torus

Used byMasked edge-weighted bucket: walks through a dart, not its reverse · Masked edge-weighted bucket: walks avoiding a dart and its reverse · Edge-weighted twisted bucket: walks through a dart, not its reverse · Edge-weighted twisted bucket: walks avoiding a dart and its reverse · Spin Kac-Ward identities from the decorated-torus formal identity · Edge-weighted root identity from the decorated-torus formal identity · Adding a dart and its reverse to the masked set · Kac-Ward bucket: walks through a dart, not its reverse · Kac-Ward bucket: walks avoiding a dart and its reverse · Reverse of a closed walk · Product of first-return factors along a dart elimination · Masked twisted bucket: walks through a dart, not its reverse · Masked twisted bucket: walks avoiding a dart and its reverse · Twisted bucket: walks through a dart, not its reverse · Twisted bucket: walks avoiding a dart and its reverse · One-edge decorated walk along an external edge · Externality of a decorated edge · External part of a loop exponent · Darts of a loop with their reverses · Masked closed-walk weight through a dart but not its reverse · Masked closed-walk weight avoiding a dart and its reverse · Column weights of the column-scaled augmented matrix · Closed-walk weight through a dart but not its reverse · Closed-walk weight avoiding a dart and its reverse · Exponent of a Kac-Ward transition · Decorated even subgraphs containing a given external edge · Cycle removal identity for decorated even subgraphs · Split of a decorated even subgraph into a rooted cycle and remainder · Chosen split of a decorated even subgraph at an external edge · Even subgraphs of the decorated torus graph · Decorated spin polynomial · Onsager's formula · Torus even subgraph of a decorated even subgraph · Edge coefficient identity on the \(L \times L\) torus · Adjacency of the decorated torus graph · Test for a dart traversing an external edge · Port-pattern bit of an unordered decorated edge · Interior points of the route of a decorated edge · Four-step route of a decorated edge in the finer torus · Step directions of the route of a decorated edge · Decorated graph of the torus · Reversal on augmented states · Column weights of the balanced augmented matrix · Column weights of the augmented Kac-Ward matrix · Row factor of the rank-two middle-edge term · Port-pattern bit of the decorated edge between two darts · Internal path between two ports at a site · Internal walk between two ports at a site · Decorated walk of a Kac-Ward transition · Decorated weight of a Kac-Ward transition · Even decorated subgraph determined by a port pattern · Decorated character sum with weights on all edges · Port bit of a dart in a decorated edge set · Equivalence between even decorated subgraphs and port patterns · Equivalence between even subgraphs of the torus and its decoration · Equivalence between even torus subgraphs and port patterns · Port pattern of an even subgraph of the torus · Port pattern on the darts of the torus · Port pattern of an even decorated subgraph · Decorated weights twisted by seam signs

DefinitionTurn between two directions as an element of \(\mathbb{Z}/4\)#✓fully proved

The turn from direction μ to ν as an element of ZMod 4.

def ons_turnZ (μ ν : Fin 4) : ZMod 4 := (ν : ZMod 4) - (μ : ZMod 4)

Used by 1

Used byOnsager's formula

DefinitionInteger turn exponent between two directions#✓fully proved

The integer turn exponent from μ to ν: 1 for a left turn, -1 for a right turn, 0 for going straight (and, by convention, for a U-turn).

def ons_turnPow (μ ν : Fin 4) : ℤ :=
  if ν = μ then 0 else if ν = μ + 1 then 1 else if ν = μ + 2 then 0 else -1

Used by 4

Used byHopf's Umlaufsatz · Cyclic turning sum of a direction list · Open turning sum of a direction list · Onsager's formula

TheoremClosed lattice walk starts at the origin#✓fully proved

The walk starts at the origin.

theorem pos_zero (d : Fin n → Fin 4) : pos d 0 = 0

Uses 2 · Used by 2

Statement usesVertices of a lattice walk from its step directions

Proof usesUnit lattice step in a given direction

Used byForward vertex recursion of a closed lattice walk · Onsager's formula

TheoremForward vertex recursion of a closed lattice walk#✓fully proved

Vertex recursion of a closed walk: the next vertex is the current one plus the current step (indices taken cyclically).

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

Uses 3 · Used by 25

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

Proof usesClosed lattice walk starts at the origin

Used byNorth step followed by west step at the top corner of a walk · Previous and next vertices of a north-then-west corner · Backward vertex recursion of a closed lattice walk · North-then-west corner at the highest vertices · South-then-east corner at the lowest vertices · Recursion for the x-coordinate of a walk step · Recursion for the y-coordinate of a walk step · Recursion for the x-coordinate of a closed walk · Recursion for the y-coordinate of a closed walk · Coordinates of the vertices around a north-then-west corner · Steps around a left turn share their left cell · Left cells keep their ray parity on a straight step · Position after a run of west steps · Some north-then-west corner has its below-left cell inside · 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 · Consecutive walk vertices are adjacent in the square lattice · Corner count of the bounded face at a walk vertex · Consecutive left cells on a straight step are face-adjacent · Consecutive left cells have the same ray parity · Left and right cells of a step share that step · Hopf's Umlaufsatz · Onsager's formula

TheoremBackward vertex recursion of a closed lattice walk#✓fully proved

Vertex recursion of a closed walk read backwards from vertex M.

theorem pos_pred (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) (M : Fin n) :
    pos d M = pos d (M - 1) + stepOf (d (M - 1))

Uses 3 · Used by 7

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 byNorth step followed by west step at the top corner of a walk · Previous and next vertices of a north-then-west corner · North-then-west corner at the highest vertices · South-then-east corner at the lowest vertices · Some north-then-west corner has its below-left cell inside · No south step arrives at a highest vertex · Every left cell has ray parity one

TheoremCoordinates of the four lattice steps#✓fully proved

The four lattice steps, case by case.

theorem stepOf_coords (w : Fin 4) :
    (w = 0 ∧ stepOf w = (1, 0)) ∨ (w = 1 ∧ stepOf w = (0, 1)) ∨
    (w = 2 ∧ stepOf w = (-1, 0)) ∨ (w = 3 ∧ stepOf w = (0, -1))

Uses 1 · Used by 9

Statement usesUnit lattice step in a given direction

Used byNorth step followed by west step at the top corner of a walk · North-then-west corner at the highest vertices · South-then-east corner at the lowest vertices · A closed walk crosses each horizontal line an even number of times · Upward crossing counts of horizontal neighbours sum to an even number · Parity of upward crossings across a vertical segment · Some north-then-west corner has its below-left cell inside · A closed walk crosses each vertical line an even number of times · Straight steps of a simple closed walk carry no corner weight

TheoremNorth step followed by west step at the top corner of a walk#✓fully proved

A closed walk with only straight steps and left turns has a north step immediately followed by a west step (at its lexicographically largest vertex).

theorem lexmax_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) :
    ∃ M : Fin n, d (M - 1) = 1 ∧ d M = 2

Uses 5 · Used by 1

Statement usesUnit lattice step in a given direction

Proof usesVertices of a lattice walk from its step directions · Backward vertex recursion of a closed lattice walk · Forward vertex recursion of a closed lattice walk · Coordinates of the four lattice steps

Used byExistence of a north-then-west corner

TheoremNorth-then-west corner at the highest vertices#✓fully proved

A closed walk without right turns has a north-then-west corner at the rightmost of its highest vertices.

theorem ymax_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) :
    ∃ M : Fin n, d (M - 1) = 1 ∧ d M = 2 ∧
      (∀ j : Fin n, (pos d j).2 ≤ (pos d M).2) ∧
      (∀ j : Fin n, (pos d j).2 = (pos d M).2 → (pos d j).1 ≤ (pos d M).1)

Uses 5 · Used by 1

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

Proof usesBackward vertex recursion of a closed lattice walk · Forward vertex recursion of a closed lattice walk · Coordinates of the four lattice steps

Used byTop row is contiguous when every top corner starts a single run

TheoremSouth-then-east corner at the lowest vertices#✓fully proved

A closed walk without right turns has a south-then-east corner at one of its lowest vertices.

theorem ymin_SE_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) :
    ∃ m : Fin n, d (m - 1) = 3 ∧ d m = 0 ∧
      (∀ j : Fin n, (pos d m).2 ≤ (pos d j).2)

Uses 5

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

Proof usesBackward vertex recursion of a closed lattice walk · Forward vertex recursion of a closed lattice walk · Coordinates of the four lattice steps

TheoremPrevious and next vertices of a north-then-west corner#✓fully proved

At a north-then-west corner M, the previous vertex is just below and the next vertex just to the left.

theorem nw_corner_neighbours (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    {M : Fin n} (hin : d (M - 1) = 1) (hout : d M = 2) :
    pos d (M - 1) = pos d M + (0, -1) ∧ pos d (M + 1) = pos d M + (-1, 0)

Uses 4

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

Proof usesBackward vertex recursion of a closed lattice walk · Forward vertex recursion of a closed lattice walk

TheoremDistinct north-then-west corners sit at distinct vertices#✓fully proved

In a simple walk, distinct north-then-west corners sit at distinct vertices.

theorem nw_corners_distinct_pos (d : Fin n → Fin 4) (hsimple : Function.Injective (pos d))
    {i j : Fin n} (hij : i ≠ j)
    (_hi : d i = 1) (_hi2 : d (i + 1) = 2) (_hj : d j = 1) (_hj2 : d (j + 1) = 2) :
    pos d (i + 1) ≠ pos d (j + 1)

Uses 1

Statement usesVertices of a lattice walk from its step directions

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.