Selecting a finite dense list of fresh boundary anchors

FreshDense fresh delta is the order-free condition used by the anchored square mesh: every connected subset of the model curve avoiding fresh has diameter at most delta / 2.

A dense set of eligible anchors contains a finite list with this property. For each pair of model-curve points at distance at least delta / 2, two eligible anchors separate the pair. The same anchors separate every nearby pair, because the complementary sides of the associated cut arcs are open. The far-pair set is compact, so finitely many such neighborhoods cover it. Any connected set avoiding all selected anchors must therefore have the required diameter.

Blueprint

• Schoenflies.exists_finite_freshDense_of_dense — a dense eligible subset of the model curve supplies a finite FreshDense list at every positive scale.
• Schoenflies.TargetSegmentCover.MeshOverlayTransferData — the complete output of one reverse overlay-transfer stage, packaged for the stage recursion.
• Schoenflies.TargetSegmentCover.nonempty_meshOverlayTransferData_inside — in the standard closed Jordan domain, separation and the outer-cycle invariant construct that stage data.
• Schoenflies.TargetSegmentCover.MeshOverlayTransferData.diam_targetStar_lt — the transferred target stars have diameter less than twice the selected mesh scale.

theorem Schoenflies.IsJordanCurve.subset_closure_sdiff_finite {C eligible forbidden : Set Plane} (hC : IsJordanCurve C) (heligible : eligible ⊆ C) (hdense : C ⊆ closure eligible) (hforbidden : forbidden.Finite) : C ⊆ closure (eligible \ forbidden)

Removing finitely many forbidden points from a relatively dense subset of a Jordan curve leaves it relatively dense. The proof works in the curve subtype, which is a nontrivial connected T₁ space and therefore has no isolated points.

theorem Schoenflies.exists_finite_freshDense_of_dense {eligible : Set Plane} (heligible : eligible ⊆ modelCurve) (hdense : modelCurve ⊆ closure eligible) {delta : ℝ} (hdelta : 0 < delta) : ∃ (fresh : List Plane), (∀ z ∈ fresh, z ∈ eligible) ∧ FreshDense fresh delta

A dense eligible subset of the model curve contains a finite list which separates every pair of model-curve points at distance more than delta / 2.

def Schoenflies.FreshNet (fresh : List Plane) (delta : ℝ) : Prop

A finite boundary list is a metric net at scale delta. This explicit consequence is retained for the boundary-continuity construction; FreshDense itself is the order-free connected-component estimate needed by the target mesh.

Equations

• Schoenflies.FreshNet fresh delta = ∀ x ∈ Schoenflies.modelCurve, ∃ z ∈ fresh, dist x z < delta

theorem Schoenflies.FreshDense.mono {fresh fresh' : List Plane} {delta : ℝ} (h : FreshDense fresh delta) (hsub : ∀ z ∈ fresh, z ∈ fresh') : FreshDense fresh' delta

theorem Schoenflies.FreshNet.mono {fresh fresh' : List Plane} {delta : ℝ} (h : FreshNet fresh delta) (hsub : ∀ z ∈ fresh, z ∈ fresh') : FreshNet fresh' delta

theorem Schoenflies.exists_finite_freshNet_of_dense {eligible : Set Plane} (hdense : modelCurve ⊆ closure eligible) {delta : ℝ} (hdelta : 0 < delta) : ∃ (fresh : List Plane), (∀ z ∈ fresh, z ∈ eligible) ∧ FreshNet fresh delta

A relatively dense eligible subset of the compact model curve supplies a finite metric net consisting entirely of eligible points.

theorem Schoenflies.exists_finite_freshDenseNet_of_dense {eligible : Set Plane} (heligible : eligible ⊆ modelCurve) (hdense : modelCurve ⊆ closure eligible) {delta : ℝ} (hdelta : 0 < delta) : ∃ (fresh : List Plane), (∀ z ∈ fresh, z ∈ eligible) ∧ FreshDense fresh delta ∧ FreshNet fresh delta

The two finite selections can be combined without losing either property.

Fresh lists for a generated target overlay

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

Strongly accessible points on the source boundary.

Equations

