Unit cell as a face of the square lattice to Membership in the bounded face

DefinitionUnit cell as a face of the square lattice#✓fully proved

The unit cell with lower-left corner p, viewed as a face of the square lattice, i.e. as the site ![p.1, p.2] of the dual lattice.

def cellFace : (ℤ × ℤ) ≃ Site 2 where
  toFun p := ![p.1, p.2]
  invFun z := (z 0, z 1)
  left_inv p := by ext <;> rfl
  right_inv z := by funext i; fin_cases i <;> rfl

Uses 1 · Used by 25

Statement usesSite of the hypercubic lattice

Used byCells of the inner face component · The inner component has finitely many cells · Face below-left of the inside top corner · Membership in the bounded face · 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 · 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 · 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 · 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 · Adjacent cells have connected lower-left corners · Distinct cells form distinct bounded faces · Face component containing a cell · The face component of a cell is bounded · The face of a cell is enclosed on all four sides · The face of a cell is alone in its component · Shared side of a cell and an adjacent face is an edge · Interior cells have connected lower-left corners · Hopf's Umlaufsatz

AbbreviationSimple closed walk as a planar subgraph#✓fully proved

A simple closed walk as a planar subgraph of ℤ².

noncomputable abbrev walkP (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d)) :
    PlanarZ2Subgraph := walkSubgraph d hclosed hsimple

Uses 4 · Used by 17

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

Used byNeighbours in the image graph are walk predecessor and successor · The inner face component is finite · 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 · Each walk step is an edge of the image graph · Face graph of a closed walk · Vertices of a walk's image graph are adjacent only to walk neighbours · Consecutive left cells on a straight step are face-adjacent · Lattice Jordan curve theorem, even-odd form · Bounded face of a simple closed walk has no pinch points · Three walk edges cannot meet at a vertex · A side between interior and exterior cells is a walk edge · Cells on either side of a step lie in different faces · Interior cells have connected lower-left corners · Hopf's Umlaufsatz

AbbreviationFace graph of a closed walk#✓fully proved

The face graph of the walk: adjacent faces of the square lattice whose common side is not an edge of the walk.

noncomputable abbrev walkRegionGraph (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d)) :
    SimpleGraph (Site 2) := whb_faceRegion (imageGraph (walkP d hclosed hsimple))

Uses 6 · Used by 18

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 a planar subgraph

Used byCells of the inner face component · The inner component has finitely many cells · Inner component of the face graph · The inner face component is finite · Membership in the bounded face · 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 · Consecutive left cells on a straight step are face-adjacent · Consecutive left cells have the same ray parity · Lattice Jordan curve theorem, even-odd form · Face-graph component of an interior cell · 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 · Interior cells have connected lower-left corners · Hopf's Umlaufsatz

TheoremEach walk step is an edge of the image graph#✓fully proved

Each step of the walk is an edge of its image graph.

theorem walkEdge_mem_imageGraph (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d))
    (k : Fin (m + 3)) :
    s(posSite d k, posSite d (k + 1)) ∈ (imageGraph (walkP d hclosed hsimple)).edgeSet

Uses 7 · Used by 4

Statement usesSite of the hypercubic lattice · Image of a planar lattice subgraph in the square lattice · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · Vertex of a walk as a lattice site · Simple closed walk as a planar subgraph

Proof usesPlanar lattice subgraph of the square lattice

Used byNeighbours 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 · Cells on either side of a step lie in different faces

TheoremNeighbours in the image graph are walk predecessor and successor#✓fully proved

In the image graph of a simple closed walk, the neighbours of a vertex are its predecessor and successor on the walk.

theorem imageGraph_adj_pos_iff (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d))
    (k : Fin (m + 3)) (q : Site 2) :
    (imageGraph (walkP d hclosed hsimple)).Adj (posSite d k) q ↔
      q = posSite d (k - 1) ∨ q = posSite d (k + 1)

Uses 9 · Used by 3

Statement usesSite of the hypercubic lattice · Image of a planar lattice subgraph in the square lattice · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · Vertex of a walk as a lattice site · Simple closed walk as a planar subgraph

Proof usesPlanar lattice subgraph of the square lattice · Vertices of a simple walk are distinct sites · Each walk step is an edge of the image graph

