The polygonal overlay, assembled into a plane graph

Schoenflies/Overlay.lean does the separating half of lem:polygonal-overlay: after cutting at the right points, two pieces of the subdivision whose interiors meet are the same segment, in one order or the other. This module turns that into a plane graph.

The only thing standing between "the same segment" and "the same edge" is that a segment has two names, (a, b) and (b, a). orientPiece removes the choice by fixing a total order on plane points — Precedes, lexicographic in the coordinates — and putting the smaller end first. Two names for one segment then orient to the same name, so "represent each duplicated subsegment once" stops being deduplication up to reversal and becomes deduplication up to equality, which List.dedup does without knowing any geometry. Nothing geometric rests on which order it is: only precedes_total and eq_of_precedes_of_precedes are ever used.

The graph is overlayGraph, a Graph Plane Piece: its edges are the oriented, deduplicated pieces, and its vertices are their ends. IsLink P x y says that P is an edge and that x and y are its two ends in one order or the other — which is why eq_or_eq_of_isLink_of_isLink is a two-line case split rather than an argument.

The three clauses of Graph.IsDrawing come out as follows.

• Each edge is drawn by an arc between its ends — isArcBetween_segment, given nondegeneracy, which subdivide_ne preserves and orienting does not disturb.
• An edge's arc meets the vertex set only at its own ends — a vertex is an end of some edge, hence a cut point, and subdivide_avoids says a cut point is interior to nothing.
• Distinct edges meet only at shared vertices — a common point that is an end of neither would be interior to both, and subdivide_separated would make the two pieces the same segment, hence (after orienting) the same name. Once it is an end of one it is a cut point, so it cannot be interior to the other either, and it is an end of both.

Blueprint

• Precedes, orientPiece — the canonical orientation of a segment.
• overlayPieces, overlayGraph, segmentDrawing — the graph of Lemma 3.7.
• polygonal_overlay — Lemma 3.7 (polygonal overlay), the whole statement.

A total order on plane points

It exists to pick one of two points canonically. Only two facts about it are used: that it compares any two points, and that it cannot rank two distinct points both ways round.

def Schoenflies.Precedes (p q : Plane) : Prop

The lexicographic order on plane points: first coordinate, then second.

Equations

• Schoenflies.Precedes p q = (p.ofLp 0 < q.ofLp 0 ∨ p.ofLp 0 = q.ofLp 0 ∧ p.ofLp 1 ≤ q.ofLp 1)

theorem Schoenflies.precedes_total (p q : Plane) : Precedes p q ∨ Precedes q p

