Corner weight of the bounded face at a walk vertex to Lower-left corner of a cell as a skeleton vertex

TheoremCorner weight of the bounded face at a walk vertex#✓fully proved

The corner weight of the bounded face at the vertex after step k is 1 after a left turn and 0 after a straight step.

theorem cornerWeight_at_walkVertex (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)
    (k : Fin (m + 3)) :
    cornerWeight
        (cornerCount (interiorCells d hclosed hsimple hreflexfree) (pos d (k + 1))) =
      if d (k + 1) - d k = 1 then 1 else 0

Uses 6 · 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 · Cells of the bounded face of a simple closed walk

Proof usesCorner count of the bounded face at a walk vertex

Used byCorner defect of the bounded face equals the number of left turns

TheoremCorner defect of the bounded face equals the number of left turns#✓fully proved

The corner defect of the bounded face of a simple closed walk without right turns equals its number of left turns.

theorem cornerDiff_interiorCells_eq_cc (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) :
    cornerDiff (interiorCells d hclosed hsimple hreflexfree) = (cc d : ℤ)

Uses 12

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 · Cells of the bounded face of a simple closed walk

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

Definition1-skeleton of a cell complex#✓fully proved

The 1-skeleton of the cell complex S: vertices are the corners of cells, edges the sides of cells.

def cellSkeleton (S : Finset Cell) : SimpleGraph {v // v ∈ regVerts S} where
  Adj a b := s(a.1, b.1) ∈ StatMech.CellEulerChar.regEdges S
  symm := ⟨fun a b h => by rwa [Sym2.eq_swap]⟩
  loopless := ⟨by
    intro a h
    exact wad_edge_not_diag h (by simp)⟩

Uses 5 · Used by 8

Statement usesUnit cell of the plane · Lattice point as a vertex of the cell complex · Sides of a unit cell · Edges of a union of unit cells · Vertices of a union of unit cells

Used byAdjacent cells have connected lower-left corners · Edges of the skeleton are the edges of the cell complex · 1-skeleton of a cell complex as a planar subgraph · Cell corners are connected to the lower-left corner · Euler characteristic at most 1 for a connected skeleton · Connectedness of the skeleton of the interior · Interior cells have connected lower-left corners · Hopf's Umlaufsatz

Definition1-skeleton of a cell complex as a planar subgraph#✓fully proved

The 1-skeleton of S as a planar subgraph of ℤ².

StatMech.Onsager.CellEulerFaithful.cellSkeletonP · 23 lines

noncomputable def cellSkeletonP (S : Finset Cell) : PlanarZ2Subgraph where
  V := {v // v ∈ regVerts S}
  finV := inferInstance
  decV := inferInstance
  G := cellSkeleton S
  emb := ⟨fun v => ![v.1.1, v.1.2], by
    intro a b h
    apply Subtype.ext
    apply Prod.ext
    · exact congrFun h 0
    · exact congrFun h 1⟩
  isSub := by
    intro a b hab
    change s(a.1, b.1) ∈ StatMech.CellEulerChar.regEdges S at hab
    rw [StatMech.CellEulerChar.regEdges, Finset.mem_biUnion] at hab
    obtain ⟨c, _, he⟩ := hab
    obtain ⟨x, y⟩ := c
    simp only [StatMech.CellEulerChar.cellEdges, Finset.mem_insert, Finset.mem_singleton] at he
    rw [hypercubicLattice_adj, Fin.sum_univ_two]
    change (a.1.1 - b.1.1).natAbs + (a.1.2 - b.1.2).natAbs = 1
    rcases he with he | he | he | he <;> rw [Sym2.eq_iff] at he <;>
      rcases he with ⟨h1, h2⟩ | ⟨h1, h2⟩ <;>
      simp only [Prod.ext_iff] at h1 h2 <;> omega

Uses 9 · Used by 10

Statement usesUnit cell of the plane · Lattice point as a vertex of the cell complex · Sides of a unit cell · 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 · Hypercubic lattice \(\mathbb{Z}^d\) · 1-skeleton of a cell complex

Used byNumber of cells is at most the nullity of the skeleton · Euler characteristic at most 1 for a connected skeleton · Bounded face formed by a cell · 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 · Cell complex edges lie in the embedded skeleton · Hopf's Umlaufsatz

TheoremCell complex edges lie in the embedded skeleton#✓fully proved

An edge of the cell complex is an edge of the embedded skeleton.

theorem regEdge_mem_imageGraph (S : Finset Cell) {e : Sym2 Vtx}
    (he : e ∈ StatMech.CellEulerChar.regEdges S) :
    Sym2.map (fun v : Vtx => ![v.1, v.2]) e ∈ (imageGraph (cellSkeletonP S)).edgeSet

Uses 10 · Used by 1

Statement usesUnit cell of the plane · Lattice point as a vertex of the cell complex · Edges of a union of unit cells · Site of the hypercubic lattice · Image of a planar lattice subgraph in the square lattice · 1-skeleton of a cell complex as a planar subgraph

Proof usesSides of a unit cell · Corners of a unit cell · Vertices of a union of unit cells · Planar lattice subgraph of the square lattice

Used byThe face of a cell is enclosed on all four sides

TheoremShared side of a cell and an adjacent face is an edge#✓fully proved

The side shared by a cell of S and an adjacent face is an edge of S.

theorem sharedPrimalEdge_mem_regEdges (S : Finset Cell) (c : Cell) (hc : c ∈ S)
    (g : Site 2) (hlat : (hypercubicLattice 2).Adj (cellFace c) g) :
    Sym2.map cellFace.symm (sharedPrimalEdge (cellFace c) g) ∈
      StatMech.CellEulerChar.regEdges S

Uses 12 · Used by 2

Statement usesUnit cell of the plane · Lattice point as a vertex of the cell complex · Edges of a union of unit cells · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Primal edge shared by adjacent faces · Unit cell as a face of the square lattice

Proof usesSides of a unit cell · Lower left corner of the unit face at \((a, b)\) · 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)\)