Used byVertices of a walk's image graph are adjacent only to walk neighbours · Consecutive left cells on a straight step are face-adjacent · Three walk edges cannot meet at a vertex

TheoremHorizontally face-adjacent cells have the same ray parity#✓fully proved

Horizontally adjacent cells joined in the face graph have the same ray parity.

theorem rayParity_eq_of_faceAdj_right (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d))
    (a b : ℤ)
    (hadj : (walkRegionGraph d hclosed hsimple).Adj (cellFace (a, b))
      (cellFace (a + 1, b))) :
    rayParity d a b = rayParity d (a + 1) b

Uses 19 · Used by 1

Statement usesSite of the hypercubic lattice · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · Ray-crossing parity of a lattice cell · Unit cell as a face of the square lattice · Face graph of a closed walk

Proof usesLower right corner of the unit face at \((a, b)\) · Upper right corner of the unit face at \((a, b)\) · Hypercubic lattice \(\mathbb{Z}^d\) · Image of a planar lattice subgraph in the square lattice · Primal edge shared by adjacent faces · Face-region graph of a square-lattice subgraph · Vertex of a walk as a lattice site · Ray parity is unchanged across a horizontal move · Each walk step is an edge of the image graph · Simple closed walk as a planar subgraph · Recursion for the x-coordinate of a walk step · Vertical lattice direction · Recursion for the y-coordinate of a walk step

Used byFace-adjacent cells have the same ray parity

TheoremVertically face-adjacent cells have the same ray parity#✓fully proved

Vertically adjacent cells joined in the face graph have the same ray parity.

theorem rayParity_eq_of_faceAdj_top (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d))
    (a b : ℤ)
    (hadj : (walkRegionGraph d hclosed hsimple).Adj (cellFace (a, b))
      (cellFace (a, b + 1))) :
    rayParity d a b = rayParity d a (b + 1)

Uses 19 · Used by 1

Statement usesSite of the hypercubic lattice · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · Ray-crossing parity of a lattice cell · Unit cell as a face of the square lattice · Face graph of a closed walk

Proof usesUpper left corner of the unit face at \((a, b)\) · Upper right corner of the unit face at \((a, b)\) · Hypercubic lattice \(\mathbb{Z}^d\) · Image of a planar lattice subgraph in the square lattice · Primal edge shared by adjacent faces · Face-region graph of a square-lattice subgraph · Vertex of a walk as a lattice site · Ray parity is unchanged across a vertical move · Each walk step is an edge of the image graph · Simple closed walk as a planar subgraph · Recursion for the x-coordinate of a walk step · Horizontal lattice direction · Recursion for the y-coordinate of a walk step

Used byFace-adjacent cells have the same ray parity

TheoremFace-adjacent cells have the same ray parity#✓fully proved

Cells adjacent in the face graph have the same ray parity.

theorem rayParity_eq_of_faceAdj (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d))
    {f g : Site 2} (hadj : (walkRegionGraph d hclosed hsimple).Adj f g) :
    rayParity d (f 0) (f 1) = rayParity d (g 0) (g 1)

Uses 12 · Used by 4

Statement usesSite of the hypercubic lattice · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · Ray-crossing parity of a lattice cell · Face graph of a closed walk

Proof usesHypercubic lattice \(\mathbb{Z}^d\) · Image of a planar lattice subgraph in the square lattice · Primal edge shared by adjacent faces · Unit cell as a face of the square lattice · Horizontally face-adjacent cells have the same ray parity · Vertically face-adjacent cells have the same ray parity · Simple closed walk as a planar subgraph

Used byRay parity is constant on face-graph components · Consecutive left cells have the same ray parity · A side between interior and exterior cells is a walk edge · Hopf's Umlaufsatz

TheoremRay parity is constant on face-graph components#✓fully proved

Ray parity is constant on connected components of the face graph.

theorem rayParity_eq_of_reachable (d : Fin (m + 3) → Fin 4)
    (hclosed : ∑ i, stepOf (d i) = 0) (hsimple : Function.Injective (pos d))
    {f g : Site 2} (hreach : (walkRegionGraph d hclosed hsimple).Reachable f g) :
    rayParity d (f 0) (f 1) = rayParity d (g 0) (g 1)