theorem Schoenflies.eq_of_precedes_of_precedes {p q : Plane} (h : Precedes p q) (h' : Precedes q p) : p = q

The canonical orientation of a piece

noncomputable def Schoenflies.orientPiece (P : Piece) : Piece

A piece with its ends in lexicographic order. Two names for one segment orient to the same name; that is the whole purpose.

Equations

• Schoenflies.orientPiece P = if Schoenflies.Precedes P.1 P.2 then P else (P.2, P.1)

theorem Schoenflies.orientPiece_of_precedes {P : Piece} (h : Precedes P.1 P.2) : orientPiece P = P

theorem Schoenflies.orientPiece_of_not_precedes {P : Piece} (h : ¬Precedes P.1 P.2) : orientPiece P = (P.2, P.1)

@[simp]

theorem Schoenflies.orientPiece_seg (P : Piece) : (orientPiece P).seg = P.seg

Orienting does not move the segment.

@[simp]

theorem Schoenflies.orientPiece_interior (P : Piece) : (orientPiece P).interior = P.interior

Nor the interior.

theorem Schoenflies.orientPiece_ends (P : Piece) (z : Plane) : z = (orientPiece P).1 ∨ z = (orientPiece P).2 ↔ z = P.1 ∨ z = P.2

Nor which points are its ends.

theorem Schoenflies.orientPiece_nondeg {P : Piece} (h : P.Nondeg) : (orientPiece P).Nondeg

theorem Schoenflies.precedes_orientPiece (P : Piece) : Precedes (orientPiece P).1 (orientPiece P).2

The output is oriented — which is what makes orientPiece idempotent.

@[simp]

theorem Schoenflies.orientPiece_idem (P : Piece) : orientPiece (orientPiece P) = orientPiece P

@[simp]

theorem Schoenflies.orientPiece_swap (P : Piece) : orientPiece (P.2, P.1) = orientPiece P

Orienting forgets the name it was given. This is the fact that makes deduplication carry no geometry.

Deduplication

cover only sees which pieces are in the list, so both steps of the assembly — orienting and deduplicating — leave it alone.

theorem Schoenflies.cover_eq_of_mem_iff {l₁ l₂ : List Piece} (h : ∀ (P : Piece), P ∈ l₁ ↔ P ∈ l₂) : cover l₁ = cover l₂

theorem Schoenflies.cover_map_orientPiece (l : List Piece) : cover (List.map orientPiece l) = cover l

noncomputable def Schoenflies.overlayPieces (pieces : List Piece) (points : List Plane) : List Piece

The edges of the overlay: the pieces of the subdivision, oriented and then deduplicated. Orienting is what makes the deduplication a plain list operation.

Equations

• Schoenflies.overlayPieces pieces points = (List.map Schoenflies.orientPiece (Schoenflies.subdivide pieces points)).dedup

theorem Schoenflies.mem_overlayPieces {pieces : List Piece} {points : List Plane} {P : Piece} : P ∈ overlayPieces pieces points ↔ ∃ Q ∈ subdivide pieces points, orientPiece Q = P

theorem Schoenflies.overlayPieces_nodup (pieces : List Piece) (points : List Plane) : (overlayPieces pieces points).Nodup

The list of edges has no duplicates.

theorem Schoenflies.overlayPieces_cover (pieces : List Piece) (points : List Plane) : cover (overlayPieces pieces points) = cover pieces

Neither orienting nor deduplicating changes what the pieces occupy.

theorem Schoenflies.overlayPieces_nondeg {pieces : List Piece} (points : List Plane) (hnd : ∀ P ∈ pieces, P.Nondeg) (P : Piece) : P ∈ overlayPieces pieces points → P.Nondeg

theorem Schoenflies.overlayPieces_ends_cut {pieces : List Piece} {points : List Plane} (hEnds : EndsAreCut pieces points) (P : Piece) : P ∈ overlayPieces pieces points → ∀ (z : Plane), z = P.1 ∨ z = P.2 → z ∈ points

Every end of every edge is a cut point: orienting does not change which points are ends, and subdivide_ends_are_cuts covers the subdivision.

theorem Schoenflies.overlayPieces_avoids {pieces : List Piece} {points : List Plane} (hnd : ∀ P ∈ pieces, P.Nondeg) (p : Plane) : p ∈ points → ∀ P ∈ overlayPieces pieces points, p ∉ P.interior

And a cut point is interior to no edge.

theorem Schoenflies.overlayPieces_disjoint_interiors {pieces : List Piece} {points : List Plane} (hnd : ∀ P ∈ pieces, P.Nondeg) (hEnds : EndsAreCut pieces points) (hMeets : MeetsAreCut pieces points) {P Q : Piece} (hP : P ∈ overlayPieces pieces points) (hQ : Q ∈ overlayPieces pieces points) (hPQ : P ≠ Q) {x : Plane} (hxP : x ∈ P.interior) : x ∉ Q.interior

Distinct edges have disjoint interiors. This is where separation is spent: two pieces sharing an interior point are the same segment, so after orienting they are the same name, and a deduplicated list holds a name once.

The graph

def Schoenflies.endSet (edges : List Piece) : Set Plane

The ends of a list of pieces.

Equations

• Schoenflies.endSet edges = {v : Schoenflies.Plane | ∃ P ∈ edges, v = P.1 ∨ v = P.2}

noncomputable def Schoenflies.overlayGraph (pieces : List Piece) (points : List Plane) : Graph Plane Piece

The overlay graph: the oriented deduplicated pieces as edges, their ends as vertices.

An edge links x and y exactly when they are its two ends in one order or the other, which is what makes eq_or_eq_of_isLink_of_isLink a case split with no content.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Schoenflies.overlayGraph_vertexSet {pieces : List Piece} {points : List Plane} : (overlayGraph pieces points).vertexSet = endSet (overlayPieces pieces points)

@[simp]

theorem Schoenflies.overlayGraph_mem_edgeSet {pieces : List Piece} {points : List Plane} {P : Piece} : P ∈ (overlayGraph pieces points).edgeSet ↔ P ∈ overlayPieces pieces points

@[simp]

theorem Schoenflies.overlayGraph_isLink {pieces : List Piece} {points : List Plane} {P : Piece} {x y : Plane} : (overlayGraph pieces points).IsLink P x y ↔ P ∈ overlayPieces pieces points ∧ (x = P.1 ∧ y = P.2 ∨ x = P.2 ∧ y = P.1)

theorem Schoenflies.overlayGraph_mem_vertexSet {pieces : List Piece} {points : List Plane} {v : Plane} : v ∈ (overlayGraph pieces points).vertexSet ↔ ∃ P ∈ overlayPieces pieces points, v = P.1 ∨ v = P.2

theorem Schoenflies.overlayGraph_inc {pieces : List Piece} {points : List Plane} {P : Piece} {v : Plane} (hP : P ∈ overlayPieces pieces points) (h : v = P.1 ∨ v = P.2) : (overlayGraph pieces points).Inc P v

An end of an edge is a vertex.

The drawing

A straight edge is drawn by the affine parametrization of its segment, so the arc clause of IsDrawing is isArcBetween_segment and nothing else.

noncomputable def Schoenflies.segmentDrawing (P : Piece) : ℝ → Plane

Every piece is drawn by the affine parametrization of its segment.

Equations

• Schoenflies.segmentDrawing P = ⇑(AffineMap.lineMap P.1 P.2)

@[simp]

theorem Schoenflies.edgeArc_segmentDrawing (P : Piece) : Graph.edgeArc segmentDrawing P = P.seg

theorem Schoenflies.overlayGraph_isDrawing (pieces : List Piece) (points : List Plane) (hnd : ∀ P ∈ pieces, P.Nondeg) (hEnds : EndsAreCut pieces points) (hMeets : MeetsAreCut pieces points) : (overlayGraph pieces points).IsDrawing segmentDrawing

The overlay graph is a plane graph.

theorem Schoenflies.overlayGraph_pointSet (pieces : List Piece) (points : List Plane) : (overlayGraph pieces points).pointSet segmentDrawing = cover pieces

What the graph occupies is what its edges occupy: every vertex is an end of an edge, so the vertices add nothing.

Finiteness

Without this the whole face and outer-face machinery of Schoenflies/Graph/Drawing.lean and Schoenflies/Graph/OuterFace.lean is inapplicable to the overlay, since every statement there carries a [G.Finite] instance. Both sets come from one finite list, so it is immediate — but it has to be said, and the instance has to be found by typeclass search at the call site.

theorem Schoenflies.finite_endSet (edges : List Piece) : (endSet edges).Finite

instance Schoenflies.overlayGraph_finite (pieces : List Piece) (points : List Plane) : (overlayGraph pieces points).Finite

theorem Schoenflies.polygonal_overlay (pieces : List Piece) (hnd : ∀ P ∈ pieces, P.Nondeg) : ∃ (G : Graph Plane Piece), G.Finite ∧ G.IsDrawing segmentDrawing ∧ G.pointSet segmentDrawing = cover pieces

Lemma 3.7 (polygonal overlay). Finitely many nondegenerate segments are the point set of a finite plane graph.

The finiteness clause is not decoration. Every statement about faces and about the outer face carries a [G.Finite] instance, and an existential that produced only IsDrawing would hide the graph behind a binder with no way to recover the instance — so the overlay could not be fed to the face machinery at all.