Overlaying a target skeleton with the anchored square mesh

A fresh square mesh does not generally contain the current target skeleton: already at stage zero the target has an arbitrary straight chord which need not be radial or lie on a mesh ring. The ambient graph for reverse finite transfer must therefore be the polygonal overlay of the two finite segment families.

TargetSegmentCover writes the whole current target skeleton as a finite exact segment cover. It also remembers which old abstract edge supplied each segment; that provenance is what will prove the subdivision clause after transverse intersections have been made vertices.

TargetSegmentCover.meshOverlay is the combined graph. It overlays the target cover with the already-subdivided edges of the anchored mesh, and its cut list contains both the mesh anchors and every old target vertex. The basic carrier, drawing, containment, edge-source, and 2-connectivity facts are established here. The nonouter target-edge carriers form a canonical finite connected cover of the old open skeleton. A uniform positive width for this cover, together with the radial mesh estimate, shows that every sufficiently fine dense mesh meets every cover piece. Consequently the combined overlay is a complete source extension at some positive scale below 4. Relative boundary anchoring and no-new-nonouter-incidence are proved for clean fresh lists and transported through edge relabelling, so the overlay now feeds directly into reverse finite transfer. FreshDenseSelection.lean constructs the required finite clean separator list from the dense strongly-accessible boundary points and packages the resulting reverse-transfer stage.

Blueprint

• Schoenflies.TargetSegmentCover — the finite segment presentation of the current polygonal target skeleton.
• Schoenflies.GeneratedPair.exists_targetSegmentCover — every generated pair supplies that presentation.
• Schoenflies.TargetSegmentCover.meshOverlay — the current target skeleton overlaid with the anchored square mesh.
• Schoenflies.TargetSegmentCover.meshOverlay_pointSet — the combined graph occupies exactly the union of the two carriers.
• Schoenflies.TargetSegmentCover.meshOverlay_isTwoConnected — the two subdivision traces glue along two fresh boundary vertices to make the combined overlay 2-connected.
• Schoenflies.TargetSegmentCover.noNewNonouterIncidenceAtBoundary_meshOverlay — clean fresh spokes cannot create a second nonouter incidence against the current target trace.
• Schoenflies.finiteOpenTargetCover — the nonouter edge carriers, with the model curve removed, form a finite connected nontrivial cover of the old open target skeleton.
• Schoenflies.exists_fine_openTarget_scale — every generated target has a positive scale below 4 at which all pieces of that cover are wider than the mesh.
• Schoenflies.TargetSegmentCover.exists_scale_isSourceExtension_relabelledMeshOverlay — at that scale, every dense anchored mesh gives the complete relabelled source extension.
• Schoenflies.TargetSegmentCover.finite_transfer_toward_source_relabelledMeshOverlay_of_outerCycle — the accessible clean overlay performs the complete reverse finite transfer.

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

A finite exact segment presentation of the target skeleton, with each segment traced back to an old abstract edge.

• pieces : List Piece

  The straight segments covering the target skeleton.

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

  No listed segment is degenerate.

• cover_eq : cover self.pieces = P.tgt.skeletonSet

  The listed segments occupy exactly the target skeleton.

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

  Every listed segment came from one old target edge.

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

Every generated pair has a finite segment presentation of its polygonal target skeleton.

noncomputable def Schoenflies.TargetSegmentCover.squareMeshPieces (delta : ℝ) (fresh anchors : List Plane) : List Piece

The already-subdivided edges of the anchored square mesh, listed as straight pieces.

Equations

• Schoenflies.TargetSegmentCover.squareMeshPieces delta fresh anchors = (Schoenflies.squareMesh delta fresh anchors).edgeFinset.toList

@[simp]

theorem Schoenflies.TargetSegmentCover.mem_squareMeshPieces {delta : ℝ} {fresh anchors : List Plane} {R : Piece} : R ∈ squareMeshPieces delta fresh anchors ↔ R ∈ (squareMesh delta fresh anchors).edgeSet

theorem Schoenflies.TargetSegmentCover.cover_squareMeshPieces (delta : ℝ) (fresh anchors : List Plane) : cover (squareMeshPieces delta fresh anchors) = (squareMesh delta fresh anchors).pointSet segmentDrawing

Listing the edges loses no carrier: every square-mesh vertex is an end of one of its edges.

noncomputable def Schoenflies.TargetSegmentCover.meshPieces {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) (delta : ℝ) (fresh anchors : List Plane) : List Piece

The two source families for the combined target overlay.

Equations