• Schoenflies.TargetSegmentCover.accessibleSourceBoundary _P = {x : Schoenflies.Plane | x ∈ srcOuter ∧ Schoenflies.StronglyAccessible (srcDom \ srcOuter) x}

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

Boundary points whose source-side preimages are strongly accessible.

Equations

• Schoenflies.TargetSegmentCover.accessibleTargetBoundary P = {z : Schoenflies.Plane | z ∈ Schoenflies.modelCurve ∧ Schoenflies.StronglyAccessible (srcDom \ srcOuter) (P.homeo.invFun z)}

theorem Schoenflies.TargetSegmentCover.accessibleTargetBoundary_dense_of_source {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)) (hsource : srcOuter ⊆ closure (accessibleSourceBoundary P)) : modelCurve ⊆ closure (accessibleTargetBoundary P)

Relative density of strongly accessible source-boundary points transports through the current skeleton homeomorphism to relative density on the model curve.

theorem Schoenflies.TargetSegmentCover.accessibleTargetBoundary_dense_of_region {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)) (hsep : IsSeparating srcOuter) (hregion : IsRegionOf srcOuter (srcDom \ srcOuter)) : modelCurve ⊆ closure (accessibleTargetBoundary P)

In the standard generated-pair setting, tangent density on the source region supplies the density hypothesis needed by finite fresh-list selection.

theorem Schoenflies.TargetSegmentCover.accessibleTargetBoundary_dense_inside {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} (P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) (hsep : IsSeparating C) : modelCurve ⊆ closure (accessibleTargetBoundary P)

For the closed Jordan domain used by the stage tower, the required source region is literally inside srcOuter, so accessible target-boundary density follows from separation of the source curve.

theorem Schoenflies.TargetSegmentCover.exists_clean_freshDense_of_accessibleTargetBoundary_dense {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)) (haccessible : modelCurve ⊆ closure (accessibleTargetBoundary P)) {delta : ℝ} (hdelta : 0 < delta) : ∃ (fresh : List Plane), (∀ z ∈ fresh, z ∈ modelCurve) ∧ (∀ z ∈ fresh, StronglyAccessible (srcDom \ srcOuter) (P.homeo.invFun z)) ∧ FreshAvoidsTargetNonouterEdges P fresh ∧ FreshDense fresh delta ∧ FreshNet fresh delta

If accessible target-boundary points are relatively dense, then at every positive scale there is a finite dense list of accessible points avoiding all old target vertices and hence all old nonouter target-edge carriers.

theorem Schoenflies.TargetSegmentCover.exists_finite_transfer_toward_source_meshOverlay_of_accessibleBoundary_dense {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} [Infinite γ] (Q : TargetSegmentCover P) (haccessible : modelCurve ⊆ closure (accessibleTargetBoundary P)) (hcycle : S₀.OuterEdgesFormCycle) (anchors : List Plane) : ∃ (delta : ℝ) (fresh : List Plane), 0 < delta ∧ delta < 4 ∧ (∀ z ∈ fresh, z ∈ modelCurve) ∧ (∀ z ∈ fresh, StronglyAccessible (srcDom \ srcOuter) (P.homeo.invFun z)) ∧ FreshAvoidsTargetNonouterEdges P fresh ∧ FreshDense fresh delta ∧ FreshNet 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

Dense accessible boundary points now suffice for the full overlay reverse transfer. The mesh scale, finite clean fresh list, fresh abstract edge names, and transferred generated pair are all selected internally.

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

The complete finite data selected by one reverse overlay-transfer stage. Packaging the dependent edge relabelling and its transferred generated pair together makes this construction directly usable by the stage recursion.

• delta : ℝ

  The positive mesh scale selected for this target.

• fresh : List Plane

  The finite accessible boundary-anchor list.

• delta_pos : 0 < self.delta
• delta_lt_four : self.delta < 4
• fresh_mem (z : Plane) : z ∈ self.fresh → z ∈ modelCurve
• fresh_accessible (z : Plane) : z ∈ self.fresh → StronglyAccessible (srcDom \ srcOuter) (P.homeo.invFun z)
• fresh_avoids : FreshAvoidsTargetNonouterEdges P self.fresh
• fresh_dense : FreshDense self.fresh self.delta
• fresh_net : FreshNet self.fresh self.delta

  The selected points also form an explicit metric net on the target boundary.