Uses 6 · Used by 3

Statement usesSite of the hypercubic lattice · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · Ray-crossing parity of a lattice cell · Face graph of a closed walk

Proof usesFace-adjacent cells have the same ray parity

Used byThe inner face component is finite · Lattice Jordan curve theorem, even-odd form · Hopf's Umlaufsatz

DefinitionTop corner with an inside cell below it#✓fully proved

A vertex M at which the walk turns from north to west and whose below-left cell is inside (chosen from StatMech.Onsager.InsideConnected.lexmax_corner_cell_inside).

noncomputable def lexInteriorIndex : Fin (m + 3) :=
  (lexmax_corner_cell_inside d hclosed hsimple hreflexfree).choose

Uses 4 · Used by 4

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Some north-then-west corner has its below-left cell inside · Ray-crossing parity of a lattice cell

Used byFace below-left of the inside top corner · The face below the inside top corner is inside · Defining property of the inside top corner · Every left cell has ray parity one

TheoremDefining property of the inside top corner#✓fully proved

The defining property of lexInteriorIndex.

theorem lexInteriorIndex_spec :
    d (lexInteriorIndex d hclosed hsimple hreflexfree - 1) = 1 ∧
      d (lexInteriorIndex d hclosed hsimple hreflexfree) = 2 ∧
      rayParity d
        ((pos d (lexInteriorIndex d hclosed hsimple hreflexfree)).1 - 1)
        ((pos d (lexInteriorIndex d hclosed hsimple hreflexfree)).2 - 1) = 1

Uses 5 · 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 · Top corner with an inside cell below it

Proof usesSome north-then-west corner has its below-left cell inside

Used byThe face below the inside top corner is inside · Every left cell has ray parity one

DefinitionFace below-left of the inside top corner#✓fully proved

The face of the cell below-left of the corner lexInteriorIndex.

noncomputable def lexInteriorFace : Site 2 :=
  cellFace
    ((pos d (lexInteriorIndex d hclosed hsimple hreflexfree)).1 - 1,
      (pos d (lexInteriorIndex d hclosed hsimple hreflexfree)).2 - 1)

Uses 5 · Used by 4

Statement usesSite of the hypercubic lattice · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · Unit cell as a face of the square lattice · Top corner with an inside cell below it

Used byInner component of the face graph · The inner face component is finite · The face below the inside top corner is inside · Lattice Jordan curve theorem, even-odd form

TheoremThe face below the inside top corner is inside#✓fully proved

The face lexInteriorFace is inside the walk.

theorem lexInteriorFace_parity :
    rayParity d (lexInteriorFace d hclosed hsimple hreflexfree 0)
      (lexInteriorFace d hclosed hsimple hreflexfree 1) = 1

Uses 6 · 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 · Face below-left of the inside top corner

Proof usesTop corner with an inside cell below it · Defining property of the inside top corner

Used byThe inner face component is finite · Lattice Jordan curve theorem, even-odd form

DefinitionInner component of the face graph#✓fully proved

The connected component of the face graph containing lexInteriorFace.

noncomputable def innerComponent :
    (walkRegionGraph d hclosed hsimple).ConnectedComponent :=
  (walkRegionGraph d hclosed hsimple).connectedComponentMk
    (lexInteriorFace d hclosed hsimple hreflexfree)

Uses 5 · Used by 7

Statement usesSite of the hypercubic lattice · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · Face below-left of the inside top corner · Face graph of a closed walk

Used byCells of the inner face component · The inner component has finitely many cells · The inner face component is finite · Membership in the bounded face · Lattice Jordan curve theorem, even-odd form · No right cell lies in the bounded face · Interior cells have connected lower-left corners

TheoremA face far outside the walk has ray parity zero#✓fully proved

A face far outside the bounding box of the walk has ray parity 0.

theorem outerBeacon_parity :
    rayParity d
      (beacon 2 (outerBoxRadius (walkP d hclosed hsimple) + 1) 0)
      (beacon 2 (outerBoxRadius (walkP d hclosed hsimple) + 1) 1) = 0

Uses 11 · Used by 3

Statement usesBase point of the exterior of a box · Radius of a box containing a planar lattice subgraph · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · Ray-crossing parity of a lattice cell · Simple closed walk as a planar subgraph

Proof usesPlanar lattice subgraph of the square lattice · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Every finite set of sites lies in a box · Cells above a walk are outside

Used byThe inner face component is finite · Lattice Jordan curve theorem, even-odd form · Hopf's Umlaufsatz

TheoremThe inner face component is finite#✓fully proved

The component innerComponent is bounded.

theorem innerComponent_finite :
    (innerComponent d hclosed hsimple hreflexfree).supp.Finite

Uses 23 · Used by 2

Statement usesSite of the hypercubic lattice · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · Inner component of the face graph · Face graph of a closed walk

Proof usesPlanar lattice subgraph of the square 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\) · Every finite set of sites lies in a box · Hypercubic lattice \(\mathbb{Z}^d\) · Image of a planar lattice subgraph in the square lattice · Outer face region of a planar lattice subgraph · 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 · Ray-crossing parity of a lattice cell · Face below-left of the inside top corner · The face below the inside top corner is inside · A face far outside the walk has ray parity zero · Ray parity is constant on face-graph components · Simple closed walk as a planar subgraph

Used byThe inner component has finitely many cells · Lattice Jordan curve theorem, even-odd form

DefinitionCells of the inner face component#✓fully proved

The cells whose faces lie in innerComponent.

def componentCellSet : Set (ℤ × ℤ) :=
  {p | cellFace p ∈ (innerComponent d hclosed hsimple hreflexfree).supp}

Uses 6 · Used by 3

Statement usesSite of the hypercubic lattice · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · Unit cell as a face of the square lattice · Inner component of the face graph · Face graph of a closed walk

Used byThe inner component has finitely many cells · Cells of the bounded face of a simple closed walk · Membership in the bounded face

TheoremThe inner component has finitely many cells#✓fully proved

There are finitely many such cells.

theorem componentCellSet_finite :
    (componentCellSet d hclosed hsimple hreflexfree).Finite

Uses 8 · Used by 2

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Cells of the inner face component

Proof usesSite of the hypercubic lattice · Unit cell as a face of the square lattice · Inner component of the face graph · The inner face component is finite · Face graph of a closed walk

Used byCells of the bounded face of a simple closed walk · Membership in the bounded face

DefinitionCells of the bounded face of a simple closed walk#✓fully proved

The cells of the bounded face of a simple closed walk without right turns. See also StatMech.Onsager.InteriorCells.interiorCells, the ray-parity interior; they agree by mem_interiorCells_iff_rayParity.

noncomputable def interiorCells : Finset (ℤ × ℤ) :=
  (componentCellSet_finite d hclosed hsimple hreflexfree).toFinset

Uses 4 · Used by 16

Statement usesVertices of a lattice walk from its step directions · Unit lattice step in a given direction · Cells of the inner face component · The inner component has finitely many cells

Used byMembership in the bounded face · Corner count of the bounded face at a walk vertex · Zero corner weight of the bounded face off the walk · Every left cell lies in the bounded face · Lattice Jordan curve theorem, even-odd form · Bounded face of a simple closed walk has no pinch points · Pinch count of the bounded face is zero · No right cell lies in the bounded face · A side between interior and exterior cells is a walk edge · 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 · Interior of a simple closed walk has Euler characteristic at most 1 · Connectedness of the skeleton of the interior · Ray-parity interior equals the bounded face · Interior cells have connected lower-left corners

TheoremMembership in the bounded face#✓fully proved

Membership in the bounded face.

@[simp] theorem mem_interiorCells (p : ℤ × ℤ) :
    p ∈ interiorCells d hclosed hsimple hreflexfree ↔
      cellFace p ∈ (innerComponent d hclosed hsimple hreflexfree).supp

Uses 9 · Used by 3

Statement usesSite of the hypercubic lattice · Vertices of a lattice walk from its step directions · Unit lattice step in a given direction · Unit cell as a face of the square lattice · Inner component of the face graph · Cells of the bounded face of a simple closed walk · Face graph of a closed walk

Proof usesCells of the inner face component · The inner component has finitely many cells

Used byLattice Jordan curve theorem, even-odd form · No right cell lies in the bounded face · Interior cells have connected lower-left corners

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.