Discrete Gauss–Bonnet formula for polyominoes

AbbreviationUnit cell of the plane#✓fully proved

A unit cell [a, a + 1] × [b, b + 1] of the plane, labelled by its lower left corner.

abbrev Cell := ℤ × ℤ
Used by 48
Used byAgreement of the two edge counts of a cell complex · Distinct cells have distinct top edges · Cell degree of a lattice vertex · Sides of a unit cell · Corners of a unit cell · Agreement of the two vertex sets of a cell complex · Angle defect at a lattice vertex · Edge degree of a lattice vertex · Cell regions built by attaching cells along boundary arcs · Agreement of the two Euler characteristics of a cell complex · Euler characteristic bound via the open-top skeleton · Edge codes of a unit cell are its doubled edge midpoints · Number of new sides added by a cell · Number of new corners added by a cell · Edges of the open-top skeleton · Open-top skeleton of a cell complex · Euler characteristic of a union of unit cells · Regular Euler characteristic bound via the open-top skeleton · Edges of a union of unit cells · Vertices of a union of unit cells · Edge count bound for a connected open-top skeleton · Four cells around a lattice vertex · Top edge of a unit cell · Top edges of a set of cells · Number of convex corners of a lattice region · Number of pinch points of a lattice region · Number of reflex corners of a lattice region · Vertex count of the skeleton · Number of cells is at most the nullity of the skeleton · Adjacent cells have connected lower-left corners · 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 · Cell corners are connected to the lower-left corner · 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 · Shared side of a cell and an adjacent face is an edge · Lower-left corner of a cell as a skeleton vertex · Corner of a cell as a skeleton vertex · Connectedness of the skeleton of the interior · Interior cells have connected lower-left corners · Hopf's Umlaufsatz

AbbreviationLattice point as a vertex of the cell complex#✓fully proved

A lattice point of ℤ², used as a vertex of the cell complex.

abbrev Vtx := ℤ × ℤ
Used by 45
Used byAgreement of the two edge counts of a cell complex · Distinct cells have distinct top edges · Cell degree of a lattice vertex · Sides of a unit cell · Corners of a unit cell · Agreement of the two vertex sets of a cell complex · Angle defect at a lattice vertex · Edge degree of a lattice vertex · Agreement of the two Euler characteristics of a cell complex · Euler characteristic bound via the open-top skeleton · Edge codes of a unit cell are its doubled edge midpoints · Lattice edge to the lower neighbour · Lattice edge to the left neighbour · Lattice edge to the right neighbour · Lattice edge to the upper neighbour · Number of new sides added by a cell · Number of new corners added by a cell · Edges of the open-top skeleton · Open-top skeleton of a cell complex · Euler characteristic of a union of unit cells · Regular Euler characteristic bound via the open-top skeleton · Edges of a union of unit cells · Vertices of a union of unit cells · Edge count bound for a connected open-top skeleton · Four cells around a lattice vertex · Top edge of a unit cell · Top edges of a set of cells · Number of convex corners of a lattice region · Number of pinch points of a lattice region · Number of reflex corners of a lattice region · Vertex count of the skeleton · Adjacent cells have connected lower-left corners · 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 · Cell corners are connected to the lower-left corner · Euler characteristic at most 1 for a connected skeleton · The face of a cell is enclosed on all four sides · Cell complex edges lie in the embedded skeleton · Shared side of a cell and an adjacent face is an edge · Lower-left corner of a cell as a skeleton vertex · Corner of a cell as a skeleton vertex · Connectedness of the skeleton of the interior · Interior cells have connected lower-left corners · Hopf's Umlaufsatz

DefinitionCorners of a unit cell#✓fully proved

The four corners of a unit cell.

def cellVerts (c : Cell) : Finset Vtx :=
  {(c.1, c.2), (c.1 + 1, c.2), (c.1, c.2 + 1), (c.1 + 1, c.2 + 1)}
Uses 2 · Used by 13
Statement usesUnit cell of the plane · Lattice point as a vertex of the cell complex
Used byAgreement of the two vertex sets of a cell complex · Number of new corners added by a cell · Edges of the open-top skeleton · Vertices of a union of unit cells · Adjacent cells have connected lower-left corners · Edges of the skeleton are the edges of the cell complex · Cell corners are connected to the lower-left corner · Cell complex edges lie in the embedded skeleton · Lower-left corner of a cell as a skeleton vertex · Corner of a cell as a skeleton vertex · Connectedness of the skeleton of the interior · Interior cells have connected lower-left corners · Hopf's Umlaufsatz

DefinitionSides of a unit cell#✓fully proved

The four sides of a unit cell, as unordered pairs of corners.

def cellEdges (c : Cell) : Finset (Sym2 Vtx) :=
  { s((c.1, c.2), (c.1 + 1, c.2)),
    s((c.1, c.2 + 1), (c.1 + 1, c.2 + 1)),
    s((c.1, c.2), (c.1, c.2 + 1)),
    s((c.1 + 1, c.2), (c.1 + 1, c.2 + 1)) }
Uses 2 · Used by 15
Statement usesUnit cell of the plane · Lattice point as a vertex of the cell complex
Used byAgreement of the two edge counts of a cell complex · Edge codes of a unit cell are its doubled edge midpoints · Number of new sides added by a cell · Edges of the open-top skeleton · Open-top skeleton of a cell complex · Regular Euler characteristic bound via the open-top skeleton · Edges of a union of unit cells · Adjacent cells have connected lower-left corners · 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 · Cell corners are connected to the lower-left corner · Cell complex edges lie in the embedded skeleton · Shared side of a cell and an adjacent face is an edge · Hopf's Umlaufsatz

DefinitionVertices of a union of unit cells#✓fully proved

The vertices of the union of the cells in K.

def regVerts (K : Finset Cell) : Finset Vtx := K.biUnion cellVerts
Uses 3 · Used by 25
Statement usesUnit cell of the plane · Lattice point as a vertex of the cell complex · Corners of a unit cell
Used byAgreement of the two vertex sets of a cell complex · Agreement of the two Euler characteristics of a cell complex · Euler characteristic bound via the open-top skeleton · Number of new corners added by a cell · Edges of the open-top skeleton · Open-top skeleton of a cell complex · Euler characteristic of a union of unit cells · Regular Euler characteristic bound via the open-top skeleton · Edge count bound for a connected open-top skeleton · Number of convex corners of a lattice region · Number of pinch points of a lattice region · Number of reflex corners of a lattice region · Vertex count of the skeleton · Adjacent cells have connected lower-left corners · 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 · Cell corners are connected to the lower-left corner · Euler characteristic at most 1 for a connected skeleton · Cell complex edges lie in the embedded skeleton · Lower-left corner of a cell as a skeleton vertex · Corner of a cell as a skeleton vertex · Connectedness of the skeleton of the interior · Interior cells have connected lower-left corners · Hopf's Umlaufsatz

DefinitionEdges of a union of unit cells#✓fully proved

The edges of the union of the cells in K.

def regEdges (K : Finset Cell) : Finset (Sym2 Vtx) := K.biUnion cellEdges
Uses 3 · Used by 19
Statement usesUnit cell of the plane · Lattice point as a vertex of the cell complex · Sides of a unit cell
Used byAgreement of the two edge counts of a cell complex · Edge degree of a lattice vertex · Agreement of the two Euler characteristics of a cell complex · Number of new sides added by a cell · Edges of the open-top skeleton · Open-top skeleton of a cell complex · Euler characteristic of a union of unit cells · Regular Euler characteristic bound via the open-top skeleton · Edge count bound for a connected open-top skeleton · Adjacent cells have connected lower-left corners · 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 · Cell corners are connected to the lower-left corner · Euler characteristic at most 1 for a connected skeleton · The face of a cell is enclosed on all four sides · Cell complex edges lie in the embedded skeleton · Shared side of a cell and an adjacent face is an edge · Hopf's Umlaufsatz

DefinitionEuler characteristic of a union of unit cells#✓fully proved

The Euler characteristic V - E + F of the union of the cells in K, with one face per cell.

def regChi (K : Finset Cell) : ℤ :=
  (regVerts K).card - (regEdges K).card + K.card
Uses 4 · Used by 5
Statement usesUnit cell of the plane · Lattice point as a vertex of the cell complex · Edges of a union of unit cells · Vertices of a union of unit cells
Used byAgreement of the two Euler characteristics of a cell complex · Euler characteristic bound via the open-top skeleton · Regular Euler characteristic bound via the open-top skeleton · Euler characteristic at most 1 for a connected skeleton · Hopf's Umlaufsatz

DefinitionNumber of new corners added by a cell#✓fully proved

