Interior cells have connected lower-left corners to A simple closed walk without right turns has under eight left turns

TheoremInterior cells have connected lower-left corners#✓fully proved

Any two interior cells of a simple closed walk without right turns have skeleton-connected lower-left corners.

theorem interior_representatives_reachable {m : ℕ}
    (d : Fin (m + 3) → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (BaseCase.pos d))
    (hreflexfree : ∀ i : Fin (m + 3), d (i + 1) - d i = 0 ∨ d (i + 1) - d i = 1)
    (c e : interiorCells d hclosed hsimple hreflexfree) :
    (cellSkeleton (interiorCells d hclosed hsimple hreflexfree)).Reachable
      (skeletonRepresentative _ c) (skeletonRepresentative _ e)

Uses 20 · Used by 1

Statement usesLattice point as a vertex of the cell complex · Vertices of a union of unit cells · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · 1-skeleton of a cell complex · Lower-left corner of a cell as a skeleton vertex · Cells of the bounded face of a simple closed walk

Proof usesUnit cell of the plane · Corners of a unit cell · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Image of a planar lattice subgraph in the square lattice · Primal edge shared by adjacent faces · Adjacent cells have connected lower-left corners · Corner of a cell as a skeleton vertex · Unit cell as a face of the square lattice · Inner component of the face graph · Membership in the bounded face · Simple closed walk as a planar subgraph · Face graph of a closed walk

Used byConnectedness of the skeleton of the interior

TheoremConnectedness of the skeleton of the interior#✓fully proved

The skeleton of the interior of a simple closed walk without right turns is connected.

theorem interior_cellSkeleton_connected {m : ℕ}
    (d : Fin (m + 3) → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (pos d))
    (hreflexfree : ∀ i : Fin (m + 3), d (i + 1) - d i = 0 ∨ d (i + 1) - d i = 1) :
    (cellSkeleton (interiorCells d hclosed hsimple hreflexfree)).Connected

Uses 13 · Used by 1

Statement usesLattice point as a vertex of the cell complex · Vertices of a union of unit cells · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · 1-skeleton of a cell complex · Cells of the bounded face of a simple closed walk

Proof usesUnit cell of the plane · Corners of a unit cell · Cell corners are connected to the lower-left corner · Interior cells have connected lower-left corners · Lower-left corner of a cell as a skeleton vertex · Cell to the left of a walk step · Every left cell lies in the bounded face

Used byInterior of a simple closed walk has Euler characteristic at most 1

TheoremInterior of a simple closed walk has Euler characteristic at most 1#✓fully proved

The interior of a simple closed walk without right turns has Euler characteristic at most 1.

theorem eulerChar_interiorCells_le_one {m : ℕ}
    (d : Fin (m + 3) → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (pos d))
    (hreflexfree : ∀ i : Fin (m + 3), d (i + 1) - d i = 0 ∨ d (i + 1) - d i = 1) :
    eulerChar (interiorCells d hclosed hsimple hreflexfree) ≤ 1

Uses 6 · Used by 1

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Euler characteristic of a cell complex · Cells of the bounded face of a simple closed walk

Proof usesEuler characteristic at most 1 for a connected skeleton · Connectedness of the skeleton of the interior

Used byDiscrete Umlaufsatz for walks of length at least three, shifted form

TheoremHopf's Umlaufsatz#✓fully proved

Hopf's Umlaufsatz for lattice polygons. A simple closed walk in ℤ² with at least three steps and no U-turns has total turning ±4 quarter turns, that is rotation index ±1 (H. Hopf, Über die Drehung der Tangenten und Sehnen ebener Kurven, 1935).

theorem turnSum_eq_four_or_neg_four (d : Fin n → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d))
    (hn : 3 ≤ n) (hnu : ∀ i, d (i + 1) ≠ d i + 2) :
    (∑ i, ons_turnPow (d i) (d (i + 1))) = 4 ∨
      (∑ i, ons_turnPow (d i) (d (i + 1))) = -4

Uses 84 · Used by 1

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Integer turn exponent between two directions

