Vertical neighbours of different parity are separated by a horizontal step to Face-graph adjacency as absence of a walk step between cells

TheoremVertical neighbours of different parity are separated by a horizontal step#✓fully proved

If cells (a, b) and (a, b + 1) have different ray parities, a horizontal step separates them.

theorem mid_nonempty_of_ne (d : Fin n → Fin 4) (a b : ℤ)
    (h : rayParity d a b ≠ rayParity d a (b + 1)) : (midSet d a (b + 1)).Nonempty

Uses 5 · Used by 1

Statement usesRay-crossing parity of a lattice cell · Horizontal steps on a unit segment

Proof usesVertices of a lattice walk from its step directions · Ray parity is unchanged across a vertical move · Horizontal lattice direction

Used byInterior of a simple closed walk has no pinch points

TheoremInterior of a simple closed walk has no pinch points#✓fully proved

The interior of a simple closed walk has no pinch points.

theorem pinch_free (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (pos d)) (_hn : 3 ≤ n) (v : ℤ × ℤ) :
    ¬ pinchAt (interiorCells d hclosed) v

Uses 16 · Used by 2

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Pinch point of a set of unit cells · Finite set of interior cells of a closed walk

Proof usesSteps on a horizontal unit segment join its endpoints · Steps on a vertical unit segment join its endpoints · Interior cells by the even-odd rule · Finiteness of the interior of a closed walk · Ray-crossing parity of a lattice cell · Vertical neighbours of different parity are separated by a horizontal step · Horizontal neighbours of different parity are separated by a vertical step · Vertical steps separating two horizontal neighbour cells · Horizontal steps on a unit segment · A horizontal direction is not vertical · Horizontal lattice direction · Vertical lattice direction

Used byPinch count of the ray-parity interior is zero · Hopf's Umlaufsatz

TheoremPinch count of the ray-parity interior is zero#✓fully proved

The interior of a simple closed walk has pinch count 0. See also StatMech.Onsager.WalkCellLocal.pinchCount_interiorCells_eq_zero.

theorem pinchCount_eq_zero (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (pos d)) (hn : 3 ≤ n) :
    pinchCount (interiorCells d hclosed) = 0

Uses 8 · Used by 2

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Number of pinch points · Finite set of interior cells of a closed walk

Proof usesVertices of a cell complex · Pinch point of a set of unit cells · Pinch point indicator · Interior of a simple closed walk has no pinch points

Used byDiscrete Umlaufsatz for walks of length at least three, shifted form · Hopf's Umlaufsatz

TheoremZero corner weight of the interior off the walk#✓fully proved

A lattice point off the walk has corner weight 0 for the interior.