The number of corners of c that are not already vertices of the region K.

def newVerts (c : Cell) (K : Finset Cell) : ℕ := (cellVerts c \ regVerts K).card
Uses 4 · Used by 1
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 byCell regions built by attaching cells along boundary arcs

DefinitionNumber of new sides added by a cell#✓fully proved

The number of sides of c that are not already edges of the region K.

def newEdges (c : Cell) (K : Finset Cell) : ℕ := (cellEdges c \ regEdges K).card
Uses 4 · Used by 1
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
Used byCell regions built by attaching cells along boundary arcs

InductiveCell regions built by attaching cells along boundary arcs#✓fully proved

Regions built from a single cell by repeatedly attaching a new cell along a boundary arc: the new cell adds one more edge than vertex, so the Euler characteristic is unchanged.

inductive EucBuildable : Finset Cell → Prop
  | singleton (c : Cell) : EucBuildable {c}
  | attach (c : Cell) (K : Finset Cell) (hK : EucBuildable K) (hc : c ∉ K)
      (harc : newEdges c K = newVerts c K + 1) : EucBuildable (insert c K)
Uses 3
Statement usesUnit cell of the plane · Number of new sides added by a cell · Number of new corners added by a cell

DefinitionFour cells around a lattice vertex#✓fully proved

The four cells having v as a corner.

def surroundCells (v : Vtx) : Finset Cell :=
  {(v.1 - 1, v.2 - 1), (v.1, v.2 - 1), (v.1 - 1, v.2), (v.1, v.2)}
Uses 2 · Used by 1
Statement usesUnit cell of the plane · Lattice point as a vertex of the cell complex
Used byCell degree of a lattice vertex

DefinitionCell degree of a lattice vertex#✓fully proved

The number of cells of K having v as a corner.

def cellDeg (K : Finset Cell) (v : Vtx) : ℕ := (surroundCells v ∩ K).card
Uses 3 · Used by 1
Statement usesFour cells around a lattice vertex · Unit cell of the plane · Lattice point as a vertex of the cell complex
Used byAngle defect at a lattice vertex

DefinitionEdge degree of a lattice vertex#✓fully proved

The number of edges of the region K incident to v.

def edgeDeg (K : Finset Cell) (v : Vtx) : ℕ :=
  ((regEdges K).filter (fun e => v ∈ e)).card
Uses 3 · 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
Used byAngle defect at a lattice vertex

DefinitionAngle defect at a lattice vertex#✓fully proved

The angle defect at v, in quarter turns: 4 - 2 · edgeDeg K v + cellDeg K v.

def defect (K : Finset Cell) (v : Vtx) : ℤ :=
  4 - 2 * (edgeDeg K v : ℤ) + (cellDeg K v : ℤ)
Uses 4 · Used by 3
Statement usesCell degree of a lattice vertex · Edge degree of a lattice vertex · Unit cell of the plane · Lattice point as a vertex of the cell complex
Used byNumber of convex corners of a lattice region · Number of pinch points of a lattice region · Number of reflex corners of a lattice region

DefinitionLattice edge to the right neighbour#✓fully proved

The lattice edge from v to its right neighbour.

def incidentEdgeR (v : Vtx) : Sym2 Vtx := s(v, (v.1 + 1, v.2))
Uses 1
Statement usesLattice point as a vertex of the cell complex

DefinitionLattice edge to the left neighbour#✓fully proved

The lattice edge from v to its left neighbour.

def incidentEdgeL (v : Vtx) : Sym2 Vtx := s(v, (v.1 - 1, v.2))
Uses 1
Statement usesLattice point as a vertex of the cell complex

DefinitionLattice edge to the upper neighbour#✓fully proved

The lattice edge from v to its upper neighbour.

def incidentEdgeU (v : Vtx) : Sym2 Vtx := s(v, (v.1, v.2 + 1))
Uses 1
Statement usesLattice point as a vertex of the cell complex

DefinitionLattice edge to the lower neighbour#✓fully proved

The lattice edge from v to its lower neighbour.

def incidentEdgeD (v : Vtx) : Sym2 Vtx := s(v, (v.1, v.2 - 1))
Uses 1
Statement usesLattice point as a vertex of the cell complex

DefinitionNumber of convex corners of a lattice region#✓fully proved

The number of vertices of the region with defect 1 (convex corners).

def wad_n1 (K : Finset Cell) : ℤ :=
  ((regVerts K).filter (fun v => defect K v = 1)).card
Uses 4
Statement usesAngle defect at a lattice vertex · Unit cell of the plane · Lattice point as a vertex of the cell complex · Vertices of a union of unit cells

DefinitionNumber of reflex corners of a lattice region#✓fully proved

The number of vertices of the region with defect -1 (reflex corners).

def wad_n3 (K : Finset Cell) : ℤ :=
  ((regVerts K).filter (fun v => defect K v = -1)).card
Uses 4
Statement usesAngle defect at a lattice vertex · Unit cell of the plane · Lattice point as a vertex of the cell complex · Vertices of a union of unit cells

DefinitionNumber of pinch points of a lattice region#✓fully proved

The number of vertices of the region with defect -2 (pinch points, where two cells meet only at a corner).

def wad_n2d (K : Finset Cell) : ℤ :=
  ((regVerts K).filter (fun v => defect K v = -2)).card
Uses 4
Statement usesAngle defect at a lattice vertex · Unit cell of the plane · Lattice point as a vertex of the cell complex · Vertices of a union of unit cells

DefinitionFour corners of a unit cell#✓fully proved

The four corners of the unit cell with lower-left corner c.

def cornersOf (c : ℤ × ℤ) : Finset (ℤ × ℤ) :=
  {c, (c.1 + 1, c.2), (c.1, c.2 + 1), (c.1 + 1, c.2 + 1)}
Used by 20
Used byVertices of a cell complex · Agreement of the two vertex sets of a cell complex · Vertices of a cell complex after adding a cell · Corner count of a lattice point · Corner count as a count of the four surrounding cells · Corner count after adding a cell · At most four cells meet at a lattice point · A lattice point has an incident cell iff it is a vertex · Cell Gauss–Bonnet formula · Change of the corner defect when a cell is added · Change of the corner defect in terms of eight neighbours · A single cell has corner defect 4 · A unit cell has four distinct corners · Change of the Euler characteristic when a cell is added · A single cell has Euler characteristic 1 · Characterization of the corners of a unit cell · Pinch count changes only at the corners of a new cell · Change of the pinch count in terms of eight neighbours · New vertices of an added cell match the local count · Double counting of cell–corner incidences

DefinitionCorner count of a lattice point#✓fully proved

The number of cells of S having the lattice point v as a corner.

def cornerCount (S : Finset (ℤ × ℤ)) (v : ℤ × ℤ) : ℕ :=
  (S.filter (fun c => v ∈ cornersOf c)).card
Uses 1 · Used by 37
Statement usesFour corners of a unit cell
Used byCorner count at the bottom-left corner of a new cell · Corner count at the bottom-right corner of a new cell · Corner count as a count of the four surrounding cells · Corner count after adding a cell · At most four cells meet at a lattice point · A lattice point has an incident cell iff it is a vertex · Corner count at the top-left corner of a new cell · Corner count at the top-right corner of a new cell · Corner defect of a set of unit cells · Cell Gauss–Bonnet formula · Corner defect as a sum of vertex weights · Change of the corner defect when a cell is added · Change of the corner defect in terms of eight neighbours · A single cell has corner defect 4 · Non-vertices are the points with no incident cell · A pinch point is a vertex · New vertices of an added cell match the local count · Double counting of cell–corner incidences · Corner count of the interior counts inside cells around a point · Even corner counts have zero corner weight · 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 · Straight steps of a simple closed walk carry no corner weight · Zero corner weight where the walk continues horizontally · Zero corner weight where the walk continues vertically · Corner defect of the interior is the number of left turns up to sign · Corner defect of the interior as a sum over walk vertices · Corner weights at the turns of a walk without right turns · Zero corner weight of the interior off the walk · Corner count of the bounded face at a walk vertex · Corner count as a sum of four indicators · Zero corner weight of the bounded face off the walk · Corner defect of the bounded face equals the number of left turns · Corner weight of the bounded face at a walk vertex · Hopf's Umlaufsatz

DefinitionVertices of a cell complex#✓fully proved

The vertices of the cell complex S: all corners of its cells.

def cellVerts (S : Finset (ℤ × ℤ)) : Finset (ℤ × ℤ) :=
  S.biUnion cornersOf
