Steps on a horizontal unit segment join its endpoints to A closed walk crosses each vertical line an even number of times

TheoremSteps on a horizontal unit segment join its endpoints#✓fully proved

A step on the horizontal segment [a, a + 1] × {b} goes from one endpoint to the other.

theorem midSet_endpoints (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) (a b : ℤ)
    (k : Fin n) (hk : k ∈ midSet d a b) :
    (pos d k = (a, b) ∧ pos d (k + 1) = (a + 1, b))
      ∨ (pos d k = (a + 1, b) ∧ pos d (k + 1) = (a, b))

Uses 6 · Used by 2

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

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

Used byA simple closed walk traverses each horizontal segment at most once · Interior of a simple closed walk has no pinch points

TheoremSteps on a vertical unit segment join its endpoints#✓fully proved

A step on the vertical segment {a + 1} × [b, b + 1] goes from one endpoint to the other.

theorem straddleSet_endpoints (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) (a b : ℤ)
    (k : Fin n) (hk : k ∈ straddleSet d a b) :
    (pos d k = (a + 1, b) ∧ pos d (k + 1) = (a + 1, b + 1))
      ∨ (pos d k = (a + 1, b + 1) ∧ pos d (k + 1) = (a + 1, b))

Uses 6 · Used by 2

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

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

Used byA simple closed walk traverses each vertical segment at most once · Interior of a simple closed walk has no pinch points

TheoremA simple closed walk traverses each horizontal segment at most once#✓fully proved

A simple closed walk traverses each horizontal unit segment at most once.

theorem midSet_card_le_one (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (pos d)) (hn : 3 ≤ n) (a b : ℤ) :
    (midSet d a b).card ≤ 1

Uses 5 · Used by 4

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

Proof usesSteps on a horizontal unit segment join its endpoints · \(k + 2 \ne k\) in \(\mathrm{Fin}\, n\) for \(n \ge 3\)

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

TheoremA simple closed walk traverses each vertical segment at most once#✓fully proved

A simple closed walk traverses each vertical unit segment at most once.

theorem straddleSet_card_le_one (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (pos d)) (hn : 3 ≤ n) (a b : ℤ) :
    (straddleSet d a b).card ≤ 1

Uses 5 · Used by 5

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

Proof uses\(k + 2 \ne k\) in \(\mathrm{Fin}\, n\) for \(n \ge 3\) · Steps on a vertical unit segment join its endpoints

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

TheoremSome north-then-west corner has its below-left cell inside#✓fully proved

A simple closed walk without right turns has a north-then-west corner M whose below-left cell ((pos d M).1 - 1, (pos d M).2 - 1) has ray parity 1.

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

Uses 10 · 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 usesUpward ray crossings above a cell · Backward vertex recursion of a closed lattice walk · Forward vertex recursion of a closed lattice walk · Coordinates 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 byTop corner with an inside cell below it · Defining property of the inside top corner

TheoremNo north step leaves a highest vertex#✓fully proved

No north step leaves a vertex of maximal height.