theorem cornerWeight_zero_of_notMem_image (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (vx vy : ℤ) (hnv : ∀ k : Fin n, pos d k ≠ (vx, vy)) :
    cornerWeight (cornerCount (interiorCells d hclosed) (vx, vy)) = 0

Uses 8 · Used by 1

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Corner count of a lattice point · Corner weight of a vertex · Finite set of interior cells of a closed walk

Proof usesRay-crossing parity of a lattice cell · Corner count of the interior counts inside cells around a point · Ray parity is constant around a non-vertex point

Used byCorner defect of the interior as a sum over walk vertices

TheoremCorner defect of the interior as a sum over walk vertices#✓fully proved

For a simple closed walk, the corner defect of the interior is the sum of the corner weights at the walk vertices.

theorem cornerDiff_interior_eq_walk_sum (d : Fin n → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    (hsimple : Function.Injective (pos d)) :
    cornerDiff (interiorCells d hclosed)
      = ∑ k : Fin n, cornerWeight (cornerCount (interiorCells d hclosed) (pos d k))

Uses 10 · Used by 2

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Corner count of a lattice point · Corner defect of a set of unit cells · Corner weight of a vertex · Finite set of interior cells of a closed walk

Proof usesVertices of a cell complex · A lattice point has an incident cell iff it is a vertex · Corner defect as a sum of vertex weights · Zero corner weight of the interior off the walk

Used byCorner defect of the interior is the number of left turns up to sign · Hopf's Umlaufsatz

TheoremCorner weights at the turns of a walk without right turns#✓fully proved

The corner weight of the interior at the vertex after step i is ±1 (sign given by the orientation) at a left turn and 0 at a straight step.

theorem cornerWeight_master (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) (i : Fin n) :
    cornerWeight (cornerCount (interiorCells d hclosed) (pos d (i + 1)))
      = (if leftParity d 0 = 1 then (1 : ℤ) else -1) * (if d (i + 1) - d i = 1 then 1 else 0)

Uses 14 · Used by 1

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Corner count of a lattice point · Corner weight of a vertex · Finite set of interior cells of a closed walk · Ray parity of the cell left of a step

Proof usesRay-crossing parity of a lattice cell · 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 · Unit cell to the left of a lattice step · Left parity is constant along a walk without right turns · Straight steps of a simple closed walk carry no corner weight

Used byCorner defect of the interior is the number of left turns up to sign

TheoremCorner defect of the interior is the number of left turns up to sign#✓fully proved

The corner defect of the interior equals ±cc d, the sign given by the orientation of the walk.

theorem cornerDiff_eq_weight_mul_cc (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) :
    cornerDiff (interiorCells d hclosed)
      = (if leftParity d 0 = 1 then (1 : ℤ) else -1) * (cc d : ℤ)

Uses 10 · Used by 2

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 · Corner defect of a set of unit cells · Finite set of interior cells of a closed walk · Ray parity of the cell left of a step

Proof usesCorner count of a lattice point · Corner weight of a vertex · Corner weights at the turns of a walk without right turns · Corner defect of the interior as a sum over walk vertices

Used byFour left turns from a pinch-free interior of Euler characteristic 1 · Discrete Umlaufsatz for walks of length at least three, shifted form

TheoremFour left turns from a pinch-free interior of Euler characteristic 1#✓fully proved

A simple closed walk without right turns whose interior is pinch-free with Euler characteristic 1 has four left turns.

theorem cc_eq_four (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)
    (hpinch : pinchCount (interiorCells d hclosed) = 0)
    (hchi : eulerChar (interiorCells d hclosed) = 1) :
    cc d = 4

Uses 11

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 · Euler characteristic of a cell complex · Number of pinch points · Finite set of interior cells of a closed walk

Proof usesA closed walk without right turns has at least four left turns · Corner defect of a set of unit cells · Cell Gauss–Bonnet formula · Corner defect of the interior is the number of left turns up to sign · Ray parity of the cell left of a step

DefinitionVertex of a walk as a lattice site#✓fully proved

The i-th vertex of the walk as a site of ℤ².

def posSite {m : ℕ} (d : Fin (m + 3) → Fin 4) (i : Fin (m + 3)) : Site 2 :=
  ![(pos d i).1, (pos d i).2]

Uses 2 · Used by 13

Statement usesSite of the hypercubic lattice · Vertices of a lattice walk from its step directions

Used byVertices of a simple walk are distinct sites · Consecutive walk vertices are adjacent in the square lattice · Simple closed walk as an embedded cycle graph · Neighbours in the image graph are walk predecessor and successor · Horizontally face-adjacent cells have the same ray parity · Vertically face-adjacent cells have the same ray parity · Each walk step is an edge of the image graph · Vertices of a walk's image graph are adjacent only to walk neighbours · Consecutive left cells on a straight step are face-adjacent · Left and right cells of a step share that step · Three walk edges cannot meet at a vertex · No right cell lies in the bounded face · Cells on either side of a step lie in different faces

TheoremVertices of a simple walk are distinct sites#✓fully proved

The vertices of a simple walk are distinct sites.

theorem posSite_injective {m : ℕ} (d : Fin (m + 3) → Fin 4)
    (hsimple : Function.Injective (pos d)) : Function.Injective (posSite d)

Uses 3 · Used by 2

Statement usesSite of the hypercubic lattice · Vertices of a lattice walk from its step directions · Vertex of a walk as a lattice site

Used bySimple closed walk as an embedded cycle graph · Neighbours in the image graph are walk predecessor and successor

TheoremEach lattice step has \(\ell^1\)-length one#✓fully proved

Each step has ℓ¹-length 1.

theorem stepOf_natAbs_sum (w : Fin 4) :
    (stepOf w).1.natAbs + (stepOf w).2.natAbs = 1

Uses 1 · Used by 1

Statement usesUnit lattice step in a given direction

Used byConsecutive walk vertices are adjacent in the square lattice

TheoremConsecutive walk vertices are adjacent in the square lattice#✓fully proved

Consecutive vertices of the walk are adjacent in the square lattice.

theorem walk_isSub {m : ℕ} (d : Fin (m + 3) → Fin 4) (hclosed : ∑ i, stepOf (d i) = 0)
    ⦃i j : Fin (m + 3)⦄ (hadj : (cycleGraph (m + 3)).Adj i j) :
    (hypercubicLattice 2).Adj (posSite d i) (posSite d j)

Uses 7 · Used by 1

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Unit lattice step in a given direction · Vertex of a walk as a lattice site

Proof usesVertices of a lattice walk from its step directions · Each lattice step has \(\ell^1\)-length one · Forward vertex recursion of a closed lattice walk

Used bySimple closed walk as an embedded cycle graph

DefinitionSimple closed walk as an embedded cycle graph#✓fully proved

A simple closed walk as a planar subgraph of ℤ²: the cycle graph cycleGraph (m + 3) embedded by its vertex positions.

noncomputable def walkSubgraph {m : ℕ} (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d)) :
    PlanarZ2Subgraph where
  V := Fin (m + 3)
  finV := inferInstance
  decV := inferInstance
  G := cycleGraph (m + 3)
  emb := ⟨posSite d, posSite_injective d hsimple⟩
  isSub := walk_isSub d hclosed

Uses 8 · Used by 5

Statement usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · 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

Used byFace-graph adjacency as absence of a walk step between cells · Ray-parity interior equals the bounded face components · Lattice Jordan curve theorem for simple closed walks · Subgraph of a simple closed lattice walk has cycle rank one · Simple closed walk as a planar subgraph

TheoremA cycle graph has one connected component#✓fully proved

A cycle graph has one connected component. A specialization of SimpleGraph.Preconnected.subsingleton_connectedComponent.

theorem cycleGraph_card_components_one (m : ℕ) :
    Nat.card (cycleGraph (m + 3)).ConnectedComponent = 1

Used by 1

Used byCycle graph has cycle rank one

TheoremNumber of edges of a cycle graph#✓fully proved

The cycle graph on m + 3 vertices has m + 3 edges.

theorem cycleGraph_card_edges (m : ℕ) :
    (cycleGraph (m + 3)).edgeSet.ncard = m + 3

Used by 1

Used byCycle graph has cycle rank one

TheoremCycle graph has cycle rank one#✓fully proved

The cycle graph has nullity (cycle rank) 1.

theorem cycle_nullity_one (m : ℕ) : nullity (cycleGraph (m + 3)) = 1

Uses 3 · Used by 1

Statement usesCycle rank of a finite graph

Proof usesA cycle graph has one connected component · Number of edges of a cycle graph

Used bySubgraph of a simple closed lattice walk has cycle rank one

TheoremSubgraph of a simple closed lattice walk has cycle rank one#✓fully proved

The planar subgraph of a simple closed walk has nullity 1.

theorem walkSubgraph_nullity_one {m : ℕ} (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d)) :
    nullity (walkSubgraph d hclosed hsimple).G = 1

