Finite segment overlays on the source side

The outer source curve is deliberately not polygonal, but every nonouter source edge of a generated pair is polygonal. This module extracts an exact finite straight-segment cover of that compact nonboundary carrier and overlays it with the local window grid. It is the finite geometric core of the forward half of the quantitative-refinement recursion.

Blueprint

• Schoenflies.SourceNonboundarySegmentCover — an exact finite segment presentation of the current source nonboundary skeleton.
• Schoenflies.GeneratedPair.exists_sourceNonboundarySegmentCover — every generated pair has such a presentation.
• Schoenflies.SourceNonboundarySegmentCover.localOverlay — the old compact source core overlaid with one fine local grid.
• Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.graph — the finite inner overlay, freshly relabelled and adjoined to the old wild outer graph.
• Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.isSourceExtension — all local source-extension fields, leaving only the two global attachment properties explicit.
• Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling. isSourceExtension_of_source_connected_two_common — the global properties follow from the carried source-connectedness invariant and two distinct common source/grid vertices.

theorem Schoenflies.Graph.isDrawing_congr_of_eqOn {β : Type u_1} {G : Graph Plane β} {drawing drawing' : β → ℝ → Plane} (h : G.IsDrawing drawing) (heq : ∀ {e : β}, e ∈ G.edgeSet → drawing' e = drawing e) : G.IsDrawing drawing'

Replacing a drawing by a pointwise equal parametrization on the graph's own edges preserves all drawing axioms.

theorem Schoenflies.Graph.isDrawing_union_of_common_vertices {β : Type u_1} {G H : Graph Plane β} {drawing : β → ℝ → Plane} (hG : G.IsDrawing drawing) (hH : H.IsDrawing drawing) (hcompat : G.Compatible H) (hcross : ∀ {p : Plane}, p ∈ G.pointSet drawing → p ∈ H.pointSet drawing → p ∈ G.vertexSet ∧ p ∈ H.vertexSet) : (G.union H).IsDrawing drawing

Compatible plane drawings whose carriers meet only at common vertices form a plane drawing on their union.

theorem Schoenflies.Graph.IsDrawing.isConnected_edgesCover_of_isWalk {β : Type u_1} {G : Graph Plane β} {drawing : β → ℝ → Plane} (h : G.IsDrawing drawing) {u v : Plane} {W : List β} (hW : G.IsWalk u W v) (hne : W ≠ []) : IsConnected (Graph.edgesCover drawing W)

A nonempty walk in a plane drawing has connected geometric carrier.

theorem Schoenflies.Graph.IsDrawing.isConnected_pointSet {β : Type u_1} {G : Graph Plane β} {drawing : β → ℝ → Plane} (h : G.IsDrawing drawing) (hG : G.Connected) : IsConnected (G.pointSet drawing)

The point set of a connected plane drawing is connected.

structure Schoenflies.SourceNonboundarySegmentCover {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) : Type

A finite exact straight-segment presentation of the compact nonboundary source skeleton.

• pieces : List Piece

  The straight segments covering the nonboundary carrier.

• nondeg (Q : Piece) : Q ∈ self.pieces → Q.Nondeg

  No listed segment is degenerate.

• cover_eq : cover self.pieces = P.sourceNonboundaryGraph.pointSet P.src.drawing

  The listed segments occupy exactly the compact nonboundary source graph.

• source (Q : Piece) : Q ∈ self.pieces → ∃ e ∈ P.str.skel.edgeSet, e ∉ P.str.outerGraph.edgeSet ∧ Q.seg ⊆ Graph.edgeArc P.src.drawing e

  Every listed segment came from one old nonouter source edge.

theorem Schoenflies.GeneratedPair.exists_sourceNonboundarySegmentCover {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) : Nonempty (SourceNonboundarySegmentCover P)

Every generated pair has a finite exact segment presentation of its compact polygonal nonboundary source skeleton.

noncomputable def Schoenflies.SourceNonboundarySegmentCover.localPieces {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} (Q : SourceNonboundarySegmentCover P) (p : Plane) (s epsilon : ℝ) : List Piece

The two finite segment families in the source local-grid overlay.

Equations

• Q.localPieces p s epsilon = Q.pieces ++ Schoenflies.localGridEdges p s (Schoenflies.localGridCount s epsilon)

noncomputable def Schoenflies.SourceNonboundarySegmentCover.localOverlay {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} (Q : SourceNonboundarySegmentCover P) (p : Plane) (s epsilon : ℝ) (extra : List Plane) : Graph Plane Piece