Uses 1 · Used by 22
Statement usesFour corners of a unit cell
Used byAgreement of the two vertex sets of a cell complex · Vertices of a cell complex after adding a cell · A lattice point has an incident cell iff it is a vertex · Corner defect of a set of unit cells · Cell Gauss–Bonnet formula · Corner defect as a sum of vertex weights · Change of the corner defect when a cell is added · A single cell has corner defect 4 · Euler characteristic of a cell complex · Agreement of the two Euler characteristics of a cell complex · Change of the Euler characteristic when a cell is added · A single cell has Euler characteristic 1 · Non-vertices are the points with no incident cell · A pinch point is a vertex · Number of pinch points · Pinch count changes only at the corners of a new cell · New vertices of an added cell match the local count · Double counting of cell–corner incidences · Corner defect of the interior as a sum over walk vertices · Pinch count of the ray-parity interior is zero · Pinch count of the bounded face is zero · Corner defect of the bounded face equals the number of left turns

TheoremA unit cell has four distinct corners#✓fully proved

A cell has four distinct corners.

theorem cornersOf_card (c : ℤ × ℤ) : (cornersOf c).card = 4
Uses 1 · Used by 3
Statement usesFour corners of a unit cell
Used byA single cell has corner defect 4 · A single cell has Euler characteristic 1 · Double counting of cell–corner incidences

TheoremCharacterization of the corners of a unit cell#✓fully proved

v is a corner of c iff c is one of the four cells around v.

theorem mem_cornersOf_iff (c v : ℤ × ℤ) :
    v ∈ cornersOf c ↔
      c = v ∨ c = (v.1 - 1, v.2) ∨ c = (v.1, v.2 - 1) ∨ c = (v.1 - 1, v.2 - 1)
Uses 1 · Used by 3
Statement usesFour corners of a unit cell
Used byCorner count as a count of the four surrounding cells · At most four cells meet at a lattice point · Pinch count changes only at the corners of a new cell

TheoremAt most four cells meet at a lattice point#✓fully proved

At most four cells meet at a lattice point.

theorem cornerCount_le_four (S : Finset (ℤ × ℤ)) (v : ℤ × ℤ) :
    cornerCount S v ≤ 4
Uses 3
Statement usesCorner count of a lattice point
Proof usesFour corners of a unit cell · Characterization of the corners of a unit cell

TheoremDouble counting of cell–corner incidences#✓fully proved

Double counting of cell–corner incidences: ∑ v, cornerCount S v = 4 * S.card.

theorem sum_cornerCount (S : Finset (ℤ × ℤ)) :
    ∑ v ∈ cellVerts S, cornerCount S v = 4 * S.card
Uses 4
Statement usesVertices of a cell complex · Corner count of a lattice point
Proof usesFour corners of a unit cell · A unit cell has four distinct corners

DefinitionCorner defect of a set of unit cells#✓fully proved

The corner defect of S: the number of vertices with exactly one incident cell of S (convex corners) minus the number with exactly three (reflex corners).

def cornerDiff (S : Finset (ℤ × ℤ)) : ℤ :=
  ((cellVerts S).filter (fun v => cornerCount S v = 1)).card
    - ((cellVerts S).filter (fun v => cornerCount S v = 3)).card
Uses 2 · Used by 12
Statement usesVertices of a cell complex · Corner count of a lattice point
Used byCorner defect of two diagonally touching cells · Cell Gauss–Bonnet formula · Corner defect as a sum of vertex weights · Change of the corner defect when a cell is added · A single cell has corner defect 4 · Failure of the cell Gauss–Bonnet formula without a pinch term · Four left turns from a pinch-free interior of Euler characteristic 1 · Corner defect of the interior is the number of left turns up to sign · Corner defect of the interior as a sum over walk vertices · Corner defect of the bounded face equals the number of left turns · Discrete Umlaufsatz for walks of length at least three, shifted form · Hopf's Umlaufsatz

TheoremCorner count after adding a cell#✓fully proved

Adding a new cell c raises the corner count by one exactly at the corners of c.

theorem cornerCount_insert (S : Finset (ℤ × ℤ)) (c : ℤ × ℤ) (hc : c ∉ S) (v : ℤ × ℤ) :
    cornerCount (insert c S) v = cornerCount S v + (if v ∈ cornersOf c then 1 else 0)
Uses 2 · Used by 1
Statement usesCorner count of a lattice point · Four corners of a unit cell
Used byChange of the corner defect when a cell is added

TheoremVertices of a cell complex after adding a cell#✓fully proved

The vertices of insert c S.

theorem cellVerts_insert (S : Finset (ℤ × ℤ)) (c : ℤ × ℤ) :
    cellVerts (insert c S) = cornersOf c ∪ cellVerts S
Uses 2 · Used by 3
Statement usesVertices of a cell complex · Four corners of a unit cell
Used byChange of the corner defect when a cell is added · Change of the Euler characteristic when a cell is added · Pinch count changes only at the corners of a new cell

DefinitionCorner weight of a vertex#✓fully proved

The weight of a vertex with k incident cells in the corner defect: 1 if k = 1, -1 if k = 3, and 0 otherwise.

def cornerWeight (k : ℕ) : ℤ := (if k = 1 then 1 else 0) - (if k = 3 then 1 else 0)
Used by 22
Used byCell Gauss–Bonnet formula · Corner defect as a sum of vertex weights · Change of the corner defect when a cell is added · Change of the corner defect in terms of eight neighbours · Corner weight agrees with its integer version · Change of a vertex weight when one more cell is incident · Even corner counts have zero corner weight · 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 · Straight steps of a simple closed walk carry no corner weight · Zero corner weight where the walk continues horizontally · Zero corner weight where the walk continues vertically · Corner defect of the interior is the number of left turns up to sign · Corner defect of the interior as a sum over walk vertices · Corner weights at the turns of a walk without right turns · Zero corner weight of the interior off the walk · Zero corner weight of the bounded face off the walk · Corner defect of the bounded face equals the number of left turns · Corner weight of the bounded face at a walk vertex · Hopf's Umlaufsatz

TheoremA lattice point has an incident cell iff it is a vertex#✓fully proved

A lattice point has an incident cell iff it is a vertex of S.

theorem cornerCount_pos_iff_mem (S : Finset (ℤ × ℤ)) (v : ℤ × ℤ) :
    0 < cornerCount S v ↔ v ∈ cellVerts S
Uses 3 · Used by 5
Statement usesVertices of a cell complex · Corner count of a lattice point
Proof usesFour corners of a unit cell
Used byChange of the corner defect when a cell is added · Non-vertices are the points with no incident cell · A pinch point is a vertex · Corner defect of the interior as a sum over walk vertices · Corner defect of the bounded face equals the number of left turns

TheoremCorner defect as a sum of vertex weights#✓fully proved

The corner defect as a sum of vertex weights.

theorem cornerDiff_eq_sum (S : Finset (ℤ × ℤ)) :
    cornerDiff S = ∑ v ∈ cellVerts S, cornerWeight (cornerCount S v)
Uses 4 · Used by 3
Statement usesVertices of a cell complex · Corner count of a lattice point · Corner defect of a set of unit cells · Corner weight of a vertex
Used byChange of the corner defect when a cell is added · Corner defect of the interior as a sum over walk vertices · Corner defect of the bounded face equals the number of left turns

TheoremChange of the corner defect when a cell is added#✓fully proved

Change of the corner defect when a new cell is added.

theorem cornerDiff_insert (S : Finset (ℤ × ℤ)) (c : ℤ × ℤ) (hc : c ∉ S) :
    cornerDiff (insert c S)
      = cornerDiff S + ∑ v ∈ cornersOf c,
          (cornerWeight (cornerCount S v + 1) - cornerWeight (cornerCount S v))
Uses 9 · Used by 1
Statement usesCorner count of a lattice point · Four corners of a unit cell · Corner defect of a set of unit cells · Corner weight of a vertex
Proof usesVertices of a cell complex · Vertices of a cell complex after adding a cell · Corner count after adding a cell · A lattice point has an incident cell iff it is a vertex · Corner defect as a sum of vertex weights
Used byCell Gauss–Bonnet formula

TheoremA single cell has corner defect 4#✓fully proved

A single cell has corner defect 4.

theorem cornerDiff_singleton (c : ℤ × ℤ) : cornerDiff ({c} : Finset (ℤ × ℤ)) = 4
Uses 5
Statement usesCorner defect of a set of unit cells
Proof usesVertices of a cell complex · Corner count of a lattice point · Four corners of a unit cell · A unit cell has four distinct corners

TheoremCorner count as a count of the four surrounding cells#✓fully proved

The corner count at v counts the cells of S among the four cells around v.