Uses 6 · Used by 3

Statement usesPlanar lattice subgraph of the square lattice · Cycle rank of a finite graph · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · Simple closed walk as an embedded cycle graph

Proof usesCycle graph has cycle rank one

Used byLattice Jordan curve theorem for simple closed walks · Lattice Jordan curve theorem, even-odd form · Hopf's Umlaufsatz

TheoremLattice Jordan curve theorem for simple closed walks#✓fully proved

Lattice Jordan curve theorem for a simple closed walk: its complement in the face graph of ℤ² has exactly one bounded connected component.

theorem walk_one_bounded_region {m : ℕ} (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d)) :
    Nat.card {c : (whb_faceRegion (imageGraph (walkSubgraph d hclosed hsimple))).ConnectedComponent
      // c.supp.Finite} = 1

Uses 11

Statement usesSite of the hypercubic lattice · Image of a planar lattice subgraph in the square lattice · Face-region graph of a square-lattice subgraph · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · Simple closed walk as an embedded cycle graph

Proof usesPlanar lattice subgraph of the square lattice · Bounded faces of a finite lattice graph are counted by its cycle rank · Cycle rank of a finite graph · Faithful discrete Jordan statement for the face count · Subgraph of a simple closed lattice walk has cycle rank one

DefinitionRay-parity interior equals the bounded face components#✓fully proved

The ray-parity interior of the walk coincides with the union of bounded face components.

def BridgeParityMembership {m : ℕ} (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d)) : Prop :=
  ∀ a b : ℤ, rayParity d a b = 1 ↔
    ((whb_faceRegion (imageGraph (walkSubgraph d hclosed hsimple))).connectedComponentMk
      ![a, b]).supp.Finite

Uses 7

Statement usesSite of the hypercubic lattice · Image of a planar lattice subgraph in the square lattice · Face-region graph of a square-lattice subgraph · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · Simple closed walk as an embedded cycle graph · Ray-crossing parity of a lattice cell

DefinitionFace-graph adjacency as absence of a walk step between cells#✓fully proved

Adjacency in the face graph of the walk is the absence of a walk step on the common side of two cells.

def BridgeAdjacencyClimb {m : ℕ} (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d)) : Prop :=
  ∀ a b : ℤ,
    ((whb_faceRegion (imageGraph (walkSubgraph d hclosed hsimple))).Adj ![a, b] ![a + 1, b] ↔
      (∀ k : Fin (m + 3), 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)))) ∧
    ((whb_faceRegion (imageGraph (walkSubgraph d hclosed hsimple))).Adj ![a, b] ![a, b + 1] ↔
      (∀ k : Fin (m + 3), isHorizEdge (d k) →
        min ((pos d k).1) ((pos d (k + 1)).1) = a → (pos d k).2 ≠ b + 1))

Uses 8

Statement usesSite of the hypercubic lattice · Image of a planar lattice subgraph in the square lattice · Face-region graph of a square-lattice subgraph · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · Simple closed walk as an embedded cycle graph · Horizontal lattice direction · Vertical lattice direction

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.