Auxiliary-crosscut source overlays #
A local window can miss the current skeleton, so the raw source/grid overlay need not have the
two common vertices required for 2-connectivity. The degenerate cases of
prop:local-grid-attachment add one polygonal crosscut of the containing face. This module
builds the corresponding finite straight-line inner overlay while keeping the original wild
outer curve separate.
Blueprint #
Schoenflies.SourceNonboundarySegmentCover.crosscutOverlay— the old compact nonboundary carrier, one auxiliary crosscut, and the local grid in a single exact segment overlay.crosscutOverlay_pointSet— its exact carrier.crosscutOverlay_isDrawing,crosscutOverlay_pointSet_subset, andcrosscutOverlay_edge_dichotomy— the local plane and domain geometry needed by finite transfer.
theorem
Schoenflies.GeneratedPair.src_face_subset_interior
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{F : γ}
(hF : F ∈ P.str.faces)
:
Every source face of a generated pair lies in the prescribed open source domain.
structure
Schoenflies.SourceFaceCrosscutData
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
(P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom)
(F : γ)
(A : Piece)
:
The geometric output of cutting a bounded source face along the line carrying a selected grid edge. The closed crosscut swallows that edge; its open part lies in the face and both ends lie on the old source skeleton.
- crosscut : Piece
Closed segment spanning the selected source face.
Instances For
theorem
Schoenflies.SourceFaceCrosscutData.seg_subset_interior
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{F : γ}
{A : Piece}
(d : SourceFaceCrosscutData P F A)
(hfrontier : frontier (P.src.cell F) ⊆ srcDom \ srcOuter)
:
If the selected face has no wild-boundary points on its frontier, the entire closed crosscut lies in the open source domain.
theorem
Schoenflies.GeneratedPair.exists_sourceFaceCrosscutData
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{F : γ}
{A : Piece}
(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)
:
Nonempty (SourceFaceCrosscutData P F A)
A line through the relative interior of a selected grid edge in a bounded source face produces the exact auxiliary-crosscut data used by the mixed source overlay.
structure
Schoenflies.SourceCrosscutGeometry
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
(P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom)
(J : Piece)
:
The exact geometry needed to adjoin a straight crosscut to a source drawing. Its interior is disjoint from the wild boundary; an endpoint is allowed on that boundary precisely when it is already a source vertex (as happens after subdividing the endpoint into the old skeleton).
- seg_subset_domain : J.seg ⊆ srcDom
Instances For
theorem
Schoenflies.SourceCrosscutGeometry.of_seg_subset_interior
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{J : Piece}
(hJopen : J.seg ⊆ srcDom \ srcOuter)
:
A crosscut whose complete closed segment lies in the open domain automatically satisfies the boundary-endpoint condition.
theorem
Schoenflies.GeneratedPair.sourceVertex_mem_outerGraph
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{x : Plane}
(hxV : x ∈ P.src.graph.vertexSet)
(hxOuter : x ∈ srcOuter)
:
A source vertex lying on the realized outer set is already a vertex of the mapped outer graph.
structure
Schoenflies.RefinedSourceFaceCrosscutData
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
(P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom)
(F : γ)
(A : Piece)
:
Type u_1
A face crosscut together with the preliminary matched subdivision that makes both of its endpoints old source vertices. This is the representation needed when either endpoint lands in the interior of a wild outer edge.
- crosscutData : SourceFaceCrosscutData P F A
Crosscut geometry before refining its endpoints.
- subdivision : P.SubdivideSetData {self.crosscutData.crosscut.1, self.crosscutData.crosscut.2}
Matched subdivision making both crosscut endpoints vertices.
- geometry : SourceCrosscutGeometry self.subdivision.pair self.crosscutData.crosscut
Instances For
theorem
Schoenflies.SourceFaceCrosscutData.exists_refinement
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
[Infinite γ]
{F : γ}
{A : Piece}
(d : SourceFaceCrosscutData P F A)
:
Every source-face crosscut admits a matched preliminary subdivision at its two endpoints. The construction is harmless when an endpoint was already a vertex and essential when it lies inside a wild outer edge.
noncomputable def
Schoenflies.SourceNonboundarySegmentCover.crosscutPieces
{γ : 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 : ℝ)
:
The source pieces after adjoining one auxiliary crosscut and one local grid.
Equations
- Q.crosscutPieces J p s epsilon = Q.pieces ++ [J] ++ Schoenflies.localGridEdges p s (Schoenflies.localGridCount s epsilon)
Instances For
noncomputable def
Schoenflies.SourceNonboundarySegmentCover.crosscutOverlay
{γ : 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)
:
The finite straight-line overlay of the old compact source core, an auxiliary crosscut, and the local grid. Old nonboundary vertices and prescribed points are retained.
Equations
- Q.crosscutOverlay J p s epsilon extra = Schoenflies.attachGraph (Q.crosscutPieces J p s epsilon) (extra ++ P.sourceNonboundaryGraph.vertexFinset.toList)
Instances For
instance
Schoenflies.SourceNonboundarySegmentCover.crosscutOverlay_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)
:
(Q.crosscutOverlay J p s epsilon extra).Finite
theorem
Schoenflies.SourceNonboundarySegmentCover.crosscutPieces_nondeg
{γ : 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 : ℝ}
(hs : 0 < s)
(hJ : J.Nondeg)
(R : Piece)
:
R ∈ Q.crosscutPieces J p s epsilon → R.Nondeg
Every source piece in the crosscut overlay is nondegenerate.
theorem
Schoenflies.SourceNonboundarySegmentCover.crosscutOverlay_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 : ℝ}
(hs : 0 < s)
(hJ : J.Nondeg)
(extra : List Plane)
:
(Q.crosscutOverlay J p s epsilon extra).IsDrawing segmentDrawing
The auxiliary-crosscut overlay is a finite straight-line plane graph.
theorem
Schoenflies.SourceNonboundarySegmentCover.crosscutOverlay_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)
:
(Q.crosscutOverlay J p s epsilon extra).pointSet segmentDrawing = P.sourceNonboundaryGraph.pointSet P.src.drawing ∪ J.seg ∪ cover (localGridEdges p s (localGridCount s epsilon))
The crosscut overlay occupies exactly the old compact source carrier, the auxiliary segment, and the local grid.
theorem
Schoenflies.SourceNonboundarySegmentCover.sourceCore_subset_crosscutOverlay
{γ : 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)
:
P.sourceNonboundaryGraph.pointSet P.src.drawing ⊆ (Q.crosscutOverlay J p s epsilon extra).pointSet segmentDrawing
The old compact source core survives in the auxiliary-crosscut overlay.
theorem
Schoenflies.SourceNonboundarySegmentCover.crosscut_subset_crosscutOverlay
{γ : 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)
:
J.seg ⊆ (Q.crosscutOverlay J p s epsilon extra).pointSet segmentDrawing
The entire auxiliary segment survives in the overlay.
theorem
Schoenflies.SourceNonboundarySegmentCover.localGrid_subset_crosscutOverlay
{γ : 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)
:
cover (localGridEdges p s (localGridCount s epsilon)) ⊆ (Q.crosscutOverlay J p s epsilon extra).pointSet segmentDrawing
The entire local grid survives in the auxiliary-crosscut overlay.
theorem
Schoenflies.SourceNonboundarySegmentCover.sourceCoreVertices_subset_crosscutOverlay
{γ : 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 : ℝ}
(hs : 0 < s)
(hJ : J.Nondeg)
(extra : List Plane)
:
P.sourceNonboundaryGraph.vertexSet ⊆ (Q.crosscutOverlay J p s epsilon extra).vertexSet
Every old compact-core vertex is retained by the auxiliary-crosscut overlay.
theorem
Schoenflies.SourceNonboundarySegmentCover.crosscutEnds_subset_crosscutOverlay
{γ : 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 : ℝ}
(hs : 0 < s)
(hJ : J.Nondeg)
(extra : List Plane)
:
{J.1, J.2} ⊆ (Q.crosscutOverlay J p s epsilon extra).vertexSet
Both endpoints of the auxiliary crosscut are overlay vertices.
theorem
Schoenflies.SourceNonboundarySegmentCover.localGridVertices_subset_crosscutOverlay
{γ : 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 : ℝ}
(hs : 0 < s)
(hJ : J.Nondeg)
(extra : List Plane)
:
(localGrid p s (localGridCount s epsilon)).vertexSet ⊆ (Q.crosscutOverlay J p s epsilon extra).vertexSet
Every raw local-grid vertex is retained by the auxiliary-crosscut overlay.
theorem
Schoenflies.SourceNonboundarySegmentCover.crosscutOverlay_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}
{R : Piece}
(hR : R ∈ (Q.crosscutOverlay J p s epsilon extra).edgeSet)
:
Every overlay edge is cut from the old compact cover, the auxiliary crosscut, or the local grid.
theorem
Schoenflies.SourceNonboundarySegmentCover.crosscutOverlay_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 : ℝ}
(hs : 0 < s)
(hJdom : J.seg ⊆ srcDom)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
(extra : List Plane)
:
(Q.crosscutOverlay J p s epsilon extra).pointSet segmentDrawing ⊆ srcDom
If both the crosscut and the window lie in the open source domain, the entire auxiliary overlay lies in the closed source domain.
theorem
Schoenflies.SourceNonboundarySegmentCover.crosscutOverlay_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 : ℝ}
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
(extra : List Plane)
{R : Piece}
:
R ∈ (Q.crosscutOverlay J p s epsilon extra).edgeSet →
IsPolygonal (Graph.edgeArc segmentDrawing R) ∧ Graph.edgeArc segmentDrawing R \ (Q.crosscutOverlay J p s epsilon extra).vertexSet ⊆ srcDom \ srcOuter
Every auxiliary-overlay edge is polygonal and has all nonvertex points in the open source domain.
theorem
Schoenflies.SourceNonboundarySegmentCover.crosscutOverlay_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 : ℝ}
(hs : 0 < s)
(hJ : J.Nondeg)
(extra : List Plane)
{e : γ}
:
e ∈ P.str.skel.edgeSet →
e ∉ P.str.outerGraph.edgeSet →
∀ {R : Piece},
R ∈ (Q.crosscutOverlay J p s epsilon extra).edgeSet →
(Graph.edgeArc segmentDrawing R ∩ (P.src.cell e \ (Q.crosscutOverlay J p s epsilon extra).vertexSet)).Nonempty →
Graph.edgeArc segmentDrawing R ⊆ Graph.edgeArc P.src.drawing e
Away from overlay vertices, an auxiliary-overlay edge meeting an old open nonboundary edge is one of that edge's subdivision pieces.
theorem
Schoenflies.SourceNonboundarySegmentCover.crosscutOverlay_grid_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 : ℝ}
(hs : 0 < s)
(hJ : J.Nondeg)
(extra : List Plane)
{A : Piece}
:
A ∈ (localGrid p s (localGridCount s epsilon)).edgeSet →
∀ {R : Piece},
R ∈ (Q.crosscutOverlay J p s epsilon extra).edgeSet →
(Graph.edgeArc segmentDrawing R ∩ (Graph.edgeArc segmentDrawing A \ (Q.crosscutOverlay J p s epsilon extra).vertexSet)).Nonempty →
Graph.edgeArc segmentDrawing R ⊆ Graph.edgeArc segmentDrawing A
Away from overlay vertices, an auxiliary-overlay edge meeting a raw local-grid edge is one of that edge's subdivision pieces.
theorem
Schoenflies.SourceNonboundarySegmentCover.crosscutOverlay_crosscut_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 : ℝ}
(hs : 0 < s)
(hJ : J.Nondeg)
(extra : List Plane)
{R : Piece}
:
R ∈ (Q.crosscutOverlay J p s epsilon extra).edgeSet →
(Graph.edgeArc segmentDrawing R ∩ (Graph.edgeArc segmentDrawing J \ (Q.crosscutOverlay J p s epsilon extra).vertexSet)).Nonempty →
Graph.edgeArc segmentDrawing R ⊆ Graph.edgeArc segmentDrawing J
Away from overlay vertices, an edge meeting the auxiliary crosscut is one of the crosscut's subdivision pieces.
theorem
Schoenflies.SourceNonboundarySegmentCover.crosscutOverlay_localGrid_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 : ℝ}
(hs : 0 < s)
(hJ : J.Nondeg)
(extra : List Plane)
:
IsPlaneSubdivisionExtension (localGrid p s (localGridCount s epsilon)) segmentDrawing
(Q.crosscutOverlay J p s epsilon extra) segmentDrawing
The auxiliary straight-line overlay contains a plane subdivision of the raw local grid.
theorem
Schoenflies.SourceNonboundarySegmentCover.pieceListGraph_single_isDrawing
{J : Piece}
(hJ : J.Nondeg)
:
A single nondegenerate straight segment, with its two ends as vertices, is a plane drawing.
Fresh relabelling and the wild outer graph #
structure
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling
{γ : 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)
:
Type u_1
Fresh abstract edge names for an auxiliary-crosscut inner overlay.
- name : Piece → γ
Assignment of overlay vertices, edges and faces to fresh cell names.
- name_inj : Set.InjOn self.name (Q.crosscutOverlay J p s epsilon extra).edgeSet
Instances For
theorem
Schoenflies.SourceNonboundarySegmentCover.exists_crosscutOverlayRelabeling
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
(Q : SourceNonboundarySegmentCover P)
[Infinite γ]
(J : Piece)
(p : Plane)
(s epsilon : ℝ)
(extra : List Plane)
:
Nonempty (Q.CrosscutOverlayRelabeling J p s epsilon extra)
An infinite cell-name type supplies fresh names for the auxiliary-crosscut overlay.
@[reducible, inline]
abbrev
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.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}
(_w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
:
The old outer graph, still drawn on the wild source curve.
Equations
- _w.outerGraph = Graph.map P.src.pos P.str.outerGraph
Instances For
@[reducible, inline]
noncomputable abbrev
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
:
The freshly relabelled auxiliary-crosscut inner overlay.
Equations
- w.innerGraph = (Q.crosscutOverlay J p s epsilon extra).relabelEdges w.name ⋯
Instances For
noncomputable def
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
:
The mixed crosscut source graph.
Equations
- w.graph = w.outerGraph.union w.innerGraph
Instances For
noncomputable def
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
:
The mixed drawing keeps the wild outer parametrizations and uses straight segments on all fresh inner edges.
Equations
- w.drawing e = if e ∈ P.str.outerGraph.edgeSet then P.src.drawing e else (Q.crosscutOverlay J p s epsilon extra).relabelDrawing w.name Schoenflies.segmentDrawing e
Instances For
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
:
Old outer names and freshly allocated inner names are disjoint.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
{e : γ}
(he : e ∈ P.str.outerGraph.edgeSet)
:
On an old outer edge the mixed drawing is the old source drawing.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
{e : γ}
(he : e ∈ w.innerGraph.edgeSet)
:
On a fresh inner edge the mixed drawing is its relabelled segment drawing.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
:
The mixed drawing restricts to a drawing of the old wild outer graph.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
(hs : 0 < s)
(hJ : J.Nondeg)
:
The mixed drawing restricts to the relabelled auxiliary-crosscut inner overlay.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
:
The outer part occupies exactly the wild source curve.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
:
The inner part occupies exactly the straight-line auxiliary-crosscut overlay.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
:
The wild outer graph and the auxiliary-crosscut inner overlay form a plane drawing.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
:
The mixed crosscut source graph is finite.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
:
w.graph.pointSet w.drawing = srcOuter ∪ (P.sourceNonboundaryGraph.pointSet P.src.drawing ∪ J.seg ∪ cover (localGridEdges p s (localGridCount s epsilon)))
The mixed graph occupies the wild outer curve, old compact core, auxiliary crosscut, and local grid.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.sourceSkeleton_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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
:
P.src.skeletonSet ⊆ w.graph.pointSet w.drawing
The complete old source skeleton is retained by the mixed crosscut graph.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.sourceVertices_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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
(hs : 0 < s)
(hJ : J.Nondeg)
:
Every old source vertex is retained by the mixed crosscut graph.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.crosscutEnds_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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
(hs : 0 < s)
(hJ : J.Nondeg)
:
Both ends of the auxiliary crosscut are vertices of the mixed graph.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
(hs : 0 < s)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
:
The mixed crosscut graph stays in the closed source domain.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
(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 on the wild outer curve or is a polygonal inner edge whose nonvertex points lie in the open source domain.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
{e : γ}
:
An edge of the mixed crosscut graph meeting an old open source edge away from mixed vertices is one of that edge's subdivision pieces.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
:
The mixed crosscut graph contains a plane subdivision of the complete old source drawing.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.sourceTrace_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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
:
(w.graph.traceGraph w.drawing P.src.skeletonSet).IsTwoConnected
The old-source trace inside the mixed crosscut graph remains 2-connected.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.localGridVertices_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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
(hs : 0 < s)
(hJ : J.Nondeg)
:
(localGrid p s (localGridCount s epsilon)).vertexSet ⊆ w.graph.vertexSet
Every raw local-grid vertex is retained by the mixed crosscut graph.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.localGrid_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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
:
(localGrid p s (localGridCount s epsilon)).pointSet segmentDrawing ⊆ w.graph.pointSet w.drawing
The complete raw local-grid carrier is retained by the mixed crosscut graph.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.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}
{J : Piece}
{p : Plane}
{s epsilon : ℝ}
{extra : List Plane}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
(hs : 0 < s)
(hJ : J.Nondeg)
(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
A mixed edge meeting a raw grid edge away from mixed vertices is a subdivision piece of that grid edge.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.graph_crosscut_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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
{f : γ}
:
f ∈ w.graph.edgeSet →
(Graph.edgeArc w.drawing f ∩ (Graph.edgeArc segmentDrawing J \ w.graph.vertexSet)).Nonempty →
Graph.edgeArc w.drawing f ⊆ Graph.edgeArc segmentDrawing J
A mixed edge meeting the auxiliary crosscut away from mixed vertices is one of the crosscut's subdivision pieces.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.crosscut_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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
:
The mixed graph contains a plane subdivision of the one-edge auxiliary crosscut.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.localGrid_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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
:
IsPlaneSubdivisionExtension (localGrid p s (localGridCount s epsilon)) segmentDrawing w.graph w.drawing
The mixed crosscut graph contains a plane subdivision of the raw local grid.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.localGridTrace_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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
(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 crosscut graph remains 2-connected.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.exists_crosscut_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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
:
The subdivided auxiliary segment is the exact carrier of a path in the mixed graph.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.graph_isTwoConnected_of_crosscut_grid_edge
{γ : 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)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
(hJsource : J.1 ∈ P.src.skeletonSet ∧ J.2 ∈ P.src.skeletonSet)
{A : Piece}
(hA : A ∈ (localGrid p s (localGridCount s epsilon)).edgeSet)
(hAJ : A.seg ⊆ J.seg)
:
If a nondegenerate raw grid edge lies on the auxiliary segment and both crosscut ends lie on the old source skeleton, the old trace, crosscut ear, and grid trace span a 2-connected subgraph. Consequently the complete mixed graph is 2-connected.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.graph_isConnected_diff_of_crosscut_grid_edge
{γ : 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)
(hs : 0 < s)
(hJopen : J.seg ⊆ srcDom \ srcOuter)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
(hsource : IsConnected (P.src.skeletonSet \ srcOuter))
(hJsource : J.1 ∈ P.src.skeletonSet)
{A : Piece}
(hA : A ∈ (localGrid p s (localGridCount s epsilon)).edgeSet)
(hAJ : A.seg ⊆ J.seg)
:
IsConnected (w.graph.pointSet w.drawing \ srcOuter)
If the old nonouter source carrier is connected, adjoining a crosscut whose first endpoint lies on it and a grid edge carried by that crosscut preserves connectedness after removing the wild outer curve.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.graph_isConnected_diff_of_crosscut_grid_edge_of_end_not_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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
(hs : 0 < s)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
(hsource : IsConnected (P.src.skeletonSet \ srcOuter))
(hJsource : J.1 ∈ P.src.skeletonSet ∧ J.2 ∈ P.src.skeletonSet)
(hJattach : J.1 ∉ srcOuter ∨ J.2 ∉ srcOuter)
{A : Piece}
(hA : A ∈ (localGrid p s (localGridCount s epsilon)).edgeSet)
(hAJ : A.seg ⊆ J.seg)
:
IsConnected (w.graph.pointSet w.drawing \ srcOuter)
The boundary-tolerant connectedness argument. The crosscut with its wild-boundary endpoints removed is still connected because it lies between its connected open segment and that segment's closure. Hence one surviving source endpoint joins it to the old nonboundary carrier, while the swallowed grid edge joins it to the grid.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
(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
Once its two global attachment properties are known, the mixed crosscut graph is a complete source extension.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.isSourceExtension_of_crosscut_grid_edge
{γ : 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)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJopen : J.seg ⊆ srcDom \ srcOuter)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
(hsource : IsConnected (P.src.skeletonSet \ srcOuter))
(hJsource : J.1 ∈ P.src.skeletonSet ∧ J.2 ∈ P.src.skeletonSet)
{A : Piece}
(hA : A ∈ (localGrid p s (localGridCount s epsilon)).edgeSet)
(hAJ : A.seg ⊆ J.seg)
:
IsSourceExtension P.src srcOuter srcDom w.graph w.drawing
The crosscut construction is a source extension once its concrete geometric attachment data are supplied; no separate graph-theoretic 2-connectivity or carrier-connectedness hypotheses remain.
theorem
Schoenflies.SourceNonboundarySegmentCover.CrosscutOverlayRelabeling.isSourceExtension_of_crosscut_grid_edge_of_end_not_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}
(w : Q.CrosscutOverlayRelabeling J p s epsilon extra)
(hs : 0 < s)
(hJ : J.Nondeg)
(hJgeom : SourceCrosscutGeometry P J)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
(hsource : IsConnected (P.src.skeletonSet \ srcOuter))
(hJsource : J.1 ∈ P.src.skeletonSet ∧ J.2 ∈ P.src.skeletonSet)
(hJattach : J.1 ∉ srcOuter ∨ J.2 ∉ srcOuter)
{A : Piece}
(hA : A ∈ (localGrid p s (localGridCount s epsilon)).edgeSet)
(hAJ : A.seg ⊆ J.seg)
:
IsSourceExtension P.src srcOuter srcDom w.graph w.drawing
Boundary-tolerant packaging: once one crosscut endpoint survives deletion of the wild outer curve, the generalized crosscut geometry gives the complete source extension.
structure
Schoenflies.LocalGridSourceExtensionData
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
(P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom)
(p : Plane)
(s epsilon : ℝ)
:
Type u_1
The concrete output required from a local-grid source attachment: a finite source extension whose carrier contains the complete raw local grid.
Finite graph extending the source skeleton and local grid.
Planar parametrizations of the extension edges.
- isSourceExtension : IsSourceExtension P.src srcOuter srcDom self.graph self.drawing
- localGrid_subset : (localGrid p s (localGridCount s epsilon)).pointSet segmentDrawing ⊆ self.graph.pointSet self.drawing
Instances For
structure
Schoenflies.RefinedCrosscutOverlayData
{γ : 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 boundary-touching crosscut construction after its two endpoint subdivisions. This packages every global graph property except connectedness after deleting the wild outer curve; that last property is exactly what the blueprint's finite component-joining loop supplies.
- cover : SourceNonboundarySegmentCover r.subdivision.pair
Finite segment cover of the subdivided nonboundary skeleton.
- relabeling : self.cover.CrosscutOverlayRelabeling r.crosscutData.crosscut p s epsilon []
Fresh names for the crosscut and local-grid overlay.
- isDrawing : self.relabeling.graph.IsDrawing self.relabeling.drawing
- isTwoConnected : self.relabeling.graph.IsTwoConnected
- sourceSkeleton_subset : r.subdivision.pair.src.skeletonSet ⊆ self.relabeling.graph.pointSet self.relabeling.drawing
- pointSet_subset : self.relabeling.graph.pointSet self.relabeling.drawing ⊆ srcDom
- localGrid_subset : (localGrid p s (localGridCount s epsilon)).pointSet segmentDrawing ⊆ self.relabeling.graph.pointSet self.relabeling.drawing
Instances For
noncomputable def
Schoenflies.RefinedCrosscutOverlayData.toLocalGridSourceExtensionData
{γ : Type u_1}
{S₀ : CellStructure γ}
{srcOuter srcDom tgtOuter tgtDom : Set Plane}
{P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom}
{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)
(hsource : IsConnected r.subdivision.pair.src.nonboundary)
(hattach : r.crosscutData.crosscut.1 ∉ srcOuter ∨ r.crosscutData.crosscut.2 ∉ srcOuter)
(hA : A ∈ (localGrid p s (localGridCount s epsilon)).edgeSet)
:
LocalGridSourceExtensionData r.subdivision.pair p s epsilon
A refined crosscut overlay is already a complete local-grid source extension whenever at least one crosscut endpoint is not on the wild outer curve.
Equations
- o.toLocalGridSourceExtensionData hs hwindow hsource hattach hA = { graph := o.relabeling.graph, drawing := o.relabeling.drawing, isSourceExtension := ⋯, localGrid_subset := ⋯ }
Instances For
theorem
Schoenflies.GeneratedPair.exists_refinedCrosscutOverlayData
{γ : 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)
(hA : A ∈ (localGrid p s (localGridCount s epsilon)).edgeSet)
:
Nonempty ((r : RefinedSourceFaceCrosscutData P F A) × RefinedCrosscutOverlayData r p s epsilon)
The boundary-touching branch now constructs a plane, 2-connected, domain-contained mixed overlay after a matched subdivision at the two crosscut endpoints. The construction also retains the entire refined source skeleton and the raw local grid.
theorem
Schoenflies.GeneratedPair.exists_localGridSourceExtension_of_face_frontier
{γ : 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)
(hfrontier : frontier (P.src.cell F) ⊆ srcDom \ srcOuter)
(hs : 0 < s)
(hwindow : p.closedSquare s ⊆ srcDom \ srcOuter)
(hsource : IsConnected P.src.nonboundary)
(hA : A ∈ (localGrid p s (localGridCount s epsilon)).edgeSet)
:
Nonempty (LocalGridSourceExtensionData P p s epsilon)
Complete local-grid source attachment for the crosscut case in which the selected source face has no wild-boundary points on its frontier. The face crosscut swallows the chosen raw grid edge, its traced subdivision is attached as an ear, and the grid trace is then glued along the two distinct ends of that edge.