theorem top_out_ne_N (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    {M v : Fin n} (hmax : ∀ j : Fin n, (pos d j).2 ≤ (pos d M).2)
    (hv : (pos d v).2 = (pos d M).2) :
    d v ≠ 1

Uses 3 · Used by 1

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 walk step

Used byA north step into a highest vertex is followed by a west step

TheoremNo south step arrives at a highest vertex#✓fully proved

No south step arrives at a vertex of maximal height.

theorem top_in_ne_S (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    {M v : Fin n} (hmax : ∀ j : Fin n, (pos d j).2 ≤ (pos d M).2)
    (hv : (pos d v).2 = (pos d M).2) :
    d (v - 1) ≠ 3

Uses 3

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

TheoremPosition after a run of west steps#✓fully proved

After j consecutive west steps from vertex M, the walk is j units to the left of M at the same height.

theorem forward_west_run (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) (M : Fin n)
    (j : ℕ) (hj : ∀ i : ℕ, i < j → d (M + (Nat.cast i : Fin n)) = 2) :
    pos d (M + (Nat.cast j : Fin n)) = ((pos d M).1 - (j : ℤ), (pos d M).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 byA west run from a highest vertex ends in a south step · A single top run makes the top row contiguous

DefinitionSingle west run covering the top row#✓fully proved

Every vertex of the walk at the height of M is reached from M by a run of consecutive west steps.

def SingleTopRun (d : Fin n → Fin 4) (M : Fin n) : Prop :=
  ∀ v : Fin n, (pos d v).2 = (pos d M).2 →
    ∃ j : ℕ, (∀ i : ℕ, i < j → d (M + (Nat.cast i : Fin n)) = 2) ∧
      (pos d v).1 = (pos d M).1 - (j : ℤ)

Uses 1 · Used by 3

Statement usesVertices of a lattice walk from its step directions

Used byA west run covering the top row is a single top run · Top row is contiguous when every top corner starts a single run · A single top run makes the top row contiguous

TheoremA single top run makes the top row contiguous#✓fully proved

If the top row is covered by a single west run from a highest vertex, it is contiguous.

theorem topRowContiguous_of_singleTopRun (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    {M : Fin n} (hmax : ∀ j : Fin n, (pos d j).2 ≤ (pos d M).2)
    (hrun : SingleTopRun d M) :
    StatMech.Onsager.UmlaufsatzStrip.TopRowContiguous d

Uses 5 · Used by 1

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Single west run covering the top row · Contiguous top row of a walk

Proof usesPosition after a run of west steps

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

TheoremTop row is contiguous when every top corner starts a single run#✓fully proved

If every highest north-then-west corner starts a single top run, the top row is contiguous.

theorem topRowContiguous_of_residue (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)
    (hres : ∀ M : Fin n, d (M - 1) = 1 → d M = 2 →
      (∀ j : Fin n, (pos d j).2 ≤ (pos d M).2) → SingleTopRun d M) :
    StatMech.Onsager.UmlaufsatzStrip.TopRowContiguous d

Uses 6

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Single west run covering the top row · Contiguous top row of a walk

Proof usesA single top run makes the top row contiguous · North-then-west corner at the highest vertices

TheoremA north step into a highest vertex is followed by a west step#✓fully proved

In a closed walk without right turns, a north step arriving at a highest vertex is followed by a west step.

theorem top_arrival_west (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 v : Fin n} (hmax : ∀ j : Fin n, (pos d j).2 ≤ (pos d M).2)
    (hv : (pos d v).2 = (pos d M).2) (harr : d (v - 1) = 1) :
    d v = 2

Uses 3

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

Proof usesNo north step leaves a highest vertex

TheoremA west step on the top row is followed by west or south#✓fully proved

A west step on the top row is followed by a west or a south step, and stays on the top row.

theorem top_west_next (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 v : Fin n} (_hmax : ∀ j : Fin n, (pos d j).2 ≤ (pos d M).2)
    (hv : (pos d v).2 = (pos d M).2) (hw : d v = 2) :
    (pos d (v + 1)).2 = (pos d M).2 ∧ (d (v + 1) = 2 ∨ d (v + 1) = 3)

Uses 4 · Used by 1

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

Proof usesHorizontal lattice direction · Recursion for the y-coordinate of a walk step

Used byA west run from a highest vertex ends in a south step

TheoremA closed walk is not all west steps#✓fully proved

A closed walk does not consist of west steps only.

theorem exists_step_ne_west (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0) (M : Fin n) :
    ∃ i : ℕ, d (M + (Nat.cast i : Fin n)) ≠ 2

Uses 1 · Used by 1

Statement usesUnit lattice step in a given direction

Used byA west run from a highest vertex ends in a south step

TheoremA west run from a highest vertex ends in a south step#✓fully proved

From a highest vertex where the walk turns west, it makes J ≥ 1 west steps and then a south step.

theorem exists_west_run_end (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) (hmax : ∀ j : Fin n, (pos d j).2 ≤ (pos d M).2) (hout : d M = 2) :
    ∃ J : ℕ, 1 ≤ J ∧ (∀ i : ℕ, i < J → d (M + (Nat.cast i : Fin n)) = 2) ∧
      d (M + (Nat.cast J : Fin n)) = 3

Uses 5

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

Proof usesA closed walk is not all west steps · A west step on the top row is followed by west or south · Position after a run of west steps

TheoremA west run covering the top row is a single top run#✓fully proved

A west run from M whose vertices cover the top row is a single top run.

theorem singleTopRun_of_runCoversTop (d : Fin n → Fin 4) (M : Fin n) (J : ℕ)
    (hrun : ∀ i : ℕ, i < J → d (M + (Nat.cast i : Fin n)) = 2)
    (hcover : ∀ v : Fin n, (pos d v).2 = (pos d M).2 →
      ∃ i : ℕ, i ≤ J ∧ (pos d v).1 = (pos d M).1 - (i : ℤ)) :
    StatMech.Onsager.TopRow.SingleTopRun d M

Uses 2

Statement usesVertices of a lattice walk from its step directions · Single west run covering the top row

TheoremA step changes the x-coordinate by at most one#✓fully proved

A step changes the x-coordinate by 0 or ±1.

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

Uses 3 · Used by 1

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 walk step

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

DefinitionNumber of crossings of a vertical line#✓fully proved

The number of horizontal steps of the walk crossing the vertical line x = m + 1/2.

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

Uses 2 · Used by 2

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

Used byA closed walk crosses each vertical line an even number of times · Cells below a walk are outside

TheoremA closed walk crosses a vertical line equally often left and right#✓fully proved

A walk crosses the line x = m + 1/2 to the right as often as to the left.

theorem leftRight_card_eq (d : Fin n → Fin 4) (m : ℤ) :
    (Finset.univ.filter
        (fun k : Fin n => (pos d k).1 ≤ m ∧ m + 1 ≤ (pos d (k + 1)).1)).card
      = (Finset.univ.filter
        (fun k : Fin n => m + 1 ≤ (pos d k).1 ∧ (pos d (k + 1)).1 ≤ m)).card

Uses 1 · Used by 1

Statement usesVertices of a lattice walk from its step directions

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

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

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

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

Uses 9 · Used by 1

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

Proof usesVertices of a lattice walk from its step directions · Coordinates of the four lattice steps · Recursion for the x-coordinate of a walk step · Horizontal lattice direction · Vertical lattice direction · A step changes the x-coordinate by at most one · A closed walk crosses a vertical line equally often left and right

Used byCells below a walk are outside

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.