Used byAdjacent cells have connected lower-left corners · The face of a cell is enclosed on all four sides

TheoremThe face of a cell is enclosed on all four sides#✓fully proved

The face of a cell of S is enclosed by the skeleton on all four sides.

theorem occupiedFace_isolated (S : Finset Cell) (c : Cell) (hc : c ∈ S) (g : Site 2) :
    ¬ (whb_faceRegion (imageGraph (cellSkeletonP S))).Adj (cellFace c) g

Uses 12 · Used by 1

Statement usesUnit cell of the plane · Site of the hypercubic lattice · Image of a planar lattice subgraph in the square lattice · Face-region graph of a square-lattice subgraph · 1-skeleton of a cell complex as a planar subgraph · Unit cell as a face of the square lattice

Proof usesLattice point as a vertex of the cell complex · Edges of a union of unit cells · Hypercubic lattice \(\mathbb{Z}^d\) · Primal edge shared by adjacent faces · Cell complex edges lie in the embedded skeleton · Shared side of a cell and an adjacent face is an edge

Used byThe face of a cell is alone in its component

DefinitionFace component containing a cell#✓fully proved

The face component of the skeleton containing the cell c.

noncomputable def occupiedComponent (S : Finset Cell) (c : Cell) :
    (whb_faceRegion (imageGraph (cellSkeletonP S))).ConnectedComponent :=
  (whb_faceRegion (imageGraph (cellSkeletonP S))).connectedComponentMk (cellFace c)

Uses 6 · Used by 4

Statement usesUnit cell of the plane · Site of the hypercubic lattice · Image of a planar lattice subgraph in the square lattice · Face-region graph of a square-lattice subgraph · 1-skeleton of a cell complex as a planar subgraph · Unit cell as a face of the square lattice

Used byBounded face formed by a cell · Distinct cells form distinct bounded faces · The face component of a cell is bounded · Hopf's Umlaufsatz

TheoremThe face of a cell is alone in its component#✓fully proved

The face of a cell of S is alone in its face component.

theorem occupiedFace_reachable_eq (S : Finset Cell) (c : Cell) (hc : c ∈ S) (g : Site 2)
    (hreach : (whb_faceRegion (imageGraph (cellSkeletonP S))).Reachable (cellFace c) g) :
    g = cellFace c

Uses 7 · Used by 2

Statement usesUnit cell of the plane · Site of the hypercubic lattice · Image of a planar lattice subgraph in the square lattice · Face-region graph of a square-lattice subgraph · 1-skeleton of a cell complex as a planar subgraph · Unit cell as a face of the square lattice

Proof usesThe face of a cell is enclosed on all four sides

Used byDistinct cells form distinct bounded faces · The face component of a cell is bounded

TheoremThe face component of a cell is bounded#✓fully proved

The face component of a cell of S is bounded.

theorem occupiedComponent_finite (S : Finset Cell) (c : Cell) (hc : c ∈ S) :
    (occupiedComponent S c).supp.Finite

Uses 8 · Used by 1

Statement usesUnit cell of the plane · Site of the hypercubic lattice · Image of a planar lattice subgraph in the square lattice · Face-region graph of a square-lattice subgraph · 1-skeleton of a cell complex as a planar subgraph · Face component containing a cell