Proof usesUnit cell of the plane · Lattice point as a vertex of the cell complex · Sides of a unit cell · Corners of a unit cell · Euler characteristic of a union of unit cells · Edges of a union of unit cells · Vertices of a union of unit cells · Planar lattice subgraph of the square lattice · Site of the hypercubic lattice · Base point of the exterior of a box · Box \((-n, n)^d\) in the hypercubic lattice · Exterior of a box in \(\mathbb{Z}^d\) · Upper left corner of the unit face at \((a, b)\) · Lower right corner of the unit face at \((a, b)\) · Upper right corner of the unit face at \((a, b)\) · Every finite set of sites lies in a box · Hypercubic lattice \(\mathbb{Z}^d\) · Image of a planar lattice subgraph in the square lattice · Bounded regions of a planar lattice subgraph · Bounded regions indexed by the cycle rank · Cycle rank one gives a unique bounded region · Outer face region of a planar lattice subgraph · Cycle rank of a finite graph · Radius of a box containing a planar lattice subgraph · Setting a set of coordinates of a lattice site · Primal edge shared by adjacent faces · Face-region graph of a square-lattice subgraph · Corner count of a lattice point · Corner defect of a set of unit cells · Corner weight of a vertex · Euler characteristic of a cell complex · Agreement of the two Euler characteristics of a cell complex · Vertex count of the skeleton · 1-skeleton of a cell complex · Edges of the skeleton are the edges of the cell complex · 1-skeleton of a cell complex as a planar subgraph · Adjacent cells have connected lower-left corners · Cell corners are connected to the lower-left corner · Bounded face formed by a cell · Distinct cells form distinct bounded faces · Face component containing a cell · Lower-left corner of a cell as a skeleton vertex · Corner of a cell as a skeleton vertex · Cell Gauss–Bonnet formula · Pinch point of a set of unit cells · Number of pinch points · A simple closed walk traverses each horizontal segment at most once · A simple closed walk traverses each vertical segment at most once · Face-graph component of an interior cell · Finite set of interior cells of a closed walk · Interior cells by the even-odd rule · Finiteness of the interior of a closed walk · Subgraph of a simple closed lattice walk has cycle rank one · Ray-crossing parity of a lattice cell · Cells above a walk are outside · 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 · Forward vertex recursion of a closed lattice walk · 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 · Ray parity of the cell left of a step · Pinch count of the ray-parity interior is zero · Interior of a simple closed walk has no pinch points · An odd number of vertical steps flips the ray parity · Vertical steps separating two horizontal neighbour cells · Horizontal steps on a unit segment · An odd number of horizontal steps flips the ray parity · Straight steps of a simple closed walk carry no corner weight · Corner count of the interior counts inside cells around a point · Unit cell as a face of the square lattice · A face far outside the walk has ray parity zero · Face-adjacent cells have the same ray parity · Ray parity is constant on face-graph components · Simple closed walk as a planar subgraph · Face graph of a closed walk · Corner defect of the interior as a sum over walk vertices · Horizontal lattice direction · Vertical lattice direction

Used byOnsager's formula

TheoremAgreement of the two definitions of the left cell#✓fully proved

The two descriptions of the cell to the left of a step agree.

theorem leftCell_bridge (d : Fin (m + 3) → Fin 4) (k : Fin (m + 3)) :
    Orientation.leftCell (d k) (pos d k) = WalkCellBoundary.leftCell d k

Uses 3 · Used by 1

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

Used byA walk without right turns is positively oriented

TheoremA walk without right turns is positively oriented#✓fully proved

The cell to the left of the first step is inside: the walk is positively oriented.

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

Uses 8 · 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 · Agreement of the two definitions of the left cell · Cell to the left of a walk step · Every left cell has ray parity one

Used byDiscrete Umlaufsatz for walks of length at least three, shifted form

TheoremRay-parity interior equals the bounded face#✓fully proved

The ray-parity interior of a simple closed walk without right turns equals its bounded face.