The compact old source core overlaid with a fine local grid. Old nonboundary vertices and any prescribed attachment points are retained as overlay vertices.

Equations

• Q.localOverlay p s epsilon extra = Schoenflies.attachGraph (Q.localPieces p s epsilon) (extra ++ P.sourceNonboundaryGraph.vertexFinset.toList)

instance Schoenflies.SourceNonboundarySegmentCover.localOverlay_finite {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} (Q : SourceNonboundarySegmentCover P) (p : Plane) (s epsilon : ℝ) (extra : List Plane) : (Q.localOverlay p s epsilon extra).Finite

theorem Schoenflies.SourceNonboundarySegmentCover.localPieces_nondeg {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} (Q : SourceNonboundarySegmentCover P) {p : Plane} {s epsilon : ℝ} (hs : 0 < s) (R : Piece) : R ∈ Q.localPieces p s epsilon → R.Nondeg

Every source segment of the local overlay is nondegenerate.

theorem Schoenflies.SourceNonboundarySegmentCover.localOverlay_isDrawing {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} (Q : SourceNonboundarySegmentCover P) {p : Plane} {s epsilon : ℝ} (hs : 0 < s) (extra : List Plane) : (Q.localOverlay p s epsilon extra).IsDrawing segmentDrawing

The source local overlay is a finite straight-line plane graph.

theorem Schoenflies.SourceNonboundarySegmentCover.localOverlay_pointSet {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} (Q : SourceNonboundarySegmentCover P) (p : Plane) (s epsilon : ℝ) (extra : List Plane) : (Q.localOverlay p s epsilon extra).pointSet segmentDrawing = P.sourceNonboundaryGraph.pointSet P.src.drawing ∪ cover (localGridEdges p s (localGridCount s epsilon))

The local overlay occupies exactly the old compact source core together with the grid.

theorem Schoenflies.SourceNonboundarySegmentCover.sourceCore_subset_localOverlay {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} (Q : SourceNonboundarySegmentCover P) (p : Plane) (s epsilon : ℝ) (extra : List Plane) : P.sourceNonboundaryGraph.pointSet P.src.drawing ⊆ (Q.localOverlay p s epsilon extra).pointSet segmentDrawing

The whole old compact source core is retained by the local overlay.

theorem Schoenflies.SourceNonboundarySegmentCover.localGrid_subset_localOverlay {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} (Q : SourceNonboundarySegmentCover P) (p : Plane) (s epsilon : ℝ) (extra : List Plane) : cover (localGridEdges p s (localGridCount s epsilon)) ⊆ (Q.localOverlay p s epsilon extra).pointSet segmentDrawing

The whole fine local grid is retained by the source overlay.

theorem Schoenflies.SourceNonboundarySegmentCover.localGridVertices_subset_localOverlay {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} (Q : SourceNonboundarySegmentCover P) {p : Plane} {s epsilon : ℝ} (hs : 0 < s) (extra : List Plane) : (localGrid p s (localGridCount s epsilon)).vertexSet ⊆ (Q.localOverlay p s epsilon extra).vertexSet

Every vertex of the raw local grid is retained as a vertex of the combined straight-line overlay.

theorem Schoenflies.SourceNonboundarySegmentCover.localOverlay_grid_edge_subset {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} (Q : SourceNonboundarySegmentCover P) {p : Plane} {s epsilon : ℝ} (hs : 0 < s) (extra : List Plane) {A : Piece} : A ∈ (localGrid p s (localGridCount s epsilon)).edgeSet → ∀ {R : Piece}, R ∈ (Q.localOverlay p s epsilon extra).edgeSet → (Graph.edgeArc segmentDrawing R ∩ (Graph.edgeArc segmentDrawing A \ (Q.localOverlay p s epsilon extra).vertexSet)).Nonempty → Graph.edgeArc segmentDrawing R ⊆ Graph.edgeArc segmentDrawing A

Away from overlay vertices, an overlay edge meeting a raw local-grid edge is one of its subdivision pieces.

theorem Schoenflies.SourceNonboundarySegmentCover.localGrid_isPlaneSubdivisionExtension {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} (Q : SourceNonboundarySegmentCover P) {p : Plane} {s epsilon : ℝ} (hs : 0 < s) (extra : List Plane) : IsPlaneSubdivisionExtension (localGrid p s (localGridCount s epsilon)) segmentDrawing (Q.localOverlay p s epsilon extra) segmentDrawing

