Boundary anchors retained by the quantitative recursion

Every reverse quantitative stage selects a finite metric net of accessible points on the model curve. This module takes their countable union, proves it dense, transports it through the prescribed boundary homeomorphism, and records the finite-stage witness for every transported source anchor.

Blueprint

This discharges lem:anchor-density and constructs the HasAnchorCrosscuts and HasSpokes inputs used in prop:boundary-continuity.

theorem Schoenflies.CellStructure.Realization.IsAdmissible.isStageOn {γ : Type u_1} {C : Set Plane} {S : CellStructure γ} {R : S.Realization} (h : R.IsAdmissible C (C ∪ inside C)) : R.graph.IsStageOn R.drawing C (inside C)

An admissible realization of the closed Jordan domain is exactly a finite stage in the form consumed by the skeleton-crosscut theorem.

theorem Schoenflies.Graph.IsDrawing.exists_nonboundary_incident_of_mem_closure {γ : Type u_1} {C : Set Plane} {G : Graph Plane γ} {drawing : γ → ℝ → Plane} [G.Finite] (h : G.IsDrawing drawing) {c : Plane} (hcV : c ∈ G.vertexSet) (hcC : c ∈ C) (hclosure : c ∈ closure (G.pointSet drawing \ C)) : ∃ (e : γ), G.Inc e c ∧ Graph.Nonboundary drawing C e

A vertex approached by points of the graph off C is incident with an edge not contained in C. A sufficiently small vertex square excludes every other vertex and every nonincident edge.

theorem Schoenflies.Graph.pointSet_traceGraph_eq_interiorPart {γ : Type u_1} {G : Graph Plane γ} {drawing : γ → ℝ → Plane} (h : G.IsDrawing drawing) (D : Set Plane) : (G.traceGraph drawing D).pointSet drawing = G.interiorPart drawing D

The set-level interior part of a finite stage is the point set of the trace subgraph whose support is the open region.

theorem Schoenflies.Graph.IsDrawing.isPolygonal_edgesCover_of_mem {γ : Type u_1} {G : Graph Plane γ} {drawing : γ → ℝ → Plane} (h : G.IsDrawing drawing) {a b : Plane} {W : List γ} (hW : G.IsWalk a W b) (hne : W ≠ []) (hpoly : ∀ e ∈ W, IsPolygonal (Graph.edgeArc drawing e)) : IsPolygonal (Graph.edgesCover drawing W)

A nonempty walk is polygonal when the edge arcs actually used by that walk are polygonal; no condition on unused (and possibly wild outer) edges is needed.