theorem interiorCells_bridge (d : Fin (m + 3) → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (pos d))
    (hreflexfree : ∀ i : Fin (m + 3), d (i + 1) - d i = 0 ∨ d (i + 1) - d i = 1) :
    InteriorCells.interiorCells d hclosed
      = WalkCellRegion.interiorCells d hclosed hsimple hreflexfree

Uses 8 · Used by 1

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Finite set of interior cells of a closed walk · Cells of the bounded face of a simple closed walk

Proof usesInterior cells by the even-odd rule · Finiteness of the interior of a closed walk · Ray-crossing parity of a lattice cell · Lattice Jordan curve theorem, even-odd form

Used byDiscrete Umlaufsatz for walks of length at least three, shifted form

TheoremDiscrete Umlaufsatz for walks of length at least three, shifted form#✓fully proved

The discrete Umlaufsatz for walks of length m + 3 without right turns.

theorem cc_eq_four' (d : Fin (m + 3) → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (pos d))
    (hreflexfree : ∀ i : Fin (m + 3), d (i + 1) - d i = 0 ∨ d (i + 1) - d i = 1) :
    cc d = 4

Uses 16 · Used by 1

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 usesA closed walk without right turns has at least four left turns · Corner defect of a set of unit cells · Euler characteristic of a cell complex · Interior of a simple closed walk has Euler characteristic at most 1 · Cell Gauss–Bonnet formula · Number of pinch points · Finite set of interior cells of a closed walk · Corner defect of the interior is the number of left turns up to sign · Ray parity of the cell left of a step · Pinch count of the ray-parity interior is zero · Ray-parity interior equals the bounded face · A walk without right turns is positively oriented · Cells of the bounded face of a simple closed walk

Used byDiscrete Umlaufsatz for walks of length at least three

TheoremDiscrete Umlaufsatz for walks of length at least three#✓fully proved

The discrete Umlaufsatz for walks of length at least 3 without right turns.

theorem cc_eq_four {n : ℕ} [NeZero n] (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (pos d)) (hn : 3 ≤ n)
    (hreflexfree : ∀ i : Fin n, d (i + 1) - d i = 0 ∨ d (i + 1) - d i = 1) :
    cc d = 4

Uses 4 · Used by 1

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 usesDiscrete Umlaufsatz for walks of length at least three, shifted form

Used byDiscrete Umlaufsatz for lattice walks without right turns

TheoremA closed walk without right turns has length at least three#✓fully proved

A closed walk without right turns or reversals has length at least 3.

theorem three_le_n {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) : 3 ≤ n

Uses 1 · Used by 1

Statement usesUnit lattice step in a given direction

Used byDiscrete Umlaufsatz for lattice walks without right turns

TheoremDiscrete Umlaufsatz for lattice walks without right turns#✓fully proved

Discrete Umlaufsatz (theorem of turning tangents) for lattice walks without right turns: a simple closed walk on ℤ² whose every turn is straight or a left quarter turn has exactly four left turns, i.e. its direction makes one full counterclockwise revolution. Right turns and reversals are excluded by hypothesis, so the walks covered are exactly counterclockwise boundaries of lattice rectangles (no reflex corner); the general signed statement is StatMech.Onsager.GeneralUmlaufsatz.turnSum_eq_four_or_neg_four. Compare H. Hopf, Über die Drehung der Tangenten und Sehnen ebener Kurven, Compositio Math. 2 (1935), for smooth curves.

theorem cc_eq_four_of_no_right_turn {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) :
    cc d = 4

Uses 5 · Used by 1

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 usesDiscrete Umlaufsatz for walks of length at least three · A closed walk without right turns has length at least three

Used byA simple closed walk without right turns has under eight left turns

TheoremA simple closed walk without right turns has under eight left turns#✓fully proved

The hypothesis of StatMech.Onsager.BaseCase.base_cc_eq_four holds: a simple closed walk without right turns has fewer than eight left turns.

theorem hnodbl_discharged {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) :
    Function.Injective (pos d) → cc d < 8

Uses 4

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 usesDiscrete Umlaufsatz for lattice walks without right turns

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.