The straight-line local overlay contains a plane subdivision of the raw local grid.

theorem Schoenflies.SourceNonboundarySegmentCover.localOverlay_edge_source {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} (Q : SourceNonboundarySegmentCover P) {p : Plane} {s epsilon : ℝ} {extra : List Plane} {R : Piece} (hR : R ∈ (Q.localOverlay p s epsilon extra).edgeSet) : (∃ A ∈ Q.pieces, R.seg ⊆ A.seg) ∨ ∃ A ∈ localGridEdges p s (localGridCount s epsilon), R.seg ⊆ A.seg

Every edge of the source local overlay is a subsegment either of the old nonboundary source cover or of the local grid.

theorem Schoenflies.SourceNonboundarySegmentCover.sourceCoreVertices_subset_localOverlay {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} (Q : SourceNonboundarySegmentCover P) {p : Plane} {s epsilon : ℝ} (hs : 0 < s) (extra : List Plane) : P.sourceNonboundaryGraph.vertexSet ⊆ (Q.localOverlay p s epsilon extra).vertexSet

Every vertex of the compact old source core is explicitly retained as a vertex of the local overlay.

theorem Schoenflies.SourceNonboundarySegmentCover.sourceNonboundaryGraph_edge_mem {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {e : γ} (he : e ∈ P.str.skel.edgeSet) (heOuter : e ∉ P.str.outerGraph.edgeSet) : e ∈ P.sourceNonboundaryGraph.edgeSet

Every old nonouter edge belongs to the compact source-core graph.

theorem Schoenflies.SourceNonboundarySegmentCover.localOverlay_edge_subset {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} (Q : SourceNonboundarySegmentCover P) {p : Plane} {s epsilon : ℝ} (hs : 0 < s) (extra : List Plane) {e : γ} : e ∈ P.str.skel.edgeSet → e ∉ P.str.outerGraph.edgeSet → ∀ {R : Piece}, R ∈ (Q.localOverlay p s epsilon extra).edgeSet → (Graph.edgeArc segmentDrawing R ∩ (P.src.cell e \ (Q.localOverlay p s epsilon extra).vertexSet)).Nonempty → Graph.edgeArc segmentDrawing R ⊆ Graph.edgeArc P.src.drawing e

Away from overlay vertices, an inner-overlay edge meeting an old open nonboundary edge is one of that edge's subdivision pieces.

Containment in the source domain

theorem Schoenflies.SourceNonboundarySegmentCover.localGridPoint_mem_closedSquare {p : Plane} {s : ℝ} {k i j : ℕ} (hs : 0 < s) (hk : 1 ≤ k) (hi : i ≤ k) (hj : j ≤ k) : gridPt (localGridX p s k) (localGridY p s k) i j ∈ p.closedSquare s

Every grid point with indices in range lies in the local grid's closed square.

theorem Schoenflies.SourceNonboundarySegmentCover.cover_localGridEdges_subset_closedSquare {p : Plane} {s : ℝ} {k : ℕ} (hs : 0 < s) (hk : 1 ≤ k) : cover (localGridEdges p s k) ⊆ p.closedSquare s

The complete local grid carrier lies in its closed square window.

theorem Schoenflies.SourceNonboundarySegmentCover.localOverlay_pointSet_subset {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} (Q : SourceNonboundarySegmentCover P) {p : Plane} {s epsilon : ℝ} (hs : 0 < s) (hwindow : p.closedSquare s ⊆ srcDom) (extra : List Plane) : (Q.localOverlay p s epsilon extra).pointSet segmentDrawing ⊆ srcDom

If the closed local window lies in the source domain, then so does the complete finite inner overlay of the old nonboundary source skeleton with that grid.

theorem Schoenflies.SourceNonboundarySegmentCover.localOverlay_edge_dichotomy {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} (Q : SourceNonboundarySegmentCover P) {p : Plane} {s epsilon : ℝ} (hs : 0 < s) (hwindow : p.closedSquare s ⊆ srcDom \ srcOuter) (extra : List Plane) {R : Piece} : R ∈ (Q.localOverlay p s epsilon extra).edgeSet → IsPolygonal (Graph.edgeArc segmentDrawing R) ∧ Graph.edgeArc segmentDrawing R \ (Q.localOverlay p s epsilon extra).vertexSet ⊆ srcDom \ srcOuter

Every edge of the finite inner overlay is polygonal and its nonvertex points lie in the open source domain. For an old nonouter edge, weak admissibility puts its open 1-cell in the interior; if the old arc touches the wild boundary, the touching point is an old core vertex and hence an overlay vertex. Grid-sourced edges lie in the chosen interior window.

theorem Schoenflies.SourceNonboundarySegmentCover.sourceCore_inter_outer_vertices {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {x : Plane} (hxCore : x ∈ P.sourceNonboundaryGraph.pointSet P.src.drawing) (hxOuter : x ∈ srcOuter) : x ∈ P.sourceNonboundaryGraph.vertexSet ∧ x ∈ (Graph.map P.src.pos P.str.outerGraph).vertexSet

The compact nonboundary source carrier meets the wild outer curve only at vertices common to the nonboundary and outer source graphs.

Relabelling and adjoining the wild outer graph

structure Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} (Q : SourceNonboundarySegmentCover P) (p : Plane) (s epsilon : ℝ) (extra : List Plane) : Type u_1

Fresh abstract edge names for the finite straight-line inner overlay.

• name : Piece → γ

  Fresh cell names for the local-grid overlay.

• name_inj : Set.InjOn self.name (Q.localOverlay p s epsilon extra).edgeSet
• name_fresh (R : Piece) : R ∈ (Q.localOverlay p s epsilon extra).edgeSet → self.name R ∉ P.str.cells

theorem Schoenflies.SourceNonboundarySegmentCover.exists_localOverlayRelabeling {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} (Q : SourceNonboundarySegmentCover P) [Infinite γ] (p : Plane) (s epsilon : ℝ) (extra : List Plane) : Nonempty (Q.LocalOverlayRelabeling p s epsilon extra)

An infinite cell-name type supplies a relabelling of the inner overlay disjoint from every name already used by the current generated structure.

@[reducible, inline]

abbrev Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.outerGraph {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (_w : Q.LocalOverlayRelabeling p s epsilon extra) : Graph Plane γ

The old outer graph realized on the wild source curve.

Equations

• _w.outerGraph = Graph.map P.src.pos P.str.outerGraph

@[reducible, inline]

noncomputable abbrev Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.innerGraph {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) : Graph Plane γ

The finite inner overlay after allocation of fresh abstract edge names.

Equations

• w.innerGraph = (Q.localOverlay p s epsilon extra).relabelEdges w.name ⋯

noncomputable def Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.graph {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) : Graph Plane γ

The mixed source extension graph.

Equations

• w.graph = w.outerGraph.union w.innerGraph

noncomputable def Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.drawing {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) : γ → ℝ → Plane

The mixed drawing uses the original parametrizations on the wild outer edges and straight segments on every freshly named inner edge.

Equations

• w.drawing e = if e ∈ P.str.outerGraph.edgeSet then P.src.drawing e else (Q.localOverlay p s epsilon extra).relabelDrawing w.name Schoenflies.segmentDrawing e

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.compatible {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) : w.outerGraph.Compatible w.innerGraph

The two edge families are disjoint and therefore compatible.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.drawing_of_outer {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) {e : γ} (he : e ∈ P.str.outerGraph.edgeSet) : w.drawing e = P.src.drawing e

On an old outer edge the mixed drawing is the old source drawing.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.drawing_of_inner {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) {e : γ} (he : e ∈ w.innerGraph.edgeSet) : w.drawing e = (Q.localOverlay p s epsilon extra).relabelDrawing w.name segmentDrawing e

On an inner edge the mixed drawing is the relabelled straight-line drawing.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.outer_isDrawing {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) : w.outerGraph.IsDrawing w.drawing

The mixed drawing restricts to a plane drawing on the old wild outer graph.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.inner_isDrawing {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) (hs : 0 < s) : w.innerGraph.IsDrawing w.drawing

The mixed drawing restricts to a plane drawing on the straight-line inner overlay.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.outer_pointSet {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) : w.outerGraph.pointSet w.drawing = srcOuter

The old outer part of the mixed graph occupies exactly the wild source curve.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.inner_pointSet {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) : w.innerGraph.pointSet w.drawing = (Q.localOverlay p s epsilon extra).pointSet segmentDrawing

The inner part occupies exactly the finite straight-line local overlay.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.graph_isDrawing {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) (hs : 0 < s) (hwindow : p.closedSquare s ⊆ srcDom \ srcOuter) : w.graph.IsDrawing w.drawing

The mixed outer/inner source graph is a plane drawing whenever the local window lies in the open source domain.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.graph_finite {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) : w.graph.Finite

The mixed source graph is finite.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.graph_pointSet {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) : w.graph.pointSet w.drawing = srcOuter ∪ (P.sourceNonboundaryGraph.pointSet P.src.drawing ∪ cover (localGridEdges p s (localGridCount s epsilon)))

The mixed source graph occupies the wild outer curve, the old compact nonboundary carrier, and the complete local grid.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.sourceSkeleton_subset_graph {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) : P.src.skeletonSet ⊆ w.graph.pointSet w.drawing

The complete old source skeleton is retained by the mixed graph.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.sourceVertices_subset_graph {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) (hs : 0 < s) : P.src.graph.vertexSet ⊆ w.graph.vertexSet

Every old source vertex is explicitly retained as a mixed-graph vertex.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.graph_pointSet_subset {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) (hs : 0 < s) (hwindow : p.closedSquare s ⊆ srcDom \ srcOuter) : w.graph.pointSet w.drawing ⊆ srcDom

The mixed source graph stays in the closed source domain.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.graph_edge_dichotomy {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) (hs : 0 < s) (hwindow : p.closedSquare s ⊆ srcDom \ srcOuter) {e : γ} : e ∈ w.graph.edgeSet → Graph.edgeArc w.drawing e ⊆ srcOuter ∨ IsPolygonal (Graph.edgeArc w.drawing e) ∧ Graph.edgeArc w.drawing e \ w.graph.vertexSet ⊆ srcDom \ srcOuter

Every mixed edge is either an old outer edge on the wild curve or a polygonal inner edge whose nonvertex points lie in the open source domain.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.graph_edge_subset {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) (hs : 0 < s) (hwindow : p.closedSquare s ⊆ srcDom \ srcOuter) {e : γ} : e ∈ P.str.skel.edgeSet → ∀ {f : γ}, f ∈ w.graph.edgeSet → (Graph.edgeArc w.drawing f ∩ (P.src.cell e \ w.graph.vertexSet)).Nonempty → Graph.edgeArc w.drawing f ⊆ Graph.edgeArc P.src.drawing e

An edge of the mixed graph meeting an old open source edge away from mixed vertices is one of that edge's subdivision pieces.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.source_isPlaneSubdivisionExtension {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) (hs : 0 < s) (hwindow : p.closedSquare s ⊆ srcDom \ srcOuter) : IsPlaneSubdivisionExtension P.src.graph P.src.drawing w.graph w.drawing

The mixed graph contains a plane subdivision of the complete old source drawing.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.sourceTrace_isTwoConnected {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) (hs : 0 < s) (hwindow : p.closedSquare s ⊆ srcDom \ srcOuter) : (w.graph.traceGraph w.drawing P.src.skeletonSet).IsTwoConnected

The trace of the old source skeleton in the mixed graph remains 2-connected.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.localGridVertices_subset_graph {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) (hs : 0 < s) : (localGrid p s (localGridCount s epsilon)).vertexSet ⊆ w.graph.vertexSet

Every raw local-grid vertex is retained in the mixed graph.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.localGrid_subset_graph {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) : (localGrid p s (localGridCount s epsilon)).pointSet segmentDrawing ⊆ w.graph.pointSet w.drawing

The entire raw local-grid carrier is retained in the mixed graph.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.graph_grid_edge_subset {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) (hs : 0 < s) (hwindow : p.closedSquare s ⊆ srcDom \ srcOuter) {A : Piece} : A ∈ (localGrid p s (localGridCount s epsilon)).edgeSet → ∀ {f : γ}, f ∈ w.graph.edgeSet → (Graph.edgeArc w.drawing f ∩ (Graph.edgeArc segmentDrawing A \ w.graph.vertexSet)).Nonempty → Graph.edgeArc w.drawing f ⊆ Graph.edgeArc segmentDrawing A

An edge of the mixed graph meeting a raw local-grid edge away from mixed vertices is a subdivision piece of that grid edge. An old outer edge cannot meet the grid at all because the grid window is strictly inside the source domain.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.localGrid_isPlaneSubdivisionExtension {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) (hs : 0 < s) (hwindow : p.closedSquare s ⊆ srcDom \ srcOuter) : IsPlaneSubdivisionExtension (localGrid p s (localGridCount s epsilon)) segmentDrawing w.graph w.drawing

The mixed graph also contains a plane subdivision of the raw local grid.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.localGridTrace_isTwoConnected {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) (hs : 0 < s) (hwindow : p.closedSquare s ⊆ srcDom \ srcOuter) : (w.graph.traceGraph w.drawing ((localGrid p s (localGridCount s epsilon)).pointSet segmentDrawing)).IsTwoConnected

The local-grid trace inside the mixed graph remains 2-connected.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.graph_isTwoConnected_of_two_common {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) (hs : 0 < s) (hwindow : p.closedSquare s ⊆ srcDom \ srcOuter) {a b : Plane} (hab : a ≠ b) (haV : a ∈ w.graph.vertexSet) (hbV : b ∈ w.graph.vertexSet) (haSource : a ∈ P.src.skeletonSet) (hbSource : b ∈ P.src.skeletonSet) (haGrid : a ∈ (localGrid p s (localGridCount s epsilon)).pointSet segmentDrawing) (hbGrid : b ∈ (localGrid p s (localGridCount s epsilon)).pointSet segmentDrawing) : w.graph.IsTwoConnected

Two distinct mixed vertices lying on both the old source skeleton and the local grid make the whole mixed graph 2-connected. The two plane-subdivision traces are 2-connected and together contain every mixed vertex.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.graph_isConnected_diff_of_source_connected {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) (hs : 0 < s) (hwindow : p.closedSquare s ⊆ srcDom \ srcOuter) (hsource : IsConnected (P.src.skeletonSet \ srcOuter)) (hmeet : (P.src.skeletonSet \ srcOuter ∩ (localGrid p s (localGridCount s epsilon)).pointSet segmentDrawing).Nonempty) : IsConnected (w.graph.pointSet w.drawing \ srcOuter)

If the old open source skeleton is connected and meets the local grid, then the mixed carrier remains connected after the wild outer curve is removed.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.isSourceExtension {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) (hs : 0 < s) (hwindow : p.closedSquare s ⊆ srcDom \ srcOuter) (htwo : w.graph.IsTwoConnected) (hconnected : IsConnected (w.graph.pointSet w.drawing \ srcOuter)) : IsSourceExtension P.src srcOuter srcDom w.graph w.drawing

The mixed graph is a complete source extension once its two global attachment properties are supplied. All finiteness, drawing, subdivision, containment, and edge-geometry fields are automatic from the exact source cover and the interior-window hypothesis.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.isSourceExtension_of_two_common {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) (hs : 0 < s) (hwindow : p.closedSquare s ⊆ srcDom \ srcOuter) {a b : Plane} (hab : a ≠ b) (haV : a ∈ w.graph.vertexSet) (hbV : b ∈ w.graph.vertexSet) (haSource : a ∈ P.src.skeletonSet) (hbSource : b ∈ P.src.skeletonSet) (haGrid : a ∈ (localGrid p s (localGridCount s epsilon)).pointSet segmentDrawing) (hbGrid : b ∈ (localGrid p s (localGridCount s epsilon)).pointSet segmentDrawing) (hconnected : IsConnected (w.graph.pointSet w.drawing \ srcOuter)) : IsSourceExtension P.src srcOuter srcDom w.graph w.drawing

With two common source/grid vertices, only connectedness off the wild outer curve remains to obtain the complete source extension.

theorem Schoenflies.SourceNonboundarySegmentCover.LocalOverlayRelabeling.isSourceExtension_of_source_connected_two_common {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {Q : SourceNonboundarySegmentCover P} {p : Plane} {s epsilon : ℝ} {extra : List Plane} (w : Q.LocalOverlayRelabeling p s epsilon extra) (hs : 0 < s) (hwindow : p.closedSquare s ⊆ srcDom \ srcOuter) (hsource : IsConnected P.src.nonboundary) {a b : Plane} (hab : a ≠ b) (haV : a ∈ w.graph.vertexSet) (hbV : b ∈ w.graph.vertexSet) (haSource : a ∈ P.src.skeletonSet) (hbSource : b ∈ P.src.skeletonSet) (haGrid : a ∈ (localGrid p s (localGridCount s epsilon)).pointSet segmentDrawing) (hbGrid : b ∈ (localGrid p s (localGridCount s epsilon)).pointSet segmentDrawing) : IsSourceExtension P.src srcOuter srcDom w.graph w.drawing

At an admissible stage, two distinct common source/grid vertices give the complete source extension. One common point joins the two connected carriers off the boundary; both common vertices make their 2-connected subdivision traces glue.