• name : Piece → γ

  Fresh abstract names for all edges of the finite overlay.

• name_inj : Set.InjOn self.name (Q.meshOverlay self.delta self.fresh anchors).edgeSet
• pair : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)

  The generated pair after reverse transfer.

• parent : γ → γ

  The abstract parent map of the transfer.

• transfer : IsTargetTransferOf self.pair P ((Q.meshOverlay self.delta self.fresh anchors).relabelEdges self.name ⋯) ((Q.meshOverlay self.delta self.fresh anchors).relabelDrawing self.name segmentDrawing) self.parent

theorem Schoenflies.TargetSegmentCover.nonempty_meshOverlayTransferData_of_accessibleBoundary_dense {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} [Infinite γ] (Q : TargetSegmentCover P) (haccessible : modelCurve ⊆ closure (accessibleTargetBoundary P)) (hcycle : S₀.OuterEdgesFormCycle) (anchors : List Plane) : Nonempty (Q.MeshOverlayTransferData anchors)

Dense accessible target-boundary points construct the packaged data for one complete reverse overlay-transfer stage.

theorem Schoenflies.TargetSegmentCover.nonempty_meshOverlayTransferData_inside {γ : Type u_1} {S₀ : CellStructure γ} [Infinite γ] {C : Set Plane} {P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) (hsep : IsSeparating C) (hcycle : S₀.OuterEdgesFormCycle) (anchors : List Plane) : Nonempty (Q.MeshOverlayTransferData anchors)

Reverse overlay-transfer stage for a closed Jordan domain. Tangent density supplies the accessible anchors, finite deletion avoids the old target vertices, and compactness selects a finite FreshDense list at the internally chosen mesh scale.

theorem Schoenflies.TargetSegmentCover.exists_meshOverlayTransferData_lt_of_accessibleBoundary_dense {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} [Infinite γ] (Q : TargetSegmentCover P) (haccessible : modelCurve ⊆ closure (accessibleTargetBoundary P)) (hcycle : S₀.OuterEdgesFormCycle) (anchors : List Plane) {bound : ℝ} (hbound : 0 < bound) : ∃ (w : Q.MeshOverlayTransferData anchors), w.delta < bound

The packaged reverse-transfer data can be selected below any positive prescribed scale.

theorem Schoenflies.TargetSegmentCover.exists_meshOverlayTransferData_lt_inside {γ : Type u_1} {S₀ : CellStructure γ} [Infinite γ] {C : Set Plane} {P : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)} (Q : TargetSegmentCover P) (hsep : IsSeparating C) (hcycle : S₀.OuterEdgesFormCycle) (anchors : List Plane) {bound : ℝ} (hbound : 0 < bound) : ∃ (w : Q.MeshOverlayTransferData anchors), w.delta < bound

In the standard closed Jordan domain, a reverse-transfer stage exists below every positive prescribed scale.

theorem Schoenflies.TargetSegmentCover.MeshOverlayTransferData.diam_closure_targetFace_lt {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} {Q : TargetSegmentCover P} {anchors : List Plane} (w : Q.MeshOverlayTransferData anchors) {F : γ} (hF : F ∈ w.pair.str.faces) : Metric.diam (closure (w.pair.tgt.cell F)) < w.delta

Every target face created by the reverse overlay transfer has diameter below the selected mesh scale. The target cell is connected and misses the new skeleton, hence lies in one bounded face of the contained square mesh; squareMesh_face_small supplies the bound.

theorem Schoenflies.TargetSegmentCover.MeshOverlayTransferData.diam_targetStar_lt {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom modelCurve (Plane.closedSquare 0 1)} {Q : TargetSegmentCover P} {anchors : List Plane} (w : Q.MeshOverlayTransferData anchors) {σ : γ} (hσ : σ ∈ w.pair.str.cells) : Metric.diam (w.pair.tgt.star σ) < 2 * w.delta

Consequently every closed target star has diameter less than twice the selected scale.