theorem cornerCount_eq_inter (S : Finset (ℤ × ℤ)) (v : ℤ × ℤ) :
    cornerCount S v
      = (S ∩ ({v, (v.1 - 1, v.2), (v.1, v.2 - 1), (v.1 - 1, v.2 - 1)} : Finset (ℤ × ℤ))).card
Uses 3 · Used by 7
Statement usesCorner count of a lattice point
Proof usesFour corners of a unit cell · Characterization of the corners of a unit cell
Used byCorner count at the bottom-left corner of a new cell · Corner count at the bottom-right corner of a new cell · Corner count at the top-left corner of a new cell · Corner count at the top-right corner of a new cell · A pinch point is a vertex · Corner count of the interior counts inside cells around a point · Corner count as a sum of four indicators

DefinitionFour edges of a unit cell#✓fully proved

The four edges of cell c, each encoded by twice its midpoint.

def edgesOf (c : ℤ × ℤ) : Finset (ℤ × ℤ) :=
  {(2 * c.1 + 1, 2 * c.2), (2 * c.1 + 1, 2 * c.2 + 2),
    (2 * c.1, 2 * c.2 + 1), (2 * c.1 + 2, 2 * c.2 + 1)}
Used by 11
Used byAgreement of the two edge counts of a cell complex · Edges of a cell complex · Cell Gauss–Bonnet formula · Change of the Euler characteristic when a cell is added · A single cell has Euler characteristic 1 · Edge codes of a unit cell are its doubled edge midpoints · Membership of a cell's bottom edge in the cell complex · Membership of a cell's left edge in the cell complex · Membership of a cell's right edge in the cell complex · Membership of a cell's top edge in the cell complex · New edges of an added cell match the local count

DefinitionEdges of a cell complex#✓fully proved

The edges of the cell complex S, encoded by doubled midpoints.

def cellEdges (S : Finset (ℤ × ℤ)) : Finset (ℤ × ℤ) := S.biUnion edgesOf
Uses 1 · Used by 11
Statement usesFour edges of a unit cell
Used byAgreement of the two edge counts of a cell complex · Cell Gauss–Bonnet formula · Euler characteristic of a cell complex · Agreement of the two Euler characteristics of a cell complex · Change of the Euler characteristic when a cell is added · A single cell has Euler characteristic 1 · Membership of a cell's bottom edge in the cell complex · Membership of a cell's left edge in the cell complex · Membership of a cell's right edge in the cell complex · Membership of a cell's top edge in the cell complex · New edges of an added cell match the local count

DefinitionEuler characteristic of a cell complex#✓fully proved

The Euler characteristic V - E + F of the closed cell complex formed by the cells of S.

def eulerChar (S : Finset (ℤ × ℤ)) : ℤ :=
  ((cellVerts S).card : ℤ) - (cellEdges S).card + S.card
Uses 2 · Used by 12
Statement usesVertices of a cell complex · Edges of a cell complex
Used byCell Gauss–Bonnet formula · Euler characteristic of two diagonally touching cells · Agreement of the two Euler characteristics of a cell complex · Change of the Euler characteristic when a cell is added · Euler characteristic bound via the open-top skeleton · A single cell has Euler characteristic 1 · Failure of the cell Gauss–Bonnet formula without a pinch term · Four left turns from a pinch-free interior of Euler characteristic 1 · Euler characteristic at most 1 for a connected skeleton · Discrete Umlaufsatz for walks of length at least three, shifted form · Interior of a simple closed walk has Euler characteristic at most 1 · Hopf's Umlaufsatz

TheoremA single cell has Euler characteristic 1#✓fully proved

A single cell has Euler characteristic 1.

theorem eulerChar_singleton (c : ℤ × ℤ) : eulerChar ({c} : Finset (ℤ × ℤ)) = 1
Uses 6
Statement usesEuler characteristic of a cell complex
Proof usesVertices of a cell complex · Four corners of a unit cell · A unit cell has four distinct corners · Edges of a cell complex · Four edges of a unit cell

TheoremChange of the Euler characteristic when a cell is added#✓fully proved

Change of the Euler characteristic when a new cell is added: new vertices minus new edges plus one.

theorem eulerChar_insert (S : Finset (ℤ × ℤ)) (c : ℤ × ℤ) (hc : c ∉ S) :
    eulerChar (insert c S)
      = eulerChar S + (((cornersOf c \ cellVerts S).card : ℤ)
          - (edgesOf c \ cellEdges S).card + 1)
Uses 6 · Used by 1
Statement usesVertices of a cell complex · Four corners of a unit cell · Edges of a cell complex · Four edges of a unit cell · Euler characteristic of a cell complex
Proof usesVertices of a cell complex after adding a cell
Used byCell Gauss–Bonnet formula

TheoremCardinality of an intersection as a sum of indicators#✓fully proved

The size of S ∩ T as the sum over T of the indicator of S. See also Finset.sum_boole.

theorem card_inter_eq_sum (S T : Finset (ℤ × ℤ)) :
    ((S ∩ T).card : ℤ) = ∑ t ∈ T, (if t ∈ S then (1 : ℤ) else 0)
Used by 6
Used byCorner count at the bottom-left corner of a new cell · Corner count at the bottom-right corner of a new cell · Corner count at the top-left corner of a new cell · Corner count at the top-right corner of a new cell · Corner count of the interior counts inside cells around a point · Corner count as a sum of four indicators

TheoremCorner count at the bottom-left corner of a new cell#✓fully proved

The corner count at the bottom-left corner of a cell (x, y) ∉ S.

theorem cornerCount_BL (S : Finset (ℤ × ℤ)) (x y : ℤ) (hc : (x, y) ∉ S) :
    (cornerCount S (x, y) : ℤ)
      = (if (x - 1, y) ∈ S then 1 else 0) + (if (x, y - 1) ∈ S then 1 else 0)
        + (if (x - 1, y - 1) ∈ S then 1 else 0)
Uses 3 · Used by 2
Statement usesCorner count of a lattice point
Proof usesCardinality of an intersection as a sum of indicators · Corner count as a count of the four surrounding cells
Used byChange of the corner defect in terms of eight neighbours · New vertices of an added cell match the local count

TheoremCorner count at the bottom-right corner of a new cell#✓fully proved

The corner count at the bottom-right corner of a cell (x, y) ∉ S.

theorem cornerCount_BR (S : Finset (ℤ × ℤ)) (x y : ℤ) (hc : (x, y) ∉ S) :
    (cornerCount S (x + 1, y) : ℤ)
      = (if (x + 1, y) ∈ S then 1 else 0) + (if (x + 1, y - 1) ∈ S then 1 else 0)
        + (if (x, y - 1) ∈ S then 1 else 0)
Uses 3 · Used by 2
Statement usesCorner count of a lattice point
Proof usesCardinality of an intersection as a sum of indicators · Corner count as a count of the four surrounding cells
Used byChange of the corner defect in terms of eight neighbours · New vertices of an added cell match the local count

TheoremCorner count at the top-left corner of a new cell#✓fully proved

The corner count at the top-left corner of a cell (x, y) ∉ S.

theorem cornerCount_TL (S : Finset (ℤ × ℤ)) (x y : ℤ) (hc : (x, y) ∉ S) :
    (cornerCount S (x, y + 1) : ℤ)
      = (if (x, y + 1) ∈ S then 1 else 0) + (if (x - 1, y + 1) ∈ S then 1 else 0)
        + (if (x - 1, y) ∈ S then 1 else 0)
Uses 3 · Used by 2
Statement usesCorner count of a lattice point
Proof usesCardinality of an intersection as a sum of indicators · Corner count as a count of the four surrounding cells
Used byChange of the corner defect in terms of eight neighbours · New vertices of an added cell match the local count

TheoremCorner count at the top-right corner of a new cell#✓fully proved

The corner count at the top-right corner of a cell (x, y) ∉ S.

theorem cornerCount_TR (S : Finset (ℤ × ℤ)) (x y : ℤ) (hc : (x, y) ∉ S) :
    (cornerCount S (x + 1, y + 1) : ℤ)
      = (if (x + 1, y + 1) ∈ S then 1 else 0) + (if (x, y + 1) ∈ S then 1 else 0)
        + (if (x + 1, y) ∈ S then 1 else 0)
Uses 3 · Used by 2
Statement usesCorner count of a lattice point
Proof usesCardinality of an intersection as a sum of indicators · Corner count as a count of the four surrounding cells
Used byChange of the corner defect in terms of eight neighbours · New vertices of an added cell match the local count

DefinitionMidpoint encoding of a lattice edge#✓fully proved

The lattice edge {a, b} encoded by the sum a + b, twice its midpoint; injective on unit edges.

