Subdividing a list of segments

A polygonal edge is its pair of endpoints: a straight segment is determined by its ends, so naming one by anything else names a distinction that does not exist. Piece := Plane × Plane, and the blueprint's "represent every duplicate geometric subsegment only once" becomes deduplication of a list of names, with no geometry in it.

The subdivision recurses on the POINT list, not on the segment. subdivide pieces points cuts every current piece at the head point and recurses with the rest. Read literally the blueprint wants the cut points as data, which would need a choice operator (the meets are existential) and then a sort (to order them along each segment). Neither is required: order does not matter, because cutting at a point that has already become an endpoint is a no-op.

Three facts about one cut, each lifted across the piece list and then across the point list:

• subdivide_cover — cutting loses nothing, so a subdivision occupies what it came from;
• subdivide_ne — no piece degenerates, so the drawing condition's invariant survives;
• subdivide_interior_subset — every piece's interior lies inside the interior of a piece it came from. This is what makes a cut permanent: nothing later can put a removed point back into an interior.

Blueprint

• Piece, cover — the segment representation and what a list of them occupies.
• subdivide and its three properties — the cutting half of Lemma 3.7 (polygonal overlay).

@[reducible, inline]

abbrev Schoenflies.Piece : Type

A polygonal edge is its pair of endpoints.

Equations

• Schoenflies.Piece = (Schoenflies.Plane × Schoenflies.Plane)

def Schoenflies.Piece.seg (P : Piece) : Set Plane

The closed segment a piece occupies.

Equations

• P.seg = segment ℝ P.1 P.2

def Schoenflies.Piece.interior (P : Piece) : Set Plane

The interior of a piece.

Equations

• P.interior = openSegment ℝ P.1 P.2

def Schoenflies.Piece.Nondeg (P : Piece) : Prop

A piece is nondegenerate when its two ends differ.

Equations

• P.Nondeg = (P.1 ≠ P.2)

def Schoenflies.cover (pieces : List Piece) : Set Plane

What a list of pieces occupies.

Equations

• Schoenflies.cover pieces = ⋃ P ∈ pieces, P.seg

@[simp]

theorem Schoenflies.cover_nil : cover [] = ∅

@[simp]

theorem Schoenflies.cover_cons (P : Piece) (ps : List Piece) : cover (P :: ps) = P.seg ∪ cover ps

theorem Schoenflies.cover_append (ps qs : List Piece) : cover (ps ++ qs) = cover ps ∪ cover qs

theorem Schoenflies.cover_flatMap (f : Piece → List Piece) (ps : List Piece) : cover (List.flatMap f ps) = ⋃ P ∈ ps, cover (f P)

One cut

noncomputable def Schoenflies.splitAt (p : Plane) (P : Piece) : List Piece

Cut one piece at one point: two pieces if the point is interior to it, and the piece unchanged otherwise. Cutting at a point that is already an endpoint is a no-op.

Equations

• Schoenflies.splitAt p P = if p ∈ P.interior then [(P.1, p), (p, P.2)] else [P]

theorem Schoenflies.splitAt_cover (p : Plane) (P : Piece) : cover (splitAt p P) = P.seg

theorem Schoenflies.splitAt_ne (p : Plane) {P : Piece} (hP : P.Nondeg) (Q : Piece) : Q ∈ splitAt p P → Q.Nondeg

Cutting at an interior point leaves both halves nondegenerate: an interior point differs from both ends.

theorem Schoenflies.splitAt_interior_subset (p : Plane) (P Q : Piece) : Q ∈ splitAt p P → Q.interior ⊆ P.interior

Cutting is permanent: each half's interior lies inside the whole's.

theorem Schoenflies.splitAt_avoids (p : Plane) {P : Piece} (hP : P.Nondeg) (Q : Piece) : Q ∈ splitAt p P → p ∉ Q.interior

After cutting at p, no piece has p in its interior.

Nondegeneracy is needed: a degenerate piece (p, p) has p in its interior and cutting it produces two more copies of itself.

One cut, across the whole list

noncomputable def Schoenflies.splitAllAt (p : Plane) (pieces : List Piece) : List Piece

Cut every piece of the list at one point.

Equations

• Schoenflies.splitAllAt p pieces = List.flatMap (Schoenflies.splitAt p) pieces

theorem Schoenflies.splitAllAt_cover (p : Plane) (pieces : List Piece) : cover (splitAllAt p pieces) = cover pieces

theorem Schoenflies.splitAllAt_ne (p : Plane) {pieces : List Piece} (h : ∀ P ∈ pieces, P.Nondeg) (Q : Piece) : Q ∈ splitAllAt p pieces → Q.Nondeg

theorem Schoenflies.splitAllAt_interior_subset (p : Plane) (pieces : List Piece) (Q : Piece) : Q ∈ splitAllAt p pieces → ∃ P ∈ pieces, Q.interior ⊆ P.interior

theorem Schoenflies.splitAllAt_avoids (p : Plane) {pieces : List Piece} (h : ∀ P ∈ pieces, P.Nondeg) (Q : Piece) : Q ∈ splitAllAt p pieces → p ∉ Q.interior

The subdivision

noncomputable def Schoenflies.subdivide (pieces : List Piece) : List Plane → List Piece

Subdivide a list of pieces at a list of points, recursing on the POINT list: cut every current piece at the head, then carry on with the tail.

Equations

• Schoenflies.subdivide pieces [] = pieces
• Schoenflies.subdivide pieces (p :: ps) = Schoenflies.subdivide (Schoenflies.splitAllAt p pieces) ps

@[simp]

theorem Schoenflies.subdivide_nil (pieces : List Piece) : subdivide pieces [] = pieces

@[simp]

theorem Schoenflies.subdivide_cons (pieces : List Piece) (p : Plane) (ps : List Plane) : subdivide pieces (p :: ps) = subdivide (splitAllAt p pieces) ps

theorem Schoenflies.subdivide_cover (pieces : List Piece) (points : List Plane) : cover (subdivide pieces points) = cover pieces

Cutting loses nothing: a subdivision occupies exactly what it came from.

theorem Schoenflies.subdivide_ne {pieces : List Piece} (points : List Plane) (h : ∀ P ∈ pieces, P.Nondeg) (Q : Piece) : Q ∈ subdivide pieces points → Q.Nondeg

No piece degenerates.

theorem Schoenflies.subdivide_interior_subset (pieces : List Piece) (points : List Plane) (Q : Piece) : Q ∈ subdivide pieces points → ∃ P ∈ pieces, Q.interior ⊆ P.interior

Every piece's interior lies inside the interior of a piece it came from. This is what makes a cut permanent.

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

After subdividing, no cut point is interior to any piece. Permanence is what makes this work: a later cut only shrinks interiors, so a point removed early stays removed.