• Q.meshPieces delta fresh anchors = Q.pieces ++ Schoenflies.TargetSegmentCover.squareMeshPieces delta fresh anchors

noncomputable def Schoenflies.TargetSegmentCover.meshOverlay {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) (delta : ℝ) (fresh anchors : List Plane) : Graph Plane Piece

The target skeleton overlaid with the anchored square mesh. Old vertices and prescribed mesh anchors are explicitly included in the cut list.

Equations

• Q.meshOverlay delta fresh anchors = Schoenflies.attachGraph (Q.meshPieces delta fresh anchors) (anchors ++ P.tgt.graph.vertexFinset.toList)

instance Schoenflies.TargetSegmentCover.meshOverlay_finite {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) (delta : ℝ) (fresh anchors : List Plane) : (Q.meshOverlay delta fresh anchors).Finite

theorem Schoenflies.TargetSegmentCover.meshPieces_nondeg {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (delta : ℝ) (anchors : List Plane) (R : Piece) : R ∈ Q.meshPieces delta fresh anchors → R.Nondeg

Every source segment of the combined overlay is nondegenerate.

theorem Schoenflies.TargetSegmentCover.meshOverlay_isDrawing {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (delta : ℝ) (anchors : List Plane) : (Q.meshOverlay delta fresh anchors).IsDrawing segmentDrawing

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

theorem Schoenflies.TargetSegmentCover.meshOverlay_pointSet {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) (delta : ℝ) (fresh anchors : List Plane) : (Q.meshOverlay delta fresh anchors).pointSet segmentDrawing = P.tgt.skeletonSet ∪ (squareMesh delta fresh anchors).pointSet segmentDrawing

The combined overlay occupies exactly the current target skeleton together with the square mesh.

theorem Schoenflies.TargetSegmentCover.targetSkeleton_subset_meshOverlay {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) (delta : ℝ) (fresh anchors : List Plane) : P.tgt.skeletonSet ⊆ (Q.meshOverlay delta fresh anchors).pointSet segmentDrawing

The current target skeleton is contained in the combined overlay.

theorem Schoenflies.TargetSegmentCover.squareMesh_subset_meshOverlay {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) (delta : ℝ) (fresh anchors : List Plane) : (squareMesh delta fresh anchors).pointSet segmentDrawing ⊆ (Q.meshOverlay delta fresh anchors).pointSet segmentDrawing

The whole anchored square mesh is contained in the combined overlay.

theorem Schoenflies.TargetSegmentCover.targetVertices_subset_meshOverlay {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (delta : ℝ) (anchors : List Plane) : P.tgt.graph.vertexSet ⊆ (Q.meshOverlay delta fresh anchors).vertexSet

Every old target vertex is explicitly retained as a vertex of the combined overlay.

theorem Schoenflies.TargetSegmentCover.squareMeshVertices_subset_meshOverlay {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (delta : ℝ) (anchors : List Plane) : (squareMesh delta fresh anchors).vertexSet ⊆ (Q.meshOverlay delta fresh anchors).vertexSet

Every square-mesh vertex is an endpoint of a source piece for the combined overlay.

theorem Schoenflies.TargetSegmentCover.meshOverlay_edge_source {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {delta : ℝ} {fresh anchors : List Plane} {R : Piece} (hR : R ∈ (Q.meshOverlay delta fresh anchors).edgeSet) : (∃ A ∈ Q.pieces, R.seg ⊆ A.seg) ∨ ∃ A ∈ meshSegments (meshCount delta) fresh, R.seg ⊆ A.seg

Every edge of the combined overlay is a subsegment either of an old target segment or of a square-mesh source segment.

theorem Schoenflies.TargetSegmentCover.meshOverlay_edge_source_squareMesh {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {delta : ℝ} {fresh anchors : List Plane} {R : Piece} (hR : R ∈ (Q.meshOverlay delta fresh anchors).edgeSet) : (∃ A ∈ Q.pieces, R.seg ⊆ A.seg) ∨ ∃ A ∈ (squareMesh delta fresh anchors).edgeSet, R.seg ⊆ A.seg

The sharper edge-source dichotomy used at the boundary: a mesh-sourced overlay edge lies inside one actual edge of the already-subdivided square mesh.

theorem Schoenflies.TargetSegmentCover.segments_from_common_end_comparable {z a r s : Plane} (hza : z ≠ a) (hr : r ∈ segment ℝ z a) (hs : s ∈ segment ℝ z a) : segment ℝ z r ⊆ segment ℝ z s ∨ segment ℝ z s ⊆ segment ℝ z r

Two subsegments of one nondegenerate segment that start at the same end are comparable by inclusion.

theorem Schoenflies.TargetSegmentCover.piece_segments_comparable_of_common_source_end {A R S : Piece} {z : Plane} (hA : A.Nondeg) (hzA : z = A.1 ∨ z = A.2) (hRA : R.seg ⊆ A.seg) (hSA : S.seg ⊆ A.seg) (hzR : z = R.1 ∨ z = R.2) (hzS : z = S.1 ∨ z = S.2) : R.seg ⊆ S.seg ∨ S.seg ⊆ R.seg

Two pieces contained in the same nondegenerate source piece and sharing one of its ends are comparable. This is the piece-level form needed to identify two overlay fragments cut from the unique square-mesh spoke at a fresh boundary point.

theorem Schoenflies.TargetSegmentCover.meshOverlay_edge_subset {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (delta : ℝ) (anchors : List Plane) ⦃e : γ⦄ : e ∈ P.str.skel.edgeSet → ∀ ⦃R : Piece⦄, R ∈ (Q.meshOverlay delta fresh anchors).edgeSet → (Graph.edgeArc segmentDrawing R ∩ (P.tgt.cell e \ (Q.meshOverlay delta fresh anchors).vertexSet)).Nonempty → Graph.edgeArc segmentDrawing R ⊆ Graph.edgeArc P.tgt.drawing e

Away from the vertices created by the overlay, an overlay edge meeting an old open target edge is one of its subdivision pieces. At a transverse crossing the common point is an overlay vertex, so the hypothesis is intentionally false there.

theorem Schoenflies.TargetSegmentCover.target_isPlaneSubdivisionExtension {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (delta : ℝ) (anchors : List Plane) : IsPlaneSubdivisionExtension P.tgt.graph P.tgt.drawing (Q.meshOverlay delta fresh anchors) segmentDrawing

The combined overlay locally contains an edge subdivision of the old target drawing.

theorem Schoenflies.TargetSegmentCover.squareMesh_isPlaneSubdivisionExtension {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (delta : ℝ) (anchors : List Plane) : IsPlaneSubdivisionExtension (squareMesh delta fresh anchors) segmentDrawing (Q.meshOverlay delta fresh anchors) segmentDrawing

The combined overlay also locally contains an edge subdivision of the anchored square mesh. Using the mesh's already-subdivided edges as source pieces makes the proof immediate.

theorem Schoenflies.TargetSegmentCover.targetTrace_isTwoConnected {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (delta : ℝ) (anchors : List Plane) : ((Q.meshOverlay delta fresh anchors).traceGraph segmentDrawing P.tgt.skeletonSet).IsTwoConnected

The old-target trace inside the combined overlay remains 2-connected.

theorem Schoenflies.TargetSegmentCover.squareMeshTrace_isTwoConnected {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) {delta : ℝ} (hdense : FreshDense fresh delta) (hdelta : delta < 4) (anchors : List Plane) : ((Q.meshOverlay delta fresh anchors).traceGraph segmentDrawing ((squareMesh delta fresh anchors).pointSet segmentDrawing)).IsTwoConnected

Under the usual density hypotheses, the square-mesh trace inside the combined overlay remains 2-connected.

theorem Schoenflies.TargetSegmentCover.meshOverlay_isTwoConnected {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) {delta : ℝ} (hdense : FreshDense fresh delta) (hdelta : delta < 4) (anchors : List Plane) : (Q.meshOverlay delta fresh anchors).IsTwoConnected

The combined target/mesh overlay is 2-connected. The two subdivision traces are glued at two distinct fresh boundary vertices, and together they contain every overlay vertex.

theorem Schoenflies.TargetSegmentCover.meshOverlay_pointSet_subset {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (delta : ℝ) (anchors : List Plane) : (Q.meshOverlay delta fresh anchors).pointSet segmentDrawing ⊆ Plane.closedSquare 0 1

The combined overlay stays in the closed target square.

theorem Schoenflies.TargetSegmentCover.meshOverlay_edge_dichotomy {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (delta : ℝ) (anchors : List Plane) ⦃R : Piece⦄ : R ∈ (Q.meshOverlay delta fresh anchors).edgeSet → Graph.edgeArc segmentDrawing R ⊆ modelCurve ∨ IsPolygonal (Graph.edgeArc segmentDrawing R) ∧ Graph.edgeArc segmentDrawing R \ (Q.meshOverlay delta fresh anchors).vertexSet ⊆ Plane.closedSquare 0 1 \ modelCurve

Every combined-overlay edge either lies on the model curve or is a polygonal edge whose nonvertex points lie in the open target square. A nonouter edge cannot meet the model curve away from overlay vertices: the outer-ring segment through such a point would give a second edge of the plane drawing there.

theorem Schoenflies.TargetSegmentCover.newTargetBoundaryAnchored_meshOverlay {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (hstrong : ∀ z ∈ fresh, StronglyAccessible (srcDom \ srcOuter) (P.homeo.invFun z)) (delta : ℝ) (anchors : List Plane) : NewTargetBoundaryAnchored P P.tgt.skeletonSet (Q.meshOverlay delta fresh anchors) segmentDrawing

New nonouter boundary edges of the combined overlay come from the square mesh and hence end at prescribed fresh points. Old-target-sourced overlay edges are already covered by every trace containing the original target skeleton, so they cannot be new.

def Schoenflies.TargetSegmentCover.FreshAvoidsTargetNonouterEdges {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)) (fresh : List Plane) : Prop

Fresh mesh anchors avoid the carriers of all old nonouter target edges. This is the finite cleanliness condition which separates a genuinely new spoke from the current target trace at the distinguished boundary.

Equations

• Schoenflies.TargetSegmentCover.FreshAvoidsTargetNonouterEdges P fresh = ∀ z ∈ fresh, ∀ e ∈ P.str.skel.edgeSet, e ∉ P.str.outerGraph.edgeSet → z ∉ Graph.edgeArc P.tgt.drawing e

theorem Schoenflies.TargetSegmentCover.mem_targetVertex_of_mem_nonouter_edgeArc_modelCurve {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} {e : γ} (he : e ∈ P.str.skel.edgeSet) (heNotOuter : e ∉ P.str.outerGraph.edgeSet) {z : Plane} (hze : z ∈ Graph.edgeArc P.tgt.drawing e) (hz : z ∈ modelCurve) : z ∈ P.tgt.graph.vertexSet

A nonouter target edge can meet the distinguished boundary only at an old target vertex. This turns the cleanliness requirement into avoidance of one finite vertex set.

theorem Schoenflies.TargetSegmentCover.freshAvoidsTargetNonouterEdges_of_avoids_targetVertices {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (havoid : ∀ z ∈ fresh, z ∉ P.tgt.graph.vertexSet) : FreshAvoidsTargetNonouterEdges P fresh

Avoiding the finite old target vertex set is sufficient for clean fresh anchors.

theorem Schoenflies.TargetSegmentCover.meshOverlay_inc_endpoint {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {delta : ℝ} {fresh anchors : List Plane} {R : Piece} {z : Plane} (hinc : (Q.meshOverlay delta fresh anchors).Inc R z) : z = R.1 ∨ z = R.2

Incidence with an edge of the target/mesh overlay means being one of the two endpoints of that piece.

theorem Schoenflies.TargetSegmentCover.meshOverlay_mesh_edges_eq_at_boundary {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (delta : ℝ) (anchors : List Plane) {z : Plane} (hz : z ∈ modelCurve) {R S : Piece} (hR : R ∈ (Q.meshOverlay delta fresh anchors).edgeSet) (hS : S ∈ (Q.meshOverlay delta fresh anchors).edgeSet) (hRinc : (Q.meshOverlay delta fresh anchors).Inc R z) (hSinc : (Q.meshOverlay delta fresh anchors).Inc S z) (hRnot : ¬Graph.edgeArc segmentDrawing R ⊆ modelCurve) (hSnot : ¬Graph.edgeArc segmentDrawing S ⊆ modelCurve) {A C : Piece} (hA : A ∈ (squareMesh delta fresh anchors).edgeSet) (hC : C ∈ (squareMesh delta fresh anchors).edgeSet) (hRA : R.seg ⊆ A.seg) (hSC : S.seg ⊆ C.seg) : R = S

Two mesh-sourced, nonouter overlay edges incident at the same boundary point coincide. The square mesh has one spoke there; both overlay pieces start at the boundary end of that spoke, so their segment carriers are nested, and planarity identifies their edge names.

theorem Schoenflies.TargetSegmentCover.noNewNonouterIncidenceAtBoundary_meshOverlay {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (havoid : FreshAvoidsTargetNonouterEdges P fresh) (delta : ℝ) (anchors : List Plane) : NoNewNonouterIncidenceAtBoundary P.tgt.skeletonSet (Q.meshOverlay delta fresh anchors) segmentDrawing modelCurve

Under the finite cleanliness condition, no new nonouter overlay edge can meet a nonouter edge of a trace already covering the old target skeleton at the distinguished boundary.

theorem Schoenflies.TargetSegmentCover.newTargetBoundaryAnchored_relabelledMeshOverlay {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (hstrong : ∀ z ∈ fresh, StronglyAccessible (srcDom \ srcOuter) (P.homeo.invFun z)) (delta : ℝ) (anchors : List Plane) (name : Piece → γ) (hname : Set.InjOn name (Q.meshOverlay delta fresh anchors).edgeSet) : NewTargetBoundaryAnchored P P.tgt.skeletonSet ((Q.meshOverlay delta fresh anchors).relabelEdges name hname) ((Q.meshOverlay delta fresh anchors).relabelDrawing name segmentDrawing)

The relative boundary anchoring of the overlay survives its injective edge renaming.

theorem Schoenflies.TargetSegmentCover.noNewNonouterIncidenceAtBoundary_relabelledMeshOverlay {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (havoid : FreshAvoidsTargetNonouterEdges P fresh) (delta : ℝ) (anchors : List Plane) (name : Piece → γ) (hname : Set.InjOn name (Q.meshOverlay delta fresh anchors).edgeSet) : NoNewNonouterIncidenceAtBoundary P.tgt.skeletonSet ((Q.meshOverlay delta fresh anchors).relabelEdges name hname) ((Q.meshOverlay delta fresh anchors).relabelDrawing name segmentDrawing) modelCurve

The relative no-new-incidence property of a clean overlay survives its injective edge renaming.

def Schoenflies.TargetSegmentCover.OpenTargetLocallyWiderThan {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)) (delta : ℝ) : Prop

A quantitative local-width condition on the old open target skeleton. Every point lies in a connected subset containing two points farther apart than the proposed mesh scale.

Equations

• One or more equations did not get rendered due to their size.

structure Schoenflies.TargetSegmentCover.FiniteOpenTargetCover {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)) : Type

Finitely many nontrivial connected pieces cover the old open target skeleton. This is the purely target-side finiteness datum from which a uniform positive mesh scale is extracted.

• pieces : List (Set Plane)

  The connected pieces.

• covers (z : Plane) : z ∈ P.tgt.skeletonSet \ modelCurve → ∃ A ∈ self.pieces, z ∈ A

  Every open-skeleton point lies in one listed piece.

• subset_open (A : Set Plane) : A ∈ self.pieces → A ⊆ P.tgt.skeletonSet \ modelCurve

  Every listed piece lies in the old open skeleton.

• preconnected (A : Set Plane) : A ∈ self.pieces → IsPreconnected A

  Every listed piece is connected.

• nontrivial (A : Set Plane) : A ∈ self.pieces → ∃ x ∈ A, ∃ y ∈ A, x ≠ y

  No listed piece is a singleton.

theorem Schoenflies.TargetSegmentCover.IsArcBetween.exists_two_mem_diff {A : Set Plane} {p q : Plane} (h : IsArcBetween A p q) : ∃ x ∈ A \ {p, q}, ∃ y ∈ A \ {p, q}, x ≠ y

The interior of a nondegenerate arc contains two distinct points.

noncomputable def Schoenflies.TargetSegmentCover.openTargetEdgePieces {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)) : List (Set Plane)

The finite family of nonouter target-edge carriers, with the model curve removed.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Schoenflies.TargetSegmentCover.mem_openTargetEdgePieces {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} {A : Set Plane} : A ∈ openTargetEdgePieces P ↔ ∃ e ∈ P.str.skel.edgeSet, e ∉ P.str.outerGraph.edgeSet ∧ A = Graph.edgeArc P.tgt.drawing e \ modelCurve

noncomputable def Schoenflies.TargetSegmentCover.finiteOpenTargetCover {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)) : FiniteOpenTargetCover P

The nonouter edge carriers form a finite connected, nontrivial cover of the whole old open target skeleton.

Equations

• Schoenflies.TargetSegmentCover.finiteOpenTargetCover P = { pieces := Schoenflies.TargetSegmentCover.openTargetEdgePieces P, covers := ⋯, subset_open := ⋯, preconnected := ⋯, nontrivial := ⋯ }

theorem Schoenflies.TargetSegmentCover.exists_uniform_piece_width (pieces : List (Set Plane)) (hnontrivial : ∀ A ∈ pieces, ∃ x ∈ A, ∃ y ∈ A, x ≠ y) : ∃ (delta : ℝ), 0 < delta ∧ ∀ A ∈ pieces, ∃ x ∈ A, ∃ y ∈ A, delta < dist x y

A finite list of nontrivial sets has a uniform positive lower bound on one pairwise distance chosen from each set.

theorem Schoenflies.TargetSegmentCover.FiniteOpenTargetCover.exists_locallyWiderThan {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (C : FiniteOpenTargetCover P) : ∃ (delta : ℝ), 0 < delta ∧ OpenTargetLocallyWiderThan P delta

A finite open-target cover supplies a positive scale at which every open-skeleton point has a connected neighborhood wider than the mesh.

theorem Schoenflies.TargetSegmentCover.OpenTargetLocallyWiderThan.mono {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} {delta epsilon : ℝ} (h : OpenTargetLocallyWiderThan P delta) (hle : epsilon ≤ delta) : OpenTargetLocallyWiderThan P epsilon

The local-width condition is preserved when the proposed mesh scale is decreased.

theorem Schoenflies.TargetSegmentCover.exists_fine_openTarget_scale {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)) : ∃ (delta : ℝ), 0 < delta ∧ delta < 4 ∧ OpenTargetLocallyWiderThan P delta

Every generated target has a positive mesh scale below 4 at which all of its open edge pieces are wider than the mesh.

theorem Schoenflies.TargetSegmentCover.exists_fine_openTarget_scale_lt {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)) {bound : ℝ} (hbound : 0 < bound) : ∃ (delta : ℝ), 0 < delta ∧ delta < 4 ∧ delta < bound ∧ OpenTargetLocallyWiderThan P delta

The locally-wide scale may be chosen below any prescribed positive bound.

theorem Schoenflies.TargetSegmentCover.mesh_hits_openTarget_of_locallyWider {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)) {fresh : List Plane} {delta : ℝ} (hdelta : 0 < delta) (hdense : FreshDense fresh delta) (hwide : OpenTargetLocallyWiderThan P delta) (anchors : List Plane) (z : Plane) : z ∈ P.tgt.skeletonSet \ modelCurve → ∃ A ⊆ P.tgt.skeletonSet \ modelCurve, IsPreconnected A ∧ z ∈ A ∧ (A ∩ ((squareMesh delta fresh anchors).pointSet segmentDrawing \ modelCurve)).Nonempty

A connected old-skeleton piece wider than the mesh scale must meet the mesh. Otherwise the radial mesh estimate bounds all of its pairwise distances by a number strictly below delta.

theorem Schoenflies.TargetSegmentCover.meshOverlay_isConnected_diff_of_hits {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) {z₀ : Plane} (hz₀ : z₀ ∈ fresh) (delta : ℝ) (anchors : List Plane) (hhit : ∀ z ∈ P.tgt.skeletonSet \ modelCurve, ∃ A ⊆ P.tgt.skeletonSet \ modelCurve, IsPreconnected A ∧ z ∈ A ∧ (A ∩ ((squareMesh delta fresh anchors).pointSet segmentDrawing \ modelCurve)).Nonempty) : IsConnected ((Q.meshOverlay delta fresh anchors).pointSet segmentDrawing \ modelCurve)

If every connected piece of the old open skeleton meets the connected open part of the mesh, their union is connected. This is the set-theoretic core of the quantitative mesh-hitting argument.

theorem Schoenflies.TargetSegmentCover.isSourceExtension_relabelledMeshOverlay {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (delta : ℝ) (anchors : List Plane) (name : Piece → γ) (hname : Set.InjOn name (Q.meshOverlay delta fresh anchors).edgeSet) (htwo : (Q.meshOverlay delta fresh anchors).IsTwoConnected) (hconnected : IsConnected ((Q.meshOverlay delta fresh anchors).pointSet segmentDrawing \ modelCurve)) : IsSourceExtension P.tgt modelCurve (Plane.closedSquare 0 1) ((Q.meshOverlay delta fresh anchors).relabelEdges name hname) ((Q.meshOverlay delta fresh anchors).relabelDrawing name segmentDrawing)

After injective edge relabelling, the combined overlay is a target extension as soon as its two genuinely global assembly properties—2-connectivity and connectedness off the boundary—are available. Every local subdivision and geometric field is discharged above.

theorem Schoenflies.TargetSegmentCover.isSourceExtension_relabelledMeshOverlay_of_hits {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) {z₀ : Plane} (hz₀ : z₀ ∈ fresh) (delta : ℝ) (anchors : List Plane) (name : Piece → γ) (hname : Set.InjOn name (Q.meshOverlay delta fresh anchors).edgeSet) (htwo : (Q.meshOverlay delta fresh anchors).IsTwoConnected) (hhit : ∀ z ∈ P.tgt.skeletonSet \ modelCurve, ∃ A ⊆ P.tgt.skeletonSet \ modelCurve, IsPreconnected A ∧ z ∈ A ∧ (A ∩ ((squareMesh delta fresh anchors).pointSet segmentDrawing \ modelCurve)).Nonempty) : IsSourceExtension P.tgt modelCurve (Plane.closedSquare 0 1) ((Q.meshOverlay delta fresh anchors).relabelEdges name hname) ((Q.meshOverlay delta fresh anchors).relabelDrawing name segmentDrawing)

The mesh-hitting condition is enough to discharge the connectedness field of the target extension. Thus only 2-connectivity and the quantitative fact that the mesh meets every connected piece of the old open skeleton remain.

theorem Schoenflies.TargetSegmentCover.isSourceExtension_relabelledMeshOverlay_of_dense_hits {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) {delta : ℝ} (hdense : FreshDense fresh delta) (hdelta : delta < 4) (anchors : List Plane) (name : Piece → γ) (hname : Set.InjOn name (Q.meshOverlay delta fresh anchors).edgeSet) (hhit : ∀ z ∈ P.tgt.skeletonSet \ modelCurve, ∃ A ⊆ P.tgt.skeletonSet \ modelCurve, IsPreconnected A ∧ z ∈ A ∧ (A ∩ ((squareMesh delta fresh anchors).pointSet segmentDrawing \ modelCurve)).Nonempty) : IsSourceExtension P.tgt modelCurve (Plane.closedSquare 0 1) ((Q.meshOverlay delta fresh anchors).relabelEdges name hname) ((Q.meshOverlay delta fresh anchors).relabelDrawing name segmentDrawing)

With a dense fresh boundary list, 2-connectivity and the nonempty-fresh requirement are automatic. The mesh-hitting condition is then the only remaining assembly hypothesis.

theorem Schoenflies.TargetSegmentCover.isSourceExtension_relabelledMeshOverlay_of_locallyWider {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) {delta : ℝ} (hdelta : 0 < delta) (hdense : FreshDense fresh delta) (hdelta4 : delta < 4) (hwide : OpenTargetLocallyWiderThan P delta) (anchors : List Plane) (name : Piece → γ) (hname : Set.InjOn name (Q.meshOverlay delta fresh anchors).edgeSet) : IsSourceExtension P.tgt modelCurve (Plane.closedSquare 0 1) ((Q.meshOverlay delta fresh anchors).relabelEdges name hname) ((Q.meshOverlay delta fresh anchors).relabelDrawing name segmentDrawing)

A sufficiently fine mesh gives the target extension from the local-width condition alone: the radial diameter estimate supplies the mesh hits, while density supplies 2-connectivity.

theorem Schoenflies.TargetSegmentCover.exists_scale_isSourceExtension_relabelledMeshOverlay {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) : ∃ (delta : ℝ), 0 < delta ∧ delta < 4 ∧ ∀ (fresh anchors : List Plane) (name : Piece → γ), (∀ z ∈ fresh, z ∈ modelCurve) → FreshDense fresh delta → ∀ (hname : Set.InjOn name (Q.meshOverlay delta fresh anchors).edgeSet), IsSourceExtension P.tgt modelCurve (Plane.closedSquare 0 1) ((Q.meshOverlay delta fresh anchors).relabelEdges name hname) ((Q.meshOverlay delta fresh anchors).relabelDrawing name segmentDrawing)

There is a positive scale below 4 such that every dense anchored mesh at that scale, after fresh injective edge relabelling, is a complete target source extension.

theorem Schoenflies.TargetSegmentCover.exists_meshOverlay_edgeRelabeling {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} [Infinite γ] (Q : TargetSegmentCover P) (delta : ℝ) (fresh anchors : List Plane) : ∃ (name : Piece → γ), Set.InjOn name (Q.meshOverlay delta fresh anchors).edgeSet ∧ ∀ e ∈ (Q.meshOverlay delta fresh anchors).edgeSet, name e ∉ P.str.cells

Fresh cell names for every edge of the combined target overlay, avoiding all names already used by the current generated structure.

theorem Schoenflies.TargetSegmentCover.finite_transfer_toward_source_relabelledMeshOverlay_of_outerCycle {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} [Infinite γ] (Q : TargetSegmentCover P) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (hstrong : ∀ z ∈ fresh, StronglyAccessible (srcDom \ srcOuter) (P.homeo.invFun z)) (havoid : FreshAvoidsTargetNonouterEdges P fresh) (delta : ℝ) (anchors : List Plane) (name : Piece → γ) (hname : Set.InjOn name (Q.meshOverlay delta fresh anchors).edgeSet) (hH : IsSourceExtension P.tgt modelCurve (Plane.closedSquare 0 1) ((Q.meshOverlay delta fresh anchors).relabelEdges name hname) ((Q.meshOverlay delta fresh anchors).relabelDrawing name segmentDrawing)) (hcycle : S₀.OuterEdgesFormCycle) : ∃ (T : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)) (par : γ → γ), IsTargetTransferOf T P ((Q.meshOverlay delta fresh anchors).relabelEdges name hname) ((Q.meshOverlay delta fresh anchors).relabelDrawing name segmentDrawing) par

Reverse finite transfer through the combined target/mesh overlay. Once the overlay is a source extension, strong accessibility of its fresh anchors and avoidance of the finitely many old nonouter target edges discharge all remaining reverse-ear hypotheses.

theorem Schoenflies.TargetSegmentCover.exists_finite_transfer_toward_source_meshOverlay_of_locallyWider {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} [Infinite γ] (Q : TargetSegmentCover P) {fresh : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (hstrong : ∀ z ∈ fresh, StronglyAccessible (srcDom \ srcOuter) (P.homeo.invFun z)) (havoid : FreshAvoidsTargetNonouterEdges P fresh) {delta : ℝ} (hdelta : 0 < delta) (hdense : FreshDense fresh delta) (hdelta4 : delta < 4) (hwide : OpenTargetLocallyWiderThan P delta) (anchors : List Plane) (hcycle : S₀.OuterEdgesFormCycle) : ∃ (name : Piece → γ) (hname : Set.InjOn name (Q.meshOverlay delta fresh anchors).edgeSet) (T : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)) (par : γ → γ), IsTargetTransferOf T P ((Q.meshOverlay delta fresh anchors).relabelEdges name hname) ((Q.meshOverlay delta fresh anchors).relabelDrawing name segmentDrawing) par

At a locally wide scale, the dense clean overlay automatically supplies both the source extension and its reverse finite transfer; fresh abstract edge names are chosen internally.

theorem Schoenflies.TargetSegmentCover.exists_scale_finite_transfer_toward_source_meshOverlay {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} [Infinite γ] (Q : TargetSegmentCover P) (hcycle : S₀.OuterEdgesFormCycle) : ∃ (delta : ℝ), 0 < delta ∧ delta < 4 ∧ ∀ (fresh anchors : List Plane), (∀ z ∈ fresh, z ∈ modelCurve) → (∀ z ∈ fresh, StronglyAccessible (srcDom \ srcOuter) (P.homeo.invFun z)) → FreshAvoidsTargetNonouterEdges P fresh → FreshDense fresh delta → ∃ (name : Piece → γ) (hname : Set.InjOn name (Q.meshOverlay delta fresh anchors).edgeSet) (T : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)) (par : γ → γ), IsTargetTransferOf T P ((Q.meshOverlay delta fresh anchors).relabelEdges name hname) ((Q.meshOverlay delta fresh anchors).relabelDrawing name segmentDrawing) par

Every generated target has one positive scale below 4 at which any dense, accessible, clean fresh list produces the complete reverse finite transfer through the combined overlay.

theorem Schoenflies.TargetSegmentCover.exists_scale_finite_transfer_toward_source_meshOverlay_lt {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} [Infinite γ] (Q : TargetSegmentCover P) (hcycle : S₀.OuterEdgesFormCycle) {bound : ℝ} (hbound : 0 < bound) : ∃ (delta : ℝ), 0 < delta ∧ delta < 4 ∧ delta < bound ∧ ∀ (fresh anchors : List Plane), (∀ z ∈ fresh, z ∈ modelCurve) → (∀ z ∈ fresh, StronglyAccessible (srcDom \ srcOuter) (P.homeo.invFun z)) → FreshAvoidsTargetNonouterEdges P fresh → FreshDense fresh delta → ∃ (name : Piece → γ) (hname : Set.InjOn name (Q.meshOverlay delta fresh anchors).edgeSet) (T : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)) (par : γ → γ), IsTargetTransferOf T P ((Q.meshOverlay delta fresh anchors).relabelEdges name hname) ((Q.meshOverlay delta fresh anchors).relabelDrawing name segmentDrawing) par

The complete reverse-transfer scale may be forced below any prescribed positive bound.