def edgeCode : Sym2 (ℤ × ℤ) → ℤ × ℤ :=
  Sym2.lift ⟨fun a b => (a.1 + b.1, a.2 + b.2), by
    intro a b
    ext <;> simp only <;> omega⟩
Used by 2
Used byAgreement of the two edge counts of a cell complex · Edge codes of a unit cell are its doubled edge midpoints

TheoremEdge codes of a unit cell are its doubled edge midpoints#✓fully proved

The codes of the edges of a cell are StatMech.Onsager.CellEuler.edgesOf.

theorem image_cellEdges_edgeCode (c : Cell) :
    (StatMech.CellEulerChar.cellEdges c).image edgeCode = edgesOf c
Uses 5 · Used by 1
Statement usesUnit cell of the plane · Sides of a unit cell · Four edges of a unit cell · Midpoint encoding of a lattice edge
Proof usesLattice point as a vertex of the cell complex
Used byAgreement of the two edge counts of a cell complex

TheoremAgreement of the two edge counts of a cell complex#✓fully proved

The two edge counts of a cell complex agree.

theorem card_cellEdges_eq_regEdges (S : Finset Cell) :
    (StatMech.Onsager.CellEuler.cellEdges S).card = (regEdges S).card
Uses 8 · 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 · Edges of a cell complex
Proof usesSides of a unit cell · Four edges of a unit cell · Midpoint encoding of a lattice edge · Edge codes of a unit cell are its doubled edge midpoints
Used byAgreement of the two Euler characteristics of a cell complex

TheoremAgreement of the two vertex sets of a cell complex#✓fully proved

The two vertex sets of a cell complex agree.

theorem cellVerts_eq_regVerts (S : Finset Cell) :
    StatMech.Onsager.CellCount.cellVerts S = regVerts S
Uses 6 · Used by 1
Statement usesUnit cell of the plane · Vertices of a union of unit cells · Vertices of a cell complex
Proof usesLattice point as a vertex of the cell complex · Corners of a unit cell · Four corners of a unit cell
Used byAgreement of the two Euler characteristics of a cell complex

TheoremAgreement of the two Euler characteristics of a cell complex#✓fully proved

The Euler characteristic eulerChar agrees with StatMech.CellEulerChar.regChi.

theorem eulerChar_eq_regChi (S : Finset Cell) : eulerChar S = regChi S
Uses 10 · Used by 3
Statement usesUnit cell of the plane · Euler characteristic of a union of unit cells · Euler characteristic of a cell complex
Proof usesLattice point as a vertex of the cell complex · Edges of a union of unit cells · Vertices of a union of unit cells · Vertices of a cell complex · Edges of a cell complex · Agreement of the two edge counts of a cell complex · Agreement of the two vertex sets of a cell complex
Used byEuler characteristic bound via the open-top skeleton · Euler characteristic at most 1 for a connected skeleton · Hopf's Umlaufsatz

DefinitionTop edge of a unit cell#✓fully proved

The top edge of the cell c.

def topEdge (c : Cell) : Sym2 Vtx :=
  s((c.1, c.2 + 1), (c.1 + 1, c.2 + 1))
Uses 2 · Used by 3
Statement usesUnit cell of the plane · Lattice point as a vertex of the cell complex
Used byDistinct cells have distinct top edges · Regular Euler characteristic bound via the open-top skeleton · Top edges of a set of cells

DefinitionTop edges of a set of cells#✓fully proved

The top edges of the cells of S.

def topEdges (S : Finset Cell) : Finset (Sym2 Vtx) := S.image topEdge
Uses 3 · Used by 5
Statement usesUnit cell of the plane · Lattice point as a vertex of the cell complex · Top edge of a unit cell
Used byDistinct cells have distinct top edges · Edges of the open-top skeleton · Open-top skeleton of a cell complex · Regular Euler characteristic bound via the open-top skeleton · Edge count bound for a connected open-top skeleton

TheoremDistinct cells have distinct top edges#✓fully proved

Distinct cells have distinct top edges.

theorem card_topEdges (S : Finset Cell) : (topEdges S).card = S.card
Uses 4 · Used by 1
Statement usesUnit cell of the plane · Lattice point as a vertex of the cell complex · Top edges of a set of cells
Proof usesTop edge of a unit cell
Used byRegular Euler characteristic bound via the open-top skeleton

DefinitionOpen-top skeleton of a cell complex#✓fully proved

The 1-skeleton of the cell complex S with the top edge of every cell removed, as a simple graph on its vertices.

