Extending an existing straight overlay

The final component-joining step of the local-grid construction starts from an already subdivided straight inner overlay and appends one polygonal joining arc. Reusing the original source pieces would lose the old cut points. Instead, this module lists the current overlay edges as the new source pieces and retains every current vertex as a prescribed cut point.

The resulting overlay is automatically a plane subdivision of the old overlay. This is the finite straight-line engine needed before the wild outer graph and the joining ear are glued.

theorem Schoenflies.IsPlaneSubdivisionExtension.trans {β : Type u_1} {δ : Type u_2} {κ : Type u_3} {G : Graph Plane β} {Gdraw : β → ℝ → Plane} {H : Graph Plane δ} {Hdraw : δ → ℝ → Plane} {K : Graph Plane κ} {Kdraw : κ → ℝ → Plane} (hGH : IsPlaneSubdivisionExtension G Gdraw H Hdraw) (hHK : IsPlaneSubdivisionExtension H Hdraw K Kdraw) : IsPlaneSubdivisionExtension G Gdraw K Kdraw

Plane subdivision extensions compose. At a point of an old edge away from final vertices, the intermediate carrier supplies an intermediate edge; both absorption clauses then apply.

noncomputable def Schoenflies.currentOverlayPieces (pieces : List Piece) (extra : List Plane) : List Piece

The already-subdivided edges of a finite straight overlay, listed as pieces.

Equations

• Schoenflies.currentOverlayPieces pieces extra = (Schoenflies.attachGraph pieces extra).edgeFinset.toList

@[simp]

theorem Schoenflies.mem_currentOverlayPieces {pieces : List Piece} {extra : List Plane} {R : Piece} : R ∈ currentOverlayPieces pieces extra ↔ R ∈ (attachGraph pieces extra).edgeSet

noncomputable def Schoenflies.extendedOverlayPieces (pieces : List Piece) (extra : List Plane) (joins : List Piece) : List Piece

Append further straight pieces to the current overlay edge list.

Equations

• Schoenflies.extendedOverlayPieces pieces extra joins = Schoenflies.currentOverlayPieces pieces extra ++ joins

noncomputable def Schoenflies.extendOverlay (pieces : List Piece) (extra : List Plane) (joins : List Piece) : Graph Plane Piece

Re-overlay the current straight graph together with the joining pieces, retaining every old vertex as a cut point.

Equations

• Schoenflies.extendOverlay pieces extra joins = Schoenflies.attachGraph (Schoenflies.extendedOverlayPieces pieces extra joins) (Schoenflies.attachGraph pieces extra).vertexFinset.toList

instance Schoenflies.extendOverlay_finite (pieces : List Piece) (extra : List Plane) (joins : List Piece) : (extendOverlay pieces extra joins).Finite

theorem Schoenflies.currentOverlayPieces_nondeg {pieces : List Piece} {extra : List Plane} (hpieces : ∀ R ∈ pieces, R.Nondeg) (R : Piece) : R ∈ currentOverlayPieces pieces extra → R.Nondeg

Every current overlay edge is nondegenerate.

theorem Schoenflies.cover_currentOverlayPieces (pieces : List Piece) (extra : List Plane) : cover (currentOverlayPieces pieces extra) = (attachGraph pieces extra).pointSet segmentDrawing

The edge list of the current overlay has exactly the current overlay's carrier.

theorem Schoenflies.extendOverlay_pointSet (pieces : List Piece) (extra : List Plane) (joins : List Piece) : (extendOverlay pieces extra joins).pointSet segmentDrawing = (attachGraph pieces extra).pointSet segmentDrawing ∪ cover joins

The extended overlay occupies exactly the old carrier together with the joining carrier.

theorem Schoenflies.extendOverlay_isDrawing {pieces : List Piece} {extra : List Plane} {joins : List Piece} (hpieces : ∀ R ∈ pieces, R.Nondeg) (hjoins : ∀ R ∈ joins, R.Nondeg) : (extendOverlay pieces extra joins).IsDrawing segmentDrawing

The extended overlay is a finite straight-line plane graph.

theorem Schoenflies.attachGraphVertices_subset_extendOverlay {pieces : List Piece} {extra : List Plane} {joins : List Piece} (hpieces : ∀ R ∈ pieces, R.Nondeg) (hjoins : ∀ R ∈ joins, R.Nondeg) : (attachGraph pieces extra).vertexSet ⊆ (extendOverlay pieces extra joins).vertexSet

Every old overlay vertex is retained by the extended overlay.

theorem Schoenflies.extendOverlay_edge_subset {pieces : List Piece} {extra : List Plane} {joins : List Piece} (hpieces : ∀ R ∈ pieces, R.Nondeg) (hjoins : ∀ R ∈ joins, R.Nondeg) {A : Piece} : A ∈ (attachGraph pieces extra).edgeSet → ∀ {R : Piece}, R ∈ (extendOverlay pieces extra joins).edgeSet → (Graph.edgeArc segmentDrawing R ∩ (Graph.edgeArc segmentDrawing A \ (extendOverlay pieces extra joins).vertexSet)).Nonempty → Graph.edgeArc segmentDrawing R ⊆ Graph.edgeArc segmentDrawing A

A new overlay edge meeting an old straight edge away from new vertices is one of its subdivision pieces.

theorem Schoenflies.extendOverlay_edge_source {pieces : List Piece} {extra : List Plane} {joins : List Piece} {R : Piece} (hR : R ∈ (extendOverlay pieces extra joins).edgeSet) : (∃ A ∈ (attachGraph pieces extra).edgeSet, R.seg ⊆ A.seg) ∨ ∃ A ∈ joins, R.seg ⊆ A.seg

Every edge of the extended overlay is cut either from a current overlay edge or from one of the newly appended pieces.

theorem Schoenflies.attachGraph_isPlaneSubdivisionExtension_extendOverlay {pieces : List Piece} {extra : List Plane} {joins : List Piece} (hpieces : ∀ R ∈ pieces, R.Nondeg) (hjoins : ∀ R ∈ joins, R.Nondeg) : IsPlaneSubdivisionExtension (attachGraph pieces extra) segmentDrawing (extendOverlay pieces extra joins) segmentDrawing

Re-overlaying after adjoining joining pieces is a plane subdivision extension of the current straight overlay.

theorem Schoenflies.attachGraphTrace_isTwoConnected_extendOverlay {pieces : List Piece} {extra : List Plane} {joins : List Piece} (hpieces : ∀ R ∈ pieces, R.Nondeg) (hjoins : ∀ R ∈ joins, R.Nondeg) (htwo : (attachGraph pieces extra).IsTwoConnected) : ((extendOverlay pieces extra joins).traceGraph segmentDrawing ((attachGraph pieces extra).pointSet segmentDrawing)).IsTwoConnected

In particular, a 2-connected current overlay remains 2-connected on its exact traced carrier after adjoining and subdividing the joining pieces.