Polygonal joining ears for boundary-touching source crosscuts #
When both ends of the auxiliary face crosscut lie on the wild outer curve, deleting that curve
separates the crosscut/grid carrier from the old nonboundary source carrier. The last step of
prop:local-grid-attachment joins those two carriers by a simple polygonal arc in the open
source domain.
This module begins with the finite inner construction: re-overlay the already-subdivided source
core, crosscut, and grid together with the joining segments, retaining every old inner vertex.
OverlayExtension then supplies the plane-subdivision certificate automatically.
theorem
Schoenflies.Graph.IsDrawing.common_vertices_of_disjoint_subgraphs
{β : Type u_2}
{G A B : Graph Plane β}
{drawing : β → ℝ → Plane}
(h : G.IsDrawing drawing)
(hA : A ≤ G)
(hB : B ≤ G)
(hdisj : Disjoint A.edgeSet B.edgeSet)
{x : Plane}
(hxA : x ∈ A.pointSet drawing)
(hxB : x ∈ B.pointSet drawing)
:
Two edge-disjoint subgraphs of one plane drawing can meet only at vertices common to both. This is the converse interface used when an already-plane union is re-subdivided on one side.
noncomputable def
Schoenflies.SourceNonboundarySegmentCover.joinedCrosscutOverlay
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
(Q : SourceNonboundarySegmentCover P)
(J : Piece)
(p : Plane)
(s epsilon : ℝ)
(extra : List Plane)
(joins : List Piece)
:
Re-overlay the complete auxiliary-crosscut inner graph together with a list of polygonal joining segments.
Equations
- Q.joinedCrosscutOverlay J p s epsilon extra joins = Schoenflies.extendOverlay (Q.crosscutPieces J p s epsilon) (extra ++ P.sourceNonboundaryGraph.vertexFinset.toList) joins
Instances For
instance
Schoenflies.SourceNonboundarySegmentCover.joinedCrosscutOverlay_finite
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
(Q : SourceNonboundarySegmentCover P)
(J : Piece)
(p : Plane)
(s epsilon : ℝ)
(extra : List Plane)
(joins : List Piece)
:
(Q.joinedCrosscutOverlay J p s epsilon extra joins).Finite
theorem
Schoenflies.SourceNonboundarySegmentCover.joinedCrosscutOverlay_pointSet
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
(Q : SourceNonboundarySegmentCover P)
(J : Piece)
(p : Plane)
(s epsilon : ℝ)
(extra : List Plane)
(joins : List Piece)
:
(Q.joinedCrosscutOverlay J p s epsilon extra joins).pointSet segmentDrawing = (Q.crosscutOverlay J p s epsilon extra).pointSet segmentDrawing ∪ cover joins
The joined inner overlay occupies exactly the old core/crosscut/grid carrier together with the polygonal joining carrier.
theorem
Schoenflies.SourceNonboundarySegmentCover.joinedCrosscutOverlay_isDrawing
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
(hs : 0 < s)
(hJ : J.Nondeg)
{joins : List Piece}
(hjoins : ∀ R ∈ joins, R.Nondeg)
:
(Q.joinedCrosscutOverlay J p s epsilon extra joins).IsDrawing segmentDrawing
The joined inner overlay is a finite straight-line plane graph.
theorem
Schoenflies.SourceNonboundarySegmentCover.crosscutOverlayVertices_subset_joinedCrosscutOverlay
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
(hs : 0 < s)
(hJ : J.Nondeg)
{joins : List Piece}
(hjoins : ∀ R ∈ joins, R.Nondeg)
:
(Q.crosscutOverlay J p s epsilon extra).vertexSet ⊆ (Q.joinedCrosscutOverlay J p s epsilon extra joins).vertexSet
Every vertex of the core/crosscut/grid overlay survives the joining re-overlay.
theorem
Schoenflies.SourceNonboundarySegmentCover.crosscutOverlay_isPlaneSubdivisionExtension_joined
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
(hs : 0 < s)
(hJ : J.Nondeg)
{joins : List Piece}
(hjoins : ∀ R ∈ joins, R.Nondeg)
:
IsPlaneSubdivisionExtension (Q.crosscutOverlay J p s epsilon extra) segmentDrawing
(Q.joinedCrosscutOverlay J p s epsilon extra joins) segmentDrawing
The joined inner overlay is a plane subdivision extension of the complete old inner crosscut overlay.
theorem
Schoenflies.SourceNonboundarySegmentCover.joinedCrosscutOverlay_old_edge_subset
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
(hs : 0 < s)
(hJ : J.Nondeg)
{joins : List Piece}
(hjoins : ∀ R ∈ joins, R.Nondeg)
{A : Piece}
:
A ∈ (Q.crosscutOverlay J p s epsilon extra).edgeSet →
∀ {R : Piece},
R ∈ (Q.joinedCrosscutOverlay J p s epsilon extra joins).edgeSet →
(Graph.edgeArc segmentDrawing R ∩ (Graph.edgeArc segmentDrawing A \ (Q.joinedCrosscutOverlay J p s epsilon extra joins).vertexSet)).Nonempty →
Graph.edgeArc segmentDrawing R ⊆ Graph.edgeArc segmentDrawing A
Every old inner edge is absorbed by its subdivision in the joined overlay.
theorem
Schoenflies.SourceNonboundarySegmentCover.joinedCrosscutOverlay_join_subset
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
(hs : 0 < s)
(hJ : J.Nondeg)
{joins : List Piece}
(hjoins : ∀ R ∈ joins, R.Nondeg)
{R : Piece}
:
R ∈ (Q.joinedCrosscutOverlay J p s epsilon extra joins).edgeSet →
(Graph.edgeArc segmentDrawing R ∩ (cover joins \ (Q.joinedCrosscutOverlay J p s epsilon extra joins).vertexSet)).Nonempty →
Graph.edgeArc segmentDrawing R ⊆ cover joins
A joined-overlay edge meeting the joining carrier away from overlay vertices is absorbed by that carrier.
theorem
Schoenflies.SourceNonboundarySegmentCover.joinEnds_subset_joinedCrosscutOverlay
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
(hs : 0 < s)
(hJ : J.Nondeg)
{joins : List Piece}
(hjoins : ∀ R ∈ joins, R.Nondeg)
:
endSet joins ⊆ (Q.joinedCrosscutOverlay J p s epsilon extra joins).vertexSet
Every endpoint of a joining segment is a vertex of the joined inner overlay.
Fresh relabelling and the wild outer graph #
structure
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
(joins : List Piece)
:
Type u_1
Fresh abstract edge names for the joined inner overlay.
- name : Piece → γ
Fresh names for the overlay after adding the joining segments.
- name_inj : Set.InjOn self.name (Q.joinedCrosscutOverlay J p s epsilon extra joins).edgeSet
Instances For
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.exists_joinedRelabeling
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
[Infinite γ]
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
(joins : List Piece)
:
Nonempty (JoinedCrosscutOverlayRelabeling w joins)
An infinite cell-name type supplies fresh names for the joined overlay.
@[reducible, inline]
abbrev
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.outerGraph
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(_u : JoinedCrosscutOverlayRelabeling w joins)
:
The unchanged mapped wild outer graph.
Equations
- _u.outerGraph = Graph.map P.src.pos P.str.outerGraph
Instances For
@[reducible, inline]
noncomputable abbrev
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.innerGraph
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
:
The freshly relabelled joined inner overlay.
Equations
- u.innerGraph = (Q.joinedCrosscutOverlay J p s epsilon extra joins).relabelEdges u.name ⋯
Instances For
noncomputable def
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.graph
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
:
The mixed graph after adjoining the polygonal join.
Equations
- u.graph = u.outerGraph.union u.innerGraph
Instances For
noncomputable def
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.drawing
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
:
The joined drawing keeps the wild outer parametrizations and draws every inner edge as a straight segment.
Equations
- u.drawing e = if e ∈ P.str.outerGraph.edgeSet then P.src.drawing e else (Q.joinedCrosscutOverlay J p s epsilon extra joins).relabelDrawing u.name Schoenflies.segmentDrawing e
Instances For
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.compatible
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
:
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.disjoint_edgeSet
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
:
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.drawing_of_outer
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
{e : γ}
(he : e ∈ P.str.outerGraph.edgeSet)
:
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.drawing_of_inner
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
{e : γ}
(he : e ∈ u.innerGraph.edgeSet)
:
u.drawing e = (Q.joinedCrosscutOverlay J p s epsilon extra joins).relabelDrawing u.name segmentDrawing e
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.outer_isDrawing
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
:
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.inner_isDrawing
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
(hs : 0 < s)
(hJ : J.Nondeg)
(hjoins : ∀ R ∈ joins, R.Nondeg)
:
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.outer_pointSet
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
:
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.inner_pointSet
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
:
u.innerGraph.pointSet u.drawing = (Q.joinedCrosscutOverlay J p s epsilon extra joins).pointSet segmentDrawing
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.graph_isDrawing
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
(hjoins : ∀ R ∈ joins, R.Nondeg)
(hjoinsOpen : cover joins ⊆ srcDom \ srcOuter)
:
The joined inner overlay remains plane when every joining segment lies in the open source domain.
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.graph_finite
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
:
The joined mixed graph is finite.
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.graph_pointSet
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
:
Exact carrier of the joined mixed graph.
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.oldVertices_subset_graph
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
(hs : 0 < s)
(hJ : J.Nondeg)
(hjoins : ∀ R ∈ joins, R.Nondeg)
:
Every vertex of the old mixed crosscut graph survives the joining re-overlay.
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.old_edge_subset
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
(hjoins : ∀ R ∈ joins, R.Nondeg)
(hjoinsOpen : cover joins ⊆ srcDom \ srcOuter)
{e : γ}
:
e ∈ w.graph.edgeSet →
∀ {f : γ},
f ∈ u.graph.edgeSet →
(Graph.edgeArc u.drawing f ∩ (Graph.edgeArc w.drawing e \ u.graph.vertexSet)).Nonempty →
Graph.edgeArc u.drawing f ⊆ Graph.edgeArc w.drawing e
A new mixed edge meeting an old mixed edge away from new vertices is one of that old edge's subdivision pieces.
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.oldGraph_isPlaneSubdivisionExtension
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
(hjoins : ∀ R ∈ joins, R.Nondeg)
(hjoinsOpen : cover joins ⊆ srcDom \ srcOuter)
:
The joined mixed graph is a plane subdivision extension of the complete old mixed graph.
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.oldTrace_isTwoConnected
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
(hjoins : ∀ R ∈ joins, R.Nondeg)
(hjoinsOpen : cover joins ⊆ srcDom \ srcOuter)
(htwo : w.graph.IsTwoConnected)
:
(u.graph.traceGraph u.drawing (w.graph.pointSet w.drawing)).IsTwoConnected
The exact trace of the old mixed carrier remains 2-connected in the joined graph.
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.joinEnds_subset_graph
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
(hs : 0 < s)
(hJ : J.Nondeg)
(hjoins : ∀ R ∈ joins, R.Nondeg)
:
Every endpoint of a joining segment is a vertex of the joined mixed graph.
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.joins_subset_graph
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
:
The complete polygonal joining carrier lies in the joined mixed graph.
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.graph_join_subset
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
(hs : 0 < s)
(hJ : J.Nondeg)
(hjoins : ∀ R ∈ joins, R.Nondeg)
(hjoinsOpen : cover joins ⊆ srcDom \ srcOuter)
{f : γ}
:
A joined mixed edge meeting the polygonal joining carrier away from mixed vertices is absorbed by that carrier.
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.joinTrace_pointSet
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
(hjoins : ∀ R ∈ joins, R.Nondeg)
(hjoinsOpen : cover joins ⊆ srcDom \ srcOuter)
:
The trace supported on the polygonal joining carrier occupies that carrier exactly.
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.exists_join_trace
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
(hjoins : ∀ R ∈ joins, R.Nondeg)
(hjoinsOpen : cover joins ⊆ srcDom \ srcOuter)
{x y : Plane}
(hxy : x ≠ y)
(hxEnd : x ∈ endSet joins)
(hyEnd : y ∈ endSet joins)
(hArc : IsArcBetween (cover joins) x y)
:
An arc presented by the joining pieces is the exact carrier of a path in the joined mixed graph.
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.graph_isTwoConnected_of_join
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
(hjoins : ∀ R ∈ joins, R.Nondeg)
(hjoinsOpen : cover joins ⊆ srcDom \ srcOuter)
(hOldTwo : w.graph.IsTwoConnected)
{x y : Plane}
(hxy : x ≠ y)
(hxEnd : x ∈ endSet joins)
(hyEnd : y ∈ endSet joins)
(hxOld : x ∈ w.graph.pointSet w.drawing)
(hyOld : y ∈ w.graph.pointSet w.drawing)
(hArc : IsArcBetween (cover joins) x y)
:
Attaching a polygonal joining arc between two old-carrier points makes the entire joined mixed graph 2-connected.
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.source_isPlaneSubdivisionExtension
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
(hjoins : ∀ R ∈ joins, R.Nondeg)
(hjoinsOpen : cover joins ⊆ srcDom \ srcOuter)
:
The joined graph remains a plane subdivision extension of the complete old source drawing.
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.graph_pointSet_subset
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
(hs : 0 < s)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
(hjoinsOpen : cover joins ⊆ srcDom \ srcOuter)
:
The joined graph stays in the closed source domain.
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.joinedInner_edge_source
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{R : Piece}
(hR : R ∈ (Q.joinedCrosscutOverlay J p s epsilon extra joins).edgeSet)
:
Every joined inner edge is cut either from an old core/crosscut/grid edge or from one of the polygonal joining segments.
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.graph_edge_dichotomy
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
(hjoins : ∀ R ∈ joins, R.Nondeg)
(hjoinsOpen : cover joins ⊆ srcDom \ srcOuter)
{e : γ}
:
e ∈ u.graph.edgeSet →
Graph.edgeArc u.drawing e ⊆ srcOuter ∨ IsPolygonal (Graph.edgeArc u.drawing e) ∧ Graph.edgeArc u.drawing e \ u.graph.vertexSet ⊆ srcDom \ srcOuter
Every joined mixed edge either lies on the wild outer curve or is polygonal with all nonvertex points in the open source domain.
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.graph_edge_subset
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
(hjoins : ∀ R ∈ joins, R.Nondeg)
(hjoinsOpen : cover joins ⊆ srcDom \ srcOuter)
{e : γ}
:
A joined edge meeting an old source cell away from joined vertices is absorbed by that old source edge.
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.graph_isConnected_diff_of_join
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
(hs : 0 < s)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
(hsource : IsConnected (P.src.skeletonSet \ srcOuter))
(hjoinsOpen : cover joins ⊆ srcDom \ srcOuter)
{A : Piece}
(hA : A ∈ (localGrid p s (localGridCount s epsilon)).edgeSet)
(hAJ : A.seg ⊆ J.seg)
{x y : Plane}
(hxJ : x ∈ J.interior)
(hySource : y ∈ P.src.skeletonSet \ srcOuter)
(hArc : IsArcBetween (cover joins) x y)
:
IsConnected (u.graph.pointSet u.drawing \ srcOuter)
A join running from the open crosscut to the old nonboundary source carrier makes the joined carrier connected after deletion of the wild outer curve.
theorem
Schoenflies.SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling.isSourceExtension
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{Q : SourceNonboundarySegmentCover P}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
{joins : List Piece}
{w : Q.CrosscutOverlayRelabeling J p s epsilon extra}
(u : JoinedCrosscutOverlayRelabeling w joins)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
(hjoins : ∀ R ∈ joins, R.Nondeg)
(hjoinsOpen : cover joins ⊆ srcDom \ srcOuter)
(hOldTwo : w.graph.IsTwoConnected)
{x y : Plane}
(hxy : x ≠ y)
(hxEnd : x ∈ endSet joins)
(hyEnd : y ∈ endSet joins)
(hxOld : x ∈ w.graph.pointSet w.drawing)
(hyOld : y ∈ w.graph.pointSet w.drawing)
(hArc : IsArcBetween (cover joins) x y)
(hconnected : IsConnected (u.graph.pointSet u.drawing \ srcOuter))
:
IsSourceExtension P.src srcOuter srcDom u.graph u.drawing
The joined construction is a complete source extension.
structure
Schoenflies.JoinedLocalGridSourceExtensionData
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{F : γ}
{A : Piece}
(r : RefinedSourceFaceCrosscutData P F A)
(p : Plane)
(s epsilon : ℝ)
:
Type u_1
The complete output of the boundary-crosscut joining construction.
- oldOverlay : RefinedCrosscutOverlayData r p s epsilon
Crosscut overlay before joining its components.
Polygonal segments joining the nonboundary components.
- joinedRelabeling : SourceNonboundarySegmentCover.JoinedCrosscutOverlayRelabeling self.oldOverlay.relabeling self.joins
Cell names for the overlay including the joining segments.
- isSourceExtension : IsSourceExtension r.subdivision.pair.src srcOuter srcDom self.joinedRelabeling.graph self.joinedRelabeling.drawing
- localGrid_subset : (localGrid p s (localGridCount s epsilon)).pointSet segmentDrawing ⊆ self.joinedRelabeling.graph.pointSet self.joinedRelabeling.drawing
Instances For
theorem
Schoenflies.RefinedCrosscutOverlayData.exists_joinedLocalGridSourceExtensionData
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
[Infinite γ]
{F : γ}
{A : Piece}
{p : Plane}
{s epsilon : ℝ}
{r : RefinedSourceFaceCrosscutData P F A}
(o : RefinedCrosscutOverlayData r p s epsilon)
(hs : 0 < s)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
(hopen : IsOpen (srcDom \ srcOuter))
(hconn : IsPreconnected (srcDom \ srcOuter))
(hsource : IsConnected r.subdivision.pair.src.nonboundary)
(hA : A ∈ (localGrid p s (localGridCount s epsilon)).edgeSet)
:
Nonempty (JoinedLocalGridSourceExtensionData r p s epsilon)
Construct the manuscript's final polygonal component-joining ear. A midpoint of the open crosscut and a point of the connected old nonboundary carrier lie in the same open connected source domain, so polygonal connectedness supplies a simple joining arc. Re-overlaying its segments and attaching its exact trace gives a complete local-grid source extension even when both crosscut endpoints lie on the wild outer curve.
theorem
Schoenflies.GeneratedPair.exists_joinedLocalGridSourceExtensionData
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
[Infinite γ]
{F : γ}
{A : Piece}
{p : Plane}
{s epsilon : ℝ}
(hF : F ∈ P.str.faces)
(hFbdd : Bornology.IsBounded (P.src.cell F))
{a b y : Plane}
(hab : a ≠ b)
(hAline : A.interior ⊆ a.line b ∩ P.src.cell F)
(hy : y ∈ A.interior)
(hs : 0 < s)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
(hopen : IsOpen (srcDom \ srcOuter))
(hconn : IsPreconnected (srcDom \ srcOuter))
(hsource : IsConnected P.src.nonboundary)
(hA : A ∈ (localGrid p s (localGridCount s epsilon)).edgeSet)
:
Nonempty ((r : RefinedSourceFaceCrosscutData P F A) × JoinedLocalGridSourceExtensionData r p s epsilon)
Complete the boundary-touching local-grid attachment starting only from a bounded source face and a grid edge whose relative interior lies on a line through that face. The preliminary matched subdivision preserves the old source carrier, so connectedness of the original nonboundary source graph is exactly the connectedness needed by the polygonal joining step.
theorem
Schoenflies.GeneratedPair.exists_joinedLocalGridSourceExtensionData_inside
{γ : Type u_1}
{S₀ : CellStructure γ}
{tgtOuter tgtDom : Set Plane}
[Infinite γ]
{C : Set Plane}
{P : GeneratedPair S₀ C (C ∪ inside C) tgtOuter tgtDom}
{F : γ}
{A : Piece}
{p : Plane}
{s epsilon : ℝ}
(hC : IsSeparating C)
(hF : F ∈ P.str.faces)
(hFbdd : Bornology.IsBounded (P.src.cell F))
{a b y : Plane}
(hab : a ≠ b)
(hAline : A.interior ⊆ a.line b ∩ P.src.cell F)
(hy : y ∈ A.interior)
(hs : 0 < s)
(hwindow : p.closedSquare s ⊆ (C ∪ inside C) \ C)
(hsource : IsConnected P.src.nonboundary)
(hA : A ∈ (localGrid p s (localGridCount s epsilon)).edgeSet)
:
Nonempty ((r : RefinedSourceFaceCrosscutData P F A) × JoinedLocalGridSourceExtensionData r p s epsilon)
In the actual Schönflies source domain, the hypotheses needed to draw the final joining arc are automatic consequences of Jordan separation: the closed domain minus its boundary is the connected open inside region.
theorem
Schoenflies.localGrid_horizontal_extremes_interior_disjoint
{p : Plane}
{s : ℝ}
{k : ℕ}
(hs : 0 < s)
(hk : 1 ≤ k)
:
Disjoint (gridHEdge (localGridX p s k) (localGridY p s k) 0 0).interior
(gridHEdge (localGridX p s k) (localGridY p s k) 0 k).interior
The relative interiors of a local grid's bottom and top leftmost edges are disjoint.
theorem
Schoenflies.GeneratedPair.exists_localGridEdge_interior_disjoint_of_common_subsingleton
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{p : Plane}
{s epsilon : ℝ}
(hs : 0 < s)
(hcommon : (P.src.skeletonSet ∩ (localGrid p s (localGridCount s epsilon)).pointSet segmentDrawing).Subsingleton)
:
∃ A ∈ (localGrid p s (localGridCount s epsilon)).edgeSet, Disjoint A.interior P.src.skeletonSet
If the complete source/grid intersection has at most one point, at least one of two opposite horizontal grid edges has relative interior disjoint from the source skeleton.
theorem
Schoenflies.GeneratedPair.exists_localGridSourceExtensionData_of_common_not_subsingleton
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
[Infinite γ]
{p : Plane}
{s epsilon : ℝ}
(hs : 0 < s)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
(hsource : IsConnected P.src.nonboundary)
(hcommon : ¬(P.src.skeletonSet ∩ (localGrid p s (localGridCount s epsilon)).pointSet segmentDrawing).Subsingleton)
:
Nonempty (LocalGridSourceExtensionData P p s epsilon)
In the two-common-point branch, retaining those points explicitly in the raw source/grid overlay gives the complete local-grid source extension directly.
theorem
Schoenflies.GeneratedPair.exists_joinedLocalGridSourceExtensionData_of_disjoint_edge
{γ : Type u_1}
{S₀ : CellStructure γ}
{tgtOuter tgtDom : Set Plane}
[Infinite γ]
{C : Set Plane}
{P : GeneratedPair S₀ C (C ∪ inside C) tgtOuter tgtDom}
{A : Piece}
{p : Plane}
{s epsilon : ℝ}
(hC : IsSeparating C)
(hs : 0 < s)
(hwindow : p.closedSquare s ⊆ (C ∪ inside C) \ C)
(hsource : IsConnected P.src.nonboundary)
(hA : A ∈ (localGrid p s (localGridCount s epsilon)).edgeSet)
(hdisj : Disjoint A.interior P.src.skeletonSet)
:
Nonempty ((F : γ) × (r : RefinedSourceFaceCrosscutData P F A) × JoinedLocalGridSourceExtensionData r p s epsilon)
A raw grid edge whose open segment misses the current source skeleton lies in one bounded source face. Thus it supplies all of the face-selection data required by the auxiliary crosscut and joining construction.
theorem
Schoenflies.GeneratedPair.exists_joinedLocalGridSourceExtensionData_of_common_subsingleton
{γ : Type u_1}
{S₀ : CellStructure γ}
{tgtOuter tgtDom : Set Plane}
[Infinite γ]
{C : Set Plane}
{P : GeneratedPair S₀ C (C ∪ inside C) tgtOuter tgtDom}
{p : Plane}
{s epsilon : ℝ}
(hC : IsSeparating C)
(hs : 0 < s)
(hwindow : p.closedSquare s ⊆ (C ∪ inside C) \ C)
(hsource : IsConnected P.src.nonboundary)
(hcommon : (P.src.skeletonSet ∩ (localGrid p s (localGridCount s epsilon)).pointSet segmentDrawing).Subsingleton)
:
Nonempty
((F : γ) × (A : Piece) × (r : RefinedSourceFaceCrosscutData P F A) × JoinedLocalGridSourceExtensionData r p s epsilon)
The at-most-one-common-point branch automatically supplies a skeleton-disjoint grid edge, so the completed face-crosscut and joining construction applies without further choices.
theorem
Schoenflies.GeneratedPair.exists_localGridSourceExtensionData_cases
{γ : Type u_1}
{S₀ : CellStructure γ}
{tgtOuter tgtDom : Set Plane}
[Infinite γ]
{C : Set Plane}
{P : GeneratedPair S₀ C (C ∪ inside C) tgtOuter tgtDom}
{p : Plane}
{s epsilon : ℝ}
(hC : IsSeparating C)
(hs : 0 < s)
(hwindow : p.closedSquare s ⊆ (C ∪ inside C) \ C)
(hsource : IsConnected P.src.nonboundary)
:
Nonempty (LocalGridSourceExtensionData P p s epsilon) ∨ Nonempty
((F : γ) ×
(A : Piece) × (r : RefinedSourceFaceCrosscutData P F A) × JoinedLocalGridSourceExtensionData r p s epsilon)
Exhaustive local-grid attachment. With two distinct source/grid intersection points the raw overlay extends the current pair directly. Otherwise a raw grid edge misses the skeleton in its relative interior, and a matched endpoint subdivision followed by the crosscut and polygonal joining ears produces the extension.
theorem
Schoenflies.GeneratedPair.SubdivideSetData.stageTransition
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{s : Set Plane}
(r : P.SubdivideSetData s)
:
StageTransition r.pair P r.parent
A matched finite source-skeleton subdivision is already a stage transition.
structure
Schoenflies.LocalGridForwardStageData
{γ : Type u_1}
{S₀ : CellStructure γ}
{tgtOuter tgtDom C : Set Plane}
(P : GeneratedPair S₀ C (C ∪ inside C) tgtOuter tgtDom)
(p : Plane)
(s epsilon : ℝ)
:
Type u_1
The uniform stage-level output of local-grid attachment, after running forward finite transfer. Both geometric branches now return one generated refinement of the original pair, with admissibility restored and the complete raw local grid in its source skeleton.
- pair : GeneratedPair S₀ C (C ∪ inside C) tgtOuter tgtDom
Generated matched pair after the local-grid transfer.
- parent : γ → γ
Parent cell of each cell in the refinement.
- transition : StageTransition self.pair P self.parent
- src_isAdmissible : self.pair.src.IsAdmissible C (C ∪ inside C)
- tgt_isAdmissible : self.pair.tgt.IsAdmissible tgtOuter tgtDom
- localGrid_subset : (localGrid p s (localGridCount s epsilon)).pointSet segmentDrawing ⊆ self.pair.src.skeletonSet
Instances For
theorem
Schoenflies.GeneratedPair.exists_localGridForwardStageData
{γ : Type u_1}
{S₀ : CellStructure γ}
{tgtOuter tgtDom : Set Plane}
[Infinite γ]
{C : Set Plane}
{P : GeneratedPair S₀ C (C ∪ inside C) tgtOuter tgtDom}
{p : Plane}
{s epsilon : ℝ}
(hC : IsSeparating C)
(hs : 0 < s)
(hwindow : p.closedSquare s ⊆ (C ∪ inside C) \ C)
(hsource : IsConnected P.src.nonboundary)
:
Nonempty (LocalGridForwardStageData P p s epsilon)
Local-grid forward successor. The source/grid intersection dichotomy, the auxiliary face crosscut, endpoint subdivisions, polygonal joining ear, and forward finite transfer are all internal.