def openTopSkeleton (S : Finset Cell) : SimpleGraph {v // v ∈ regVerts S} where
  Adj a b := s(a.1, b.1) ∈ regEdges S \ topEdges S
  symm := ⟨fun a b h => by
    rwa [Sym2.eq_swap]⟩
  loopless := ⟨by
    intro a h
    exact (wad_edge_not_diag (mem_sdiff.mp h).1) (by simp)⟩
Uses 6 · Used by 4
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 · Top edges of a set of cells
Used byEuler characteristic bound via the open-top skeleton · Edges of the open-top skeleton · Regular Euler characteristic bound via the open-top skeleton · Edge count bound for a connected open-top skeleton

DefinitionEdges of the open-top skeleton#✓fully proved

The edges of openTopSkeleton S are the edges of S other than top edges.

StatMech.Onsager.CellEulerBound.openTopEdgeEquiv · 15 lines 
noncomputable def openTopEdgeEquiv (S : Finset Cell) :
    {e // e ∈ (openTopSkeleton S).edgeSet} ≃ {e // e ∈ regEdges S \ topEdges S} where
  toFun e := ⟨Sym2.map Subtype.val e.1,
    (mem_openTopSkeleton_edgeSet_iff S e.1).mp e.2⟩
  invFun e := ⟨e.1.attachWith (fun v hv =>
      wad_edge_mem_regVerts (mem_sdiff.mp e.2).1 hv), by
    rw [mem_openTopSkeleton_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 8 · Used by 1
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 · Open-top skeleton of a cell complex · Top edges of a set of cells
Used byEdge count bound for a connected open-top skeleton

TheoremEdge count bound for a connected open-top skeleton#✓fully proved

If the open-top skeleton is connected, it has at least as many edges as vertices minus one.

theorem regVerts_card_le (S : Finset Cell) (hconn : (openTopSkeleton S).Connected) :
    (regVerts S).card ≤ (regEdges S \ topEdges S).card + 1
Uses 7 · 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 · Vertices of a union of unit cells · Open-top skeleton of a cell complex · Top edges of a set of cells
Proof usesEdges of the open-top skeleton
Used byRegular Euler characteristic bound via the open-top skeleton

TheoremRegular Euler characteristic bound via the open-top skeleton#✓fully proved

If the open-top skeleton of S is connected, then regChi S ≤ 1.

theorem regChi_le_one (S : Finset Cell) (hconn : (openTopSkeleton S).Connected) :
    regChi S ≤ 1
Uses 11 · Used by 1
Statement usesUnit cell of the plane · Lattice point as a vertex of the cell complex · Euler characteristic of a union of unit cells · Vertices of a union of unit cells · Open-top skeleton of a cell complex
Proof usesSides of a unit cell · Edges of a union of unit cells · Distinct cells have distinct top edges · Edge count bound for a connected open-top skeleton · Top edge of a unit cell · Top edges of a set of cells
Used byEuler characteristic bound via the open-top skeleton

TheoremEuler characteristic bound via the open-top skeleton#✓fully proved

If the open-top skeleton of S is connected, then eulerChar S ≤ 1. See also StatMech.Onsager.CellEulerFaithful.eulerChar_le_one_of_skeleton_connected, which assumes connectivity of the full skeleton.

theorem eulerChar_le_one (S : Finset Cell) (hconn : (openTopSkeleton S).Connected) :
    eulerChar S ≤ 1
Uses 8
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 · Open-top skeleton of a cell complex
Proof usesEuler characteristic of a union of unit cells · Agreement of the two Euler characteristics of a cell complex · Regular Euler characteristic bound via the open-top skeleton

TheoremCorner defect of two diagonally touching cells#✓fully proved

Two diagonally touching cells have corner defect 6.

theorem cornerDiff_cex :
    cornerDiff ({((0:ℤ), (0:ℤ)), ((1:ℤ), (1:ℤ))} : Finset (ℤ × ℤ)) = 6
Uses 1 · Used by 1
Statement usesCorner defect of a set of unit cells
Used byFailure of the cell Gauss–Bonnet formula without a pinch term

TheoremEuler characteristic of two diagonally touching cells#✓fully proved

Two diagonally touching cells have Euler characteristic 1.

theorem eulerChar_cex :
    eulerChar ({((0:ℤ), (0:ℤ)), ((1:ℤ), (1:ℤ))} : Finset (ℤ × ℤ)) = 1
Uses 1 · Used by 1
Statement usesEuler characteristic of a cell complex
Used byFailure of the cell Gauss–Bonnet formula without a pinch term

TheoremFailure of the cell Gauss–Bonnet formula without a pinch term#✓fully proved

The formula cornerDiff S = 4 * eulerChar S fails in general (two diagonally touching cells); see StatMech.Onsager.CellGaussBonnetGlobal.cornerDiff_eq for the correct formula with a pinch term.

theorem gaussBonnet_stated_false :
    ¬ ∀ S : Finset (ℤ × ℤ), cornerDiff S = 4 * eulerChar S
Uses 4
Statement usesCorner defect of a set of unit cells · Euler characteristic of a cell complex
Proof usesCorner defect of two diagonally touching cells · Euler characteristic of two diagonally touching cells

DefinitionIndicator of a Boolean#✓fully proved

The indicator 1 or 0 of a Boolean.

def bI (b : Bool) : ℤ := if b then 1 else 0
Used by 10
Used byBoolean indicator of a decided proposition · Change of the corner defect in terms of eight neighbours · Number of new edges when a cell is added · Number of new vertices when a cell is added · Local change of the corner defect · Failure of the local identity without a pinch term · Local change of the number of pinch points · Change of the pinch count in terms of eight neighbours · New edges of an added cell match the local count · New vertices of an added cell match the local count

DefinitionInteger-valued corner weight#✓fully proved

The vertex weight cornerWeight extended to integers.

def icw (k : ℤ) : ℤ := (if k = 1 then 1 else 0) - (if k = 3 then 1 else 0)
Used by 4
Used byCorner weight agrees with its integer version · Change of a vertex weight when one more cell is incident · Integer jump of the corner weight · Failure of the local identity without a pinch term

DefinitionInteger jump of the corner weight#✓fully proved

The change of the vertex weight from m to m + 1 incident cells.

def ijump (m : ℤ) : ℤ := icw (m + 1) - icw m
Uses 1 · Used by 4
Statement usesInteger-valued corner weight
Used byChange of the corner defect in terms of eight neighbours · Change of a vertex weight when one more cell is incident · Local change of the corner defect · Failure of the local identity without a pinch term

DefinitionIndicator of zero#✓fully proved

The indicator of m = 0.

def isZero (m : ℤ) : ℤ := if m = 0 then 1 else 0
Used by 3
Used byNumber of new vertices when a cell is added · Failure of the local identity without a pinch term · New vertices of an added cell match the local count

DefinitionLocal change of the corner defect#✓fully proved

The change of the corner defect when a cell is added, given which of its eight neighbours are present (e, w, n, s, ne, nw, se, sw).

def lhsLocal (e w n s ne nw se sw : Bool) : ℤ :=
  ijump (bI w + bI s + bI sw) + ijump (bI e + bI se + bI s)
    + ijump (bI n + bI nw + bI w) + ijump (bI ne + bI n + bI e)
Uses 2 · Used by 4
Statement usesIndicator of a Boolean · Integer jump of the corner weight
Used byCell Gauss–Bonnet formula · Change of the corner defect in terms of eight neighbours · Local cell Gauss–Bonnet identity · Failure of the local identity without a pinch term

DefinitionNumber of new vertices when a cell is added#✓fully proved

The number of new vertices when a cell is added, given its eight neighbours.

def deltaV (e w n s ne nw se sw : Bool) : ℤ :=
  isZero (bI w + bI s + bI sw) + isZero (bI e + bI se + bI s)
    + isZero (bI n + bI nw + bI w) + isZero (bI ne + bI n + bI e)
Uses 2 · Used by 4
Statement usesIndicator of a Boolean · Indicator of zero
Used byCell Gauss–Bonnet formula · Failure of the local identity without a pinch term · Four times the local change of the Euler characteristic · New vertices of an added cell match the local count

DefinitionNumber of new edges when a cell is added#✓fully proved

The number of new edges when a cell is added, given its four side neighbours.

def deltaE (e w n s : Bool) : ℤ :=
  (1 - bI s) + (1 - bI n) + (1 - bI w) + (1 - bI e)
Uses 1 · Used by 4
Statement usesIndicator of a Boolean
Used byCell Gauss–Bonnet formula · Failure of the local identity without a pinch term · Four times the local change of the Euler characteristic · New edges of an added cell match the local count

DefinitionFour times the local change of the Euler characteristic#✓fully proved

Four times the change of the Euler characteristic when a cell is added.

def rhsStated (e w n s ne nw se sw : Bool) : ℤ :=
  4 * (deltaV e w n s ne nw se sw - deltaE e w n s + 1)
Uses 2 · Used by 2
Statement usesNumber of new edges when a cell is added · Number of new vertices when a cell is added
Used byFailure of the local identity without a pinch term · Corrected right side of the local Gauss–Bonnet identity

TheoremFailure of the local identity without a pinch term#✓fully proved

The change of the corner defect is not always four times the change of the Euler characteristic.

theorem localIdentity_stated_false :
    ¬ ∀ e w n s ne nw se sw : Bool,
      lhsLocal e w n s ne nw se sw = rhsStated e w n s ne nw se sw
Uses 8
Statement usesLocal change of the corner defect · Four times the local change of the Euler characteristic
Proof usesIndicator of a Boolean · Number of new edges when a cell is added · Number of new vertices when a cell is added · Integer-valued corner weight · Integer jump of the corner weight · Indicator of zero

DefinitionLocal change of the number of pinch points#✓fully proved

The change of the number of pinch points at the four corners of a new cell, given its eight neighbours.

def pinchDelta (e w n s ne nw se sw : Bool) : ℤ :=
  (bI (sw && !w && !s) - bI (w && s && !sw))
  + (bI (se && !e && !s) - bI (e && s && !se))
  + (bI (nw && !n && !w) - bI (n && w && !nw))
  + (bI (ne && !n && !e) - bI (n && e && !ne))
Uses 1 · Used by 3
Statement usesIndicator of a Boolean
Used byCell Gauss–Bonnet formula · Change of the pinch count in terms of eight neighbours · Corrected right side of the local Gauss–Bonnet identity

DefinitionCorrected right side of the local Gauss–Bonnet identity#✓fully proved

Four times the change of the Euler characteristic plus twice the change of the number of pinch points.

def rhsCorrected (e w n s ne nw se sw : Bool) : ℤ :=
  rhsStated e w n s ne nw se sw + 2 * pinchDelta e w n s ne nw se sw
Uses 2 · Used by 2
Statement usesLocal change of the number of pinch points · Four times the local change of the Euler characteristic
Used byCell Gauss–Bonnet formula · Local cell Gauss–Bonnet identity

TheoremLocal cell Gauss–Bonnet identity#✓fully proved

Local cell Gauss–Bonnet identity: when a cell is added, the change of the corner defect is four times the change of the Euler characteristic plus twice the change of the number of pinch points.

theorem localIdentity_corrected :
    ∀ e w n s ne nw se sw : Bool,
      lhsLocal e w n s ne nw se sw = rhsCorrected e w n s ne nw se sw
Uses 2 · Used by 1
Statement usesLocal change of the corner defect · Corrected right side of the local Gauss–Bonnet identity
Used byCell Gauss–Bonnet formula

TheoremCorner weight agrees with its integer version#✓fully proved

cornerWeight agrees with its integer version icw.

theorem cornerWeight_eq_icw (m : ℕ) : cornerWeight m = icw (m : ℤ)
Uses 2 · Used by 1
Statement usesCorner weight of a vertex · Integer-valued corner weight
Used byChange of a vertex weight when one more cell is incident

TheoremChange of a vertex weight when one more cell is incident#✓fully proved

The change of a vertex weight when one more cell becomes incident.

theorem cornerWeight_jump (m : ℕ) :
    cornerWeight (m + 1) - cornerWeight m = ijump (m : ℤ)
Uses 4 · Used by 1
Statement usesCorner weight of a vertex · Integer jump of the corner weight
Proof usesCorner weight agrees with its integer version · Integer-valued corner weight
Used byChange of the corner defect in terms of eight neighbours

TheoremBoolean indicator of a decided proposition#✓fully proved

The indicator bI of a decided proposition.

theorem bI_decide (p : Prop) [Decidable p] : bI (decide p) = if p then 1 else 0
Uses 1
Statement usesIndicator of a Boolean

TheoremChange of the corner defect in terms of eight neighbours#✓fully proved

The change of the corner defect when the cell (x, y) is added, in terms of its eight neighbours.

theorem cornerDiff_jump_sum (S : Finset (ℤ × ℤ)) (x y : ℤ) (hc : (x, y) ∉ S) :
    (∑ v ∈ cornersOf (x, y),
        (cornerWeight (cornerCount S v + 1) - cornerWeight (cornerCount S v)))
      = lhsLocal (decide ((x + 1, y) ∈ S)) (decide ((x - 1, y) ∈ S)) (decide ((x, y + 1) ∈ S))
          (decide ((x, y - 1) ∈ S)) (decide ((x + 1, y + 1) ∈ S)) (decide ((x - 1, y + 1) ∈ S))
          (decide ((x + 1, y - 1) ∈ S)) (decide ((x - 1, y - 1) ∈ S))
Uses 11 · Used by 1
Statement usesCorner count of a lattice point · Four corners of a unit cell · Corner weight of a vertex · Local change of the corner defect
Proof usesCorner count at the bottom-left corner of a new cell · Corner count at the bottom-right corner of a new cell · Corner count at the top-left corner of a new cell · Corner count at the top-right corner of a new cell · Change of a vertex weight when one more cell is incident · Indicator of a Boolean · Integer jump of the corner weight
Used byCell Gauss–Bonnet formula

TheoremNon-vertices are the points with no incident cell#✓fully proved

A lattice point is not a vertex of S iff no cell of S is incident to it.

theorem notMem_cellVerts_iff_cornerCount_zero (S : Finset (ℤ × ℤ)) (v : ℤ × ℤ) :
    v ∉ cellVerts S ↔ cornerCount S v = 0
Uses 3 · Used by 1
Statement usesVertices of a cell complex · Corner count of a lattice point
Proof usesA lattice point has an incident cell iff it is a vertex
Used byNew vertices of an added cell match the local count

TheoremCardinality of a set difference as a sum of indicators#✓fully proved

The size of s \ t as a sum of indicators.

theorem card_sdiff_eq_sum (s t : Finset (ℤ × ℤ)) :
    ((s \ t).card : ℤ) = ∑ v ∈ s, (if v ∉ t then (1 : ℤ) else 0)
Used by 2
Used byNew edges of an added cell match the local count · New vertices of an added cell match the local count

TheoremNew vertices of an added cell match the local count#✓fully proved

The number of new vertices when the cell (x, y) is added.

theorem sdiff_cellVerts_card_eq_deltaV (S : Finset (ℤ × ℤ)) (x y : ℤ) (hc : (x, y) ∉ S) :
    ((cornersOf (x, y) \ cellVerts S).card : ℤ)
      = deltaV (decide ((x + 1, y) ∈ S)) (decide ((x - 1, y) ∈ S)) (decide ((x, y + 1) ∈ S))
          (decide ((x, y - 1) ∈ S)) (decide ((x + 1, y + 1) ∈ S)) (decide ((x - 1, y + 1) ∈ S))
          (decide ((x + 1, y - 1) ∈ S)) (decide ((x - 1, y - 1) ∈ S))
Uses 12 · Used by 1
Statement usesVertices of a cell complex · Four corners of a unit cell · Number of new vertices when a cell is added
Proof usesCorner count at the bottom-left corner of a new cell · Corner count at the bottom-right corner of a new cell · Corner count at the top-left corner of a new cell · Corner count at the top-right corner of a new cell · Cardinality of a set difference as a sum of indicators · Non-vertices are the points with no incident cell · Corner count of a lattice point · Indicator of a Boolean · Indicator of zero
Used byCell Gauss–Bonnet formula

TheoremMembership of a cell's bottom edge in the cell complex#✓fully proved

The horizontal edge with doubled midpoint (2x + 1, 2y) belongs to S iff one of the two cells it bounds does.

theorem mem_cellEdges_bottom (S : Finset (ℤ × ℤ)) (x y : ℤ) :
    ((2 * x + 1, 2 * y) : ℤ × ℤ) ∈ cellEdges S ↔ (x, y) ∈ S ∨ (x, y - 1) ∈ S
Uses 2 · Used by 1
Statement usesEdges of a cell complex
Proof usesFour edges of a unit cell
Used byNew edges of an added cell match the local count

TheoremMembership of a cell's top edge in the cell complex#✓fully proved

The horizontal edge with doubled midpoint (2x + 1, 2y + 2) belongs to S iff one of the two cells it bounds does.

theorem mem_cellEdges_top (S : Finset (ℤ × ℤ)) (x y : ℤ) :
    ((2 * x + 1, 2 * y + 2) : ℤ × ℤ) ∈ cellEdges S ↔ (x, y) ∈ S ∨ (x, y + 1) ∈ S
Uses 2 · Used by 1
Statement usesEdges of a cell complex
Proof usesFour edges of a unit cell
Used byNew edges of an added cell match the local count

TheoremMembership of a cell's left edge in the cell complex#✓fully proved

The vertical edge with doubled midpoint (2x, 2y + 1) belongs to S iff one of the two cells it bounds does.

theorem mem_cellEdges_left (S : Finset (ℤ × ℤ)) (x y : ℤ) :
    ((2 * x, 2 * y + 1) : ℤ × ℤ) ∈ cellEdges S ↔ (x, y) ∈ S ∨ (x - 1, y) ∈ S
Uses 2 · Used by 1
Statement usesEdges of a cell complex
Proof usesFour edges of a unit cell
Used byNew edges of an added cell match the local count

TheoremMembership of a cell's right edge in the cell complex#✓fully proved

The vertical edge with doubled midpoint (2x + 2, 2y + 1) belongs to S iff one of the two cells it bounds does.

theorem mem_cellEdges_right (S : Finset (ℤ × ℤ)) (x y : ℤ) :
    ((2 * x + 2, 2 * y + 1) : ℤ × ℤ) ∈ cellEdges S ↔ (x, y) ∈ S ∨ (x + 1, y) ∈ S
Uses 2 · Used by 1
Statement usesEdges of a cell complex
Proof usesFour edges of a unit cell
Used byNew edges of an added cell match the local count

TheoremNew edges of an added cell match the local count#✓fully proved

The number of new edges when the cell (x, y) is added.

theorem sdiff_cellEdges_card_eq_deltaE (S : Finset (ℤ × ℤ)) (x y : ℤ) (hc : (x, y) ∉ S) :
    ((edgesOf (x, y) \ cellEdges S).card : ℤ)
      = deltaE (decide ((x + 1, y) ∈ S)) (decide ((x - 1, y) ∈ S)) (decide ((x, y + 1) ∈ S))
          (decide ((x, y - 1) ∈ S))
Uses 9 · Used by 1
Statement usesEdges of a cell complex · Four edges of a unit cell · Number of new edges when a cell is added
Proof usesCardinality of a set difference as a sum of indicators · Membership of a cell's bottom edge in the cell complex · Membership of a cell's left edge in the cell complex · Membership of a cell's right edge in the cell complex · Membership of a cell's top edge in the cell complex · Indicator of a Boolean
Used byCell Gauss–Bonnet formula

DefinitionPinch point of a set of unit cells#✓fully proved

The lattice point v is a pinch point of S: of the four cells around v, exactly two diagonally opposite ones belong to S.

def pinchAt (S : Finset (ℤ × ℤ)) (v : ℤ × ℤ) : Prop :=
  (v ∈ S ∧ (v.1 - 1, v.2 - 1) ∈ S ∧ (v.1 - 1, v.2) ∉ S ∧ (v.1, v.2 - 1) ∉ S) ∨
    ((v.1 - 1, v.2) ∈ S ∧ (v.1, v.2 - 1) ∈ S ∧ v ∉ S ∧ (v.1 - 1, v.2 - 1) ∉ S)
Used by 13
Used byA pinch point is a vertex · Pinch count changes only at the corners of a new cell · Change of the pinch indicator at the bottom-left corner of a new cell · Change of the pinch indicator at the bottom-right corner of a new cell · Change of the pinch indicator at the top-left corner of a new cell · Change of the pinch indicator at the top-right corner of a new cell · Pinch point indicator · Pinch count of the ray-parity interior is zero · Interior of a simple closed walk has no pinch points · Corner count of the bounded face at a walk vertex · Bounded face of a simple closed walk has no pinch points · Pinch count of the bounded face is zero · Hopf's Umlaufsatz

DefinitionPinch point indicator#✓fully proved

The indicator of v being a pinch point of S.

def pinchW (S : Finset (ℤ × ℤ)) (v : ℤ × ℤ) : ℤ := if pinchAt S v then 1 else 0
Uses 1 · Used by 10
Statement usesPinch point of a set of unit cells
Used byCell Gauss–Bonnet formula · Number of pinch points · Pinch count changes only at the corners of a new cell · Change of the pinch indicator at the bottom-left corner of a new cell · Change of the pinch indicator at the bottom-right corner of a new cell · Change of the pinch indicator at the top-left corner of a new cell · Change of the pinch indicator at the top-right corner of a new cell · Change of the pinch count in terms of eight neighbours · Pinch count of the ray-parity interior is zero · Pinch count of the bounded face is zero

DefinitionNumber of pinch points#✓fully proved

The number of pinch points of S.

def pinchCount (S : Finset (ℤ × ℤ)) : ℤ := ∑ v ∈ cellVerts S, pinchW S v
Uses 2 · Used by 7
Statement usesVertices of a cell complex · Pinch point indicator
Used byCell Gauss–Bonnet formula · Pinch count changes only at the corners of a new cell · Four left turns from a pinch-free interior of Euler characteristic 1 · Pinch count of the ray-parity interior is zero · Pinch count of the bounded face is zero · Discrete Umlaufsatz for walks of length at least three, shifted form · Hopf's Umlaufsatz

TheoremA pinch point is a vertex#✓fully proved

A pinch point is a vertex of S.

theorem pinchAt_mem_cellVerts (S : Finset (ℤ × ℤ)) (v : ℤ × ℤ) (h : pinchAt S v) :
    v ∈ cellVerts S
Uses 5 · Used by 1
Statement usesVertices of a cell complex · Pinch point of a set of unit cells
Proof usesCorner count of a lattice point · Corner count as a count of the four surrounding cells · A lattice point has an incident cell iff it is a vertex
Used byPinch count changes only at the corners of a new cell

TheoremPinch count changes only at the corners of a new cell#✓fully proved

Adding a cell changes the pinch count only at the corners of that cell.

theorem pinchCount_insert (S : Finset (ℤ × ℤ)) (c : ℤ × ℤ) (_hc : c ∉ S) :
    pinchCount (insert c S)
      = pinchCount S + ∑ v ∈ cornersOf c, (pinchW (insert c S) v - pinchW S v)
Uses 8 · Used by 1
Statement usesFour corners of a unit cell · Number of pinch points · Pinch point indicator
Proof usesVertices of a cell complex · Characterization of the corners of a unit cell · Vertices of a cell complex after adding a cell · Pinch point of a set of unit cells · A pinch point is a vertex
Used byCell Gauss–Bonnet formula

TheoremChange of the pinch indicator at the bottom-left corner of a new cell#✓fully proved

Change of the pinch indicator at the bottom-left corner of a new cell.

theorem pinch_diff_BL (S : Finset (ℤ × ℤ)) (x y : ℤ) (hc : (x, y) ∉ S) :
    pinchW (insert (x, y) S) (x, y) - pinchW S (x, y)
      = (if ((x - 1, y - 1) ∈ S ∧ (x - 1, y) ∉ S ∧ (x, y - 1) ∉ S) then (1 : ℤ) else 0)
        - (if ((x - 1, y) ∈ S ∧ (x, y - 1) ∈ S ∧ (x - 1, y - 1) ∉ S) then (1 : ℤ) else 0)
Uses 2 · Used by 1
Statement usesPinch point indicator
Proof usesPinch point of a set of unit cells
Used byChange of the pinch count in terms of eight neighbours

TheoremChange of the pinch indicator at the bottom-right corner of a new cell#✓fully proved

Change of the pinch indicator at the bottom-right corner of a new cell.

theorem pinch_diff_BR (S : Finset (ℤ × ℤ)) (x y : ℤ) (hc : (x, y) ∉ S) :
    pinchW (insert (x, y) S) (x + 1, y) - pinchW S (x + 1, y)
      = (if ((x + 1, y - 1) ∈ S ∧ (x + 1, y) ∉ S ∧ (x, y - 1) ∉ S) then (1 : ℤ) else 0)
        - (if ((x + 1, y) ∈ S ∧ (x, y - 1) ∈ S ∧ (x + 1, y - 1) ∉ S) then (1 : ℤ) else 0)
Uses 2 · Used by 1
Statement usesPinch point indicator
Proof usesPinch point of a set of unit cells
Used byChange of the pinch count in terms of eight neighbours

TheoremChange of the pinch indicator at the top-left corner of a new cell#✓fully proved

Change of the pinch indicator at the top-left corner of a new cell.

theorem pinch_diff_TL (S : Finset (ℤ × ℤ)) (x y : ℤ) (hc : (x, y) ∉ S) :
    pinchW (insert (x, y) S) (x, y + 1) - pinchW S (x, y + 1)
      = (if ((x - 1, y + 1) ∈ S ∧ (x, y + 1) ∉ S ∧ (x - 1, y) ∉ S) then (1 : ℤ) else 0)
        - (if ((x, y + 1) ∈ S ∧ (x - 1, y) ∈ S ∧ (x - 1, y + 1) ∉ S) then (1 : ℤ) else 0)
Uses 2 · Used by 1
Statement usesPinch point indicator
Proof usesPinch point of a set of unit cells
Used byChange of the pinch count in terms of eight neighbours

TheoremChange of the pinch indicator at the top-right corner of a new cell#✓fully proved

Change of the pinch indicator at the top-right corner of a new cell.

theorem pinch_diff_TR (S : Finset (ℤ × ℤ)) (x y : ℤ) (hc : (x, y) ∉ S) :
    pinchW (insert (x, y) S) (x + 1, y + 1) - pinchW S (x + 1, y + 1)
      = (if ((x + 1, y + 1) ∈ S ∧ (x, y + 1) ∉ S ∧ (x + 1, y) ∉ S) then (1 : ℤ) else 0)
        - (if ((x, y + 1) ∈ S ∧ (x + 1, y) ∈ S ∧ (x + 1, y + 1) ∉ S) then (1 : ℤ) else 0)
Uses 2 · Used by 1
Statement usesPinch point indicator
Proof usesPinch point of a set of unit cells
Used byChange of the pinch count in terms of eight neighbours

TheoremChange of the pinch count in terms of eight neighbours#✓fully proved

The change of the pinch count when a cell is added, in terms of its eight neighbours.

theorem pinch_jump_sum (S : Finset (ℤ × ℤ)) (x y : ℤ) (hc : (x, y) ∉ S) :
    (∑ v ∈ cornersOf (x, y), (pinchW (insert (x, y) S) v - pinchW S v))
      = pinchDelta (decide ((x + 1, y) ∈ S)) (decide ((x - 1, y) ∈ S)) (decide ((x, y + 1) ∈ S))
          (decide ((x, y - 1) ∈ S)) (decide ((x + 1, y + 1) ∈ S)) (decide ((x - 1, y + 1) ∈ S))
          (decide ((x + 1, y - 1) ∈ S)) (decide ((x - 1, y - 1) ∈ S))
Uses 8 · Used by 1
Statement usesFour corners of a unit cell · Local change of the number of pinch points · Pinch point indicator
Proof usesIndicator of a Boolean · Change of the pinch indicator at the bottom-left corner of a new cell · Change of the pinch indicator at the bottom-right corner of a new cell · Change of the pinch indicator at the top-left corner of a new cell · Change of the pinch indicator at the top-right corner of a new cell
Used byCell Gauss–Bonnet formula

TheoremCell Gauss–Bonnet formula#✓fully proved

Cell Gauss–Bonnet formula: for every finite set of unit cells, convex corners minus reflex corners equals four times the Euler characteristic plus twice the number of pinch points.

theorem cornerDiff_eq (S : Finset (ℤ × ℤ)) :
    cornerDiff S = 4 * eulerChar S + 2 * pinchCount S
Uses 23 · Used by 3
Statement usesCorner defect of a set of unit cells · Euler characteristic of a cell complex · Number of pinch points
Proof usesChange of the corner defect in terms of eight neighbours · New edges of an added cell match the local count · New vertices of an added cell match the local count · Vertices of a cell complex · Corner count of a lattice point · Four corners of a unit cell · Edges of a cell complex · Change of the corner defect when a cell is added · Corner weight of a vertex · Four edges of a unit cell · Change of the Euler characteristic when a cell is added · Number of new edges when a cell is added · Number of new vertices when a cell is added · Local change of the corner defect · Local cell Gauss–Bonnet identity · Local change of the number of pinch points · Corrected right side of the local Gauss–Bonnet identity · Change of the pinch count in terms of eight neighbours · Pinch count changes only at the corners of a new cell · Pinch point indicator
Used byFour left turns from a pinch-free interior of Euler characteristic 1 · Discrete Umlaufsatz for walks of length at least three, shifted form · Hopf's Umlaufsatz
98 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.