theorem Schoenflies.Graph.IsWalk.exists_lift_map {α : Type u_2} {α' : Type u_3} {β : Type u_4} {G : Graph α β} {f : α → α'} (hf : Set.InjOn f G.vertexSet) {u : α} (hu : u ∈ G.vertexSet) {W : List β} {y : α'} (h : (Graph.map f G).IsWalk (f u) W y) : ∃ (v : α), G.IsWalk u W v ∧ f v = y

A walk in an injectively mapped graph lifts to a walk in the original graph, starting at the prescribed preimage vertex.

theorem Schoenflies.Graph.IsPath.exists_lift_map {α : Type u_2} {α' : Type u_3} {β : Type u_4} {G : Graph α β} {f : α → α'} (hf : Set.InjOn f G.vertexSet) {u : α} (hu : u ∈ G.vertexSet) {W : List β} {y : α'} (h : (Graph.map f G).IsPath (f u) W y) : ∃ (v : α), G.IsPath u W v ∧ f v = y

The corresponding lifting statement for a simple path.

theorem Schoenflies.CellStructure.SkeletonHomeo.image_edgesCover {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} (g : SkeletonHomeo R₁ R₂) {W : List γ} (hW : ∀ e ∈ W, e ∈ S.skel.edgeSet) : g.toFun '' Graph.edgesCover R₁.drawing W = Graph.edgesCover R₂.drawing W

A skeleton homeomorphism carries the union of any finite list of corresponding edges onto the union of the same edge list in the target realization.

theorem Schoenflies.Graph.IsStageOn.exists_crosscut_path {γ : Type u_1} {C : Set Plane} {G : Graph Plane γ} {drawing : γ → ℝ → Plane} [G.Finite] (h : G.IsStageOn drawing C (inside C)) (hC : IsJordanCurve C) {a b : Plane} (hab : a ≠ b) (haC : a ∈ C) (hbC : b ∈ C) (ha : ∃ (e : γ), G.Inc e a ∧ Graph.Nonboundary drawing C e) (hb : ∃ (e : γ), G.Inc e b ∧ Graph.Nonboundary drawing C e) : ∃ (W : List γ), G.IsPath a W b ∧ (∀ e ∈ W, Graph.Nonboundary drawing C e) ∧ IsCrosscut C (Graph.edgesCover drawing W) a b

Strengthened skeleton-crosscut extraction: the crosscut is the carrier of a simple graph path all of whose edges are nonboundary. This edge-list form can be transported to a matched realization edge by edge.

theorem Schoenflies.exists_halfSpoke_tail {N : ℕ} (hN : 2 ≤ N) (z : Plane) {delta : ℝ} (hdelta : 0 < delta) : ∃ A ⊆ halfSpoke N z, IsPreconnected A ∧ A ⊆ Metric.ball z delta ∧ z ∈ closure A

Every radial half-spoke has arbitrarily small connected tails accumulating at its missing outer endpoint.

def Schoenflies.quantitativeFreshTargetSet {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} [Infinite γ] (P₀ : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) (hC : IsSeparating C) (hcycle : S₀.OuterEdgesFormCycle) (q : QuantitativeSchedule C) : Set Plane

All target-boundary points selected as fresh spoke endpoints by some reverse stage.

Equations

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

theorem Schoenflies.quantitativeFreshTargetSet_subset {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} [Infinite γ] (P₀ : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) (hC : IsSeparating C) (hcycle : S₀.OuterEdgesFormCycle) (q : QuantitativeSchedule C) : quantitativeFreshTargetSet P₀ hC hcycle q ⊆ modelCurve

theorem Schoenflies.quantitativeFresh_halfSpoke_subset_targetSkeleton {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} [Infinite γ] (P₀ : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) (hC : IsSeparating C) (hcycle : S₀.OuterEdgesFormCycle) (q : QuantitativeSchedule C) {n : ℕ} {z : Plane} (hz : z ∈ (scheduledQuantitativeSuccessor hC hcycle q n (quantitativeStage P₀ hC hcycle q n)).reverse.overlay.fresh) : halfSpoke (meshCount (scheduledQuantitativeSuccessor hC hcycle q n (quantitativeStage P₀ hC hcycle q n)).reverse.overlay.delta) z ⊆ (quantitativeStage P₀ hC hcycle q (n + 1)).tgt.skeletonSet

The radial half-spoke attached to a fresh target anchor at successor n is retained by the target skeleton of the complete two-sided successor.

theorem Schoenflies.quantitativeFreshTargetSet_dense {γ : Type u_1} {S₀ : CellStructure γ} {C : Set Plane} [Infinite γ] (P₀ : GeneratedPair S₀ C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)) (hC : IsSeparating C) (hcycle : S₀.OuterEdgesFormCycle) (q : QuantitativeSchedule C) : modelCurve ⊆ closure (quantitativeFreshTargetSet P₀ hC hcycle q)

The selected target anchors are dense on the model curve.

noncomputable def Schoenflies.prescribedTargetAnchorSet {C : Set Plane} {u v : Plane → Plane} (hC : IsJordanCurve C) (hu : IsHomeoOn u v C modelCurve) : Set Plane

The target anchor set for the recursion started with the prescribed boundary map.

Equations

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

noncomputable def Schoenflies.prescribedSourceAnchorSet {C : Set Plane} {u v : Plane → Plane} (hC : IsJordanCurve C) (hu : IsHomeoOn u v C modelCurve) : Set Plane

The corresponding source anchors, transported by the prescribed boundary inverse.

Equations

• Schoenflies.prescribedSourceAnchorSet hC hu = v '' Schoenflies.prescribedTargetAnchorSet hC hu

theorem Schoenflies.prescribedTargetAnchorSet_subset {C : Set Plane} {u v : Plane → Plane} (hC : IsJordanCurve C) (hu : IsHomeoOn u v C modelCurve) : prescribedTargetAnchorSet hC hu ⊆ modelCurve

theorem Schoenflies.prescribedTargetAnchorSet_dense {C : Set Plane} {u v : Plane → Plane} (hC : IsJordanCurve C) (hu : IsHomeoOn u v C modelCurve) : modelCurve ⊆ closure (prescribedTargetAnchorSet hC hu)

theorem Schoenflies.prescribedSourceAnchorSet_subset {C : Set Plane} {u v : Plane → Plane} (hC : IsJordanCurve C) (hu : IsHomeoOn u v C modelCurve) : prescribedSourceAnchorSet hC hu ⊆ C

theorem Schoenflies.IsHomeoOn.subset_closure_image_inv {f g : Plane → Plane} {s t A : Set Plane} (h : IsHomeoOn f g s t) (hA : A ⊆ t) (hdense : t ⊆ closure A) : s ⊆ closure (g '' A)

Density pulls back through the inverse side of a relative homeomorphism.

theorem Schoenflies.prescribedSourceAnchorSet_dense {C : Set Plane} {u v : Plane → Plane} (hC : IsJordanCurve C) (hu : IsHomeoOn u v C modelCurve) : C ⊆ closure (prescribedSourceAnchorSet hC hu)

theorem Schoenflies.prescribedJordanStage_homeo_eq_boundary {C : Set Plane} {u v : Plane → Plane} (hC : IsJordanCurve C) (hu : IsHomeoOn u v C modelCurve) (n : ℕ) : Set.EqOn ((prescribedJordanStageSequence hC u v hu).stage n).homeo.toFun u C

Every stage skeleton homeomorphism still agrees with the prescribed boundary map.

theorem Schoenflies.prescribedJordanStage_invFun_eq_boundaryInv {C : Set Plane} {u v : Plane → Plane} (hC : IsJordanCurve C) (hu : IsHomeoOn u v C modelCurve) (n : ℕ) {z : Plane} (hz : z ∈ modelCurve) : ((prescribedJordanStageSequence hC u v hu).stage n).homeo.invFun z = v z

On the model curve, the inverse of every finite-stage skeleton map is the prescribed boundary inverse.

theorem Schoenflies.prescribedJordanStage_succ_src_isAdmissible {C : Set Plane} {u v : Plane → Plane} (hC : IsJordanCurve C) (hu : IsHomeoOn u v C modelCurve) (n : ℕ) : ((prescribedJordanStageSequence hC u v hu).stage (n + 1)).src.IsAdmissible C (C ∪ inside C)

Every noninitial prescribed stage is source-admissible; it is the output of the forward half of the preceding quantitative successor.

theorem Schoenflies.prescribedSourceAnchorSet_stageWitness {C : Set Plane} {u v : Plane → Plane} (hC : IsJordanCurve C) (hu : IsHomeoOn u v C modelCurve) {c : Plane} (hc : c ∈ prescribedSourceAnchorSet hC hu) : ∃ (n : ℕ), ∃ z ∈ (scheduledQuantitativeSuccessor ⋯ outerEdgesFormCycle_initialStructure (denseQuantitativeSchedule ⋯) n ((prescribedJordanStageSequence hC u v hu).stage n)).reverse.overlay.fresh, c = v z ∧ ((prescribedJordanStageSequence hC u v hu).stage n).homeo.invFun z = c

Each transported source anchor comes with the reverse stage at which it was selected and the exact finite-stage source endpoint realizing it.

theorem Schoenflies.prescribedSourceAnchorSet_stageClosure {C : Set Plane} {u v : Plane → Plane} (hC : IsJordanCurve C) (hu : IsHomeoOn u v C modelCurve) {c : Plane} (hc : c ∈ prescribedSourceAnchorSet hC hu) : ∃ (n : ℕ), c ∈ closure (((prescribedJordanStageSequence hC u v hu).stage (n + 1)).src.skeletonSet \ C)

Every selected source anchor is approached by the open nonboundary part of one finite-stage skeleton. This retains precisely the finite combinatorial germ needed to find an incident nonboundary edge after making the anchor a vertex.

theorem Schoenflies.prescribedSourceAnchorSet_hasSpokes {C : Set Plane} {u v : Plane → Plane} (hC : IsJordanCurve C) (hu : IsHomeoOn u v C modelCurve) : HasSpokes C (prescribedSourceAnchorSet hC hu) u (prescribedJordanStageSequence hC u v hu).limitTower.F

The dense prescribed anchor set has the spoke germs required by boundary continuity. A fresh radial target segment is already present at the reverse half-stage; target-skeleton monotonicity retains it through the following forward refinement, and the finite-stage inverse transports an arbitrarily short tail into the Jordan domain.

theorem Schoenflies.prescribedSourceAnchorSet_hasAnchorCrosscuts {C : Set Plane} {u v : Plane → Plane} (hC : IsJordanCurve C) (hu : IsHomeoOn u v C modelCurve) : HasAnchorCrosscuts C (prescribedSourceAnchorSet hC hu) u (prescribedJordanStageSequence hC u v hu).limitTower.F

Any two distinct prescribed anchors are joined by a finite-stage crosscut, and the same abstract edge path in the matched target skeleton is its image. The limit map agrees with that finite skeleton map on the source crosscut.