Proof usesThe face of a cell is alone in its component · Unit cell as a face of the square lattice

Used byBounded face formed by a cell

DefinitionBounded face formed by a cell#✓fully proved

The bounded face of the skeleton formed by a cell of S.

noncomputable def occupiedBoundedFace (S : Finset Cell) (c : S) :
    jcb_BoundedRegion (cellSkeletonP S) :=
  ⟨occupiedComponent S c.1, occupiedComponent_finite S c.1 c.2⟩

Uses 8 · Used by 3

Statement usesUnit cell of the plane · Site of the hypercubic lattice · Image of a planar lattice subgraph in the square lattice · Bounded regions of a planar lattice subgraph · Face-region graph of a square-lattice subgraph · 1-skeleton of a cell complex as a planar subgraph · Face component containing a cell · The face component of a cell is bounded

Used byNumber of cells is at most the nullity of the skeleton · Distinct cells form distinct bounded faces · Hopf's Umlaufsatz

TheoremDistinct cells form distinct bounded faces#✓fully proved

Distinct cells form distinct bounded faces.

theorem occupiedBoundedFace_injective (S : Finset Cell) :
    Function.Injective (occupiedBoundedFace S)

Uses 10 · Used by 2

Statement usesUnit cell of the plane · Bounded regions of a planar lattice subgraph · 1-skeleton of a cell complex as a planar subgraph · Bounded face formed by a cell

Proof usesSite of the hypercubic lattice · Image of a planar lattice subgraph in the square lattice · Face-region graph of a square-lattice subgraph · Face component containing a cell · The face of a cell is alone in its component · Unit cell as a face of the square lattice

Used byNumber of cells is at most the nullity of the skeleton · Hopf's Umlaufsatz

TheoremNumber of cells is at most the nullity of the skeleton#✓fully proved

The number of cells is at most the nullity of the skeleton.

theorem card_le_cellSkeleton_nullity (S : Finset Cell) :
    S.card ≤ nullity (cellSkeletonP S).G

Uses 18 · Used by 1

Statement usesUnit cell of the plane · Planar lattice subgraph of the square lattice · Cycle rank of a finite graph · 1-skeleton of a cell complex as a planar subgraph

Proof usesSite 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\) · 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 · Setting a set of coordinates of a lattice site · Primal edge shared by adjacent faces · Face-region graph of a square-lattice subgraph · Bounded face formed by a cell · Distinct cells form distinct bounded faces

Used byEuler characteristic at most 1 for a connected skeleton

DefinitionEdges of the skeleton are the edges of the cell complex#✓fully proved

The edges of cellSkeleton S are the edges of the cell complex S.

noncomputable def cellSkeletonEdgeEquiv (S : Finset Cell) :
    {e // e ∈ (cellSkeleton S).edgeSet} ≃ {e // e ∈ StatMech.CellEulerChar.regEdges S} where
  toFun e := ⟨Sym2.map Subtype.val e.1, by
    exact (mem_cellSkeleton_edgeSet_iff S e.1).mp e.2⟩
  invFun e := ⟨e.1.attachWith (fun v hv => wad_edge_mem_regVerts e.2 hv), by
    rw [mem_cellSkeleton_edgeSet_iff]
    simpa only [Sym2.attachWith_map_subtypeVal] using e.2⟩
  left_inv e := by
    apply Subtype.ext
    apply Sym2.map.injective Subtype.val_injective
    simp only [Sym2.attachWith_map_subtypeVal]
  right_inv e := by
    apply Subtype.ext
    simp only [Sym2.attachWith_map_subtypeVal]

Uses 7 · Used by 2

Statement usesUnit cell of the plane · Lattice point as a vertex of the cell complex · Sides of a unit cell · Corners of a unit cell · Edges of a union of unit cells · Vertices of a union of unit cells · 1-skeleton of a cell complex

Used byEuler characteristic at most 1 for a connected skeleton · Hopf's Umlaufsatz

TheoremVertex count of the skeleton#✓fully proved

The skeleton has (regVerts S).card vertices.

theorem card_cellSkeleton_vertices (S : Finset Cell) :
    Nat.card {v // v ∈ regVerts S} = (regVerts S).card

Uses 3 · Used by 2

Statement usesUnit cell of the plane · Lattice point as a vertex of the cell complex · Vertices of a union of unit cells

Used byEuler characteristic at most 1 for a connected skeleton · Hopf's Umlaufsatz

TheoremEuler characteristic at most 1 for a connected skeleton#✓fully proved

If the 1-skeleton of S is connected, then eulerChar S ≤ 1. See also StatMech.Onsager.CellEulerBound.eulerChar_le_one.

theorem eulerChar_le_one_of_skeleton_connected (S : Finset Cell)
    (hconn : (cellSkeleton S).Connected) : eulerChar S ≤ 1

Uses 14 · Used by 1

Statement usesUnit cell of the plane · Lattice point as a vertex of the cell complex · Vertices of a union of unit cells · Euler characteristic of a cell complex · 1-skeleton of a cell complex

Proof usesEuler characteristic of a union of unit cells · Edges of a union of unit cells · Planar lattice subgraph of the square lattice · Cycle rank of a finite graph · Agreement of the two Euler characteristics of a cell complex · Vertex count of the skeleton · Number of cells is at most the nullity of the skeleton · Edges of the skeleton are the edges of the cell complex · 1-skeleton of a cell complex as a planar subgraph

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

DefinitionCorner of a cell as a skeleton vertex#✓fully proved

A corner of a cell of S, as a vertex of the skeleton.

def skeletonVertexOfCorner (S : Finset Cell) (c : Cell) (hc : c ∈ S)
    (v : Vtx) (hv : v ∈ StatMech.CellEulerChar.cellVerts c) : {v // v ∈ regVerts S} :=
  ⟨v, wad_cellVerts_subset_regVerts hc hv⟩

Uses 4 · Used by 5

Statement usesUnit cell of the plane · Lattice point as a vertex of the cell complex · Corners of a unit cell · Vertices of a union of unit cells

Used byAdjacent cells have connected lower-left corners · Cell corners are connected to the lower-left corner · Lower-left corner of a cell as a skeleton vertex · Interior cells have connected lower-left corners · Hopf's Umlaufsatz

TheoremCell corners are connected to the lower-left corner#✓fully proved

Every corner of a cell is connected in the skeleton to its lower-left corner.

theorem corner_reachable_lowerLeft (S : Finset Cell) (c : Cell) (hc : c ∈ S)
    (v : Vtx) (hv : v ∈ StatMech.CellEulerChar.cellVerts c) :
    (cellSkeleton S).Reachable (skeletonVertexOfCorner S c hc v hv)
      (skeletonVertexOfCorner S c hc c (by
        obtain ⟨x, y⟩ := c
        simp [StatMech.CellEulerChar.cellVerts]))

Uses 8 · Used by 3

Statement usesUnit cell of the plane · Lattice point as a vertex of the cell complex · Corners of a unit cell · Vertices of a union of unit cells · 1-skeleton of a cell complex · Corner of a cell as a skeleton vertex

Proof usesSides of a unit cell · Edges of a union of unit cells

Used byAdjacent cells have connected lower-left corners · Connectedness of the skeleton of the interior · Hopf's Umlaufsatz

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

The lower-left corners of two adjacent cells of S are connected in the skeleton.

theorem cell_representatives_reachable_of_adj (S : Finset Cell) (c d : Cell)
    (hc : c ∈ S) (hd : d ∈ S)
    (hadj : (hypercubicLattice 2).Adj (cellFace c) (cellFace d)) :
    (cellSkeleton S).Reachable
      (skeletonVertexOfCorner S c hc c (by
        obtain ⟨x, y⟩ := c; simp [StatMech.CellEulerChar.cellVerts]))
      (skeletonVertexOfCorner S d hd d (by
        obtain ⟨x, y⟩ := d; simp [StatMech.CellEulerChar.cellVerts]))

Uses 14 · Used by 2

Statement usesUnit cell of the plane · Lattice point as a vertex of the cell complex · Corners of a unit cell · Vertices of a union of unit cells · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · 1-skeleton of a cell complex · Corner of a cell as a skeleton vertex · Unit cell as a face of the square lattice

Proof usesSides of a unit cell · Edges of a union of unit cells · Primal edge shared by adjacent faces · Cell corners are connected to the lower-left corner · Shared side of a cell and an adjacent face is an edge

Used byInterior cells have connected lower-left corners · Hopf's Umlaufsatz

DefinitionLower-left corner of a cell as a skeleton vertex#✓fully proved

The lower-left corner of a cell of S, as a vertex of the skeleton.

def skeletonRepresentative (S : Finset Cell) (c : S) : {v // v ∈ regVerts S} :=
  skeletonVertexOfCorner S c.1 c.2 c.1 (by
    obtain ⟨x, y⟩ := c.1
    simp [StatMech.CellEulerChar.cellVerts])

Uses 5 · Used by 3

Statement usesUnit cell of the plane · Lattice point as a vertex of the cell complex · Corners of a unit cell · Vertices of a union of unit cells · Corner of a cell as a skeleton vertex

Used byConnectedness of the skeleton of the interior · Interior cells have connected lower-left corners · Hopf's Umlaufsatz

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.