Finite transfer, direction (b): toward the Jordan domain

Direction (b) starts with an extension of the target realization and reproduces it on the source side. This module begins its construction with the target analogue of the common subdivision from direction (a). The graph-theoretic extension assumptions are exactly Schoenflies.IsSourceExtension, applied to P.tgt: only the side on which the realization lives changes.

The trace of the target extension supported on the old target skeleton is 2-connected. Its finitely many vertices are inserted by GeneratedPair.exists_subdivideTargetSetData; each target point is transported backwards through the skeleton homeomorphism, and the resulting source parameter is then carried forward by SubdivData.realizeHomeo. Thus the same subdivision is made on both sides and both refinement maps share one parent map.

The reverse ear bookkeeping is also completed here. The ambient target path is injectively renamed, realized as a target crosscut, and then matched to a polygonal source crosscut by reversing EarHomeo. Off the wild curve, endpoint accessibility is derived from polygonal-side accessibility. At a fresh anchor, this module constructs the compact carrier of closed nonboundary edges and discharges compactness, cell absorption, and coverage before applying Schoenflies.polyAccessible_of_stronglyAccessible_in. TargetBoundaryAnchored and the compatibility of the evolving skeleton map now supply strong accessibility automatically. Consequently the only remaining input is TargetEarFreshCombinatorics: the prescribed ear order must say that a wild-boundary endpoint is absent from the current nonboundary carrier and incident with one unique current source face.

Blueprint

• Schoenflies.IsTargetPartialTransferOf, Schoenflies.TargetCommonSubdivision — the target-to-source analogues of the direction-(a) transfer interfaces.
• Schoenflies.targetCommonSubdivision — step 1 of thm:finite-transfer(b).
• Schoenflies.TargetEarStepData, Schoenflies.exists_targetSideEarStepData — the complete target-path relabelling and split data for one reverse ear.
• Schoenflies.TargetEarEndpointAccessibility, Schoenflies.targetEarStep_of_endpointAccessibility — the reverse ear construction reduced to its exact source-side geometric invariant.
• Schoenflies.GeneratedPair.sourceNonboundaryGraph, Schoenflies.GeneratedPair.source_polyAccessible_of_fresh — the compact source carrier and the fresh-anchor accessibility theorem with all cellulation hypotheses discharged.
• Schoenflies.TargetBoundaryAnchored, Schoenflies.TargetEarFreshCombinatorics, Schoenflies.targetEarFreshInvariant_of_boundaryAnchored — the fixed anchor geometry split cleanly from the remaining prescribed-ear combinatorics.
• Schoenflies.targetTransferOfEars, Schoenflies.finite_transfer_toward_source_of_freshInvariant — the relative-ear induction and direction-(b) theorem assuming only that combinatorial invariant.

structure Schoenflies.IsTargetPartialTransferOf {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (T P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (B : Graph Plane γ) (Hdraw : γ → ℝ → Plane) (par : γ → γ) : Prop

An intermediate target-to-source transfer: the target realization occupies the current subgraph of the target extension, while both sides refine the original pair along one map.

• refines_src : T.src.Refines P.src par

  The new source realization refines the original source realization.

• refines_tgt : T.tgt.Refines P.tgt par

  The new target realization refines the original target realization along the same map.

• sourceSkeletonSet_subset : P.src.skeletonSet ⊆ T.src.skeletonSet

  The evolving source skeleton contains the original source skeleton.

• homeo_eqOn : Set.EqOn T.homeo.toFun P.homeo.toFun P.src.skeletonSet

  On the original source skeleton, the evolving skeleton map is still the original map.

• skeletonSet_eq : T.tgt.skeletonSet = B.pointSet Hdraw

  The new target skeleton occupies exactly the current target subgraph.

• vertexSet_subset : B.vertexSet ⊆ T.tgt.graph.vertexSet

  Every current target-graph vertex is a 0-cell of the new pair.

theorem Schoenflies.IsTargetPartialTransferOf.targetSkeletonSet_subset {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {T P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {B : Graph Plane γ} {Hdraw : γ → ℝ → Plane} {par : γ → γ} (hT : IsTargetPartialTransferOf T P B Hdraw par) : P.tgt.skeletonSet ⊆ T.tgt.skeletonSet

The evolving target skeleton contains the original target skeleton. This is transported from the corresponding source inclusion through the two compatible skeleton homeomorphisms.

theorem Schoenflies.IsTargetPartialTransferOf.source_pos_eq_invFun_target_pos {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {T P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {B : Graph Plane γ} {Hdraw : γ → ℝ → Plane} {par : γ → γ} (hT : IsTargetPartialTransferOf T P B Hdraw par) {v : γ} (hv : v ∈ T.str.skel.vertexSet) (hvP : T.tgt.pos v ∈ P.tgt.skeletonSet) : T.src.pos v = P.homeo.invFun (T.tgt.pos v)

A current abstract vertex lying over the original target skeleton has the original source preimage. This is the pointwise compatibility needed to recognize prescribed source anchors after any number of reverse-ear insertions.

structure Schoenflies.IsTargetTransferOf {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (T P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (H : Graph Plane γ) (Hdraw : γ → ℝ → Plane) (par : γ → γ) extends Schoenflies.IsTargetPartialTransferOf T P H Hdraw par : Prop

The final conclusion of direction (b): a target extension reproduced by an admissible matched pair on both sides.

• refines_src : T.src.Refines P.src par
• refines_tgt : T.tgt.Refines P.tgt par
• sourceSkeletonSet_subset : P.src.skeletonSet ⊆ T.src.skeletonSet
• homeo_eqOn : Set.EqOn T.homeo.toFun P.homeo.toFun P.src.skeletonSet
• skeletonSet_eq : T.tgt.skeletonSet = H.pointSet Hdraw
• vertexSet_subset : H.vertexSet ⊆ T.tgt.graph.vertexSet
• src_isAdmissible : T.src.IsAdmissible srcOuter srcDom

  The transferred source realization is admissible.

• tgt_isAdmissible : T.tgt.IsAdmissible tgtOuter tgtDom

  The transferred target realization is admissible.

def Schoenflies.TargetCommonSubdivision {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (H : Graph Plane γ) (Hdraw : γ → ℝ → Plane) : Prop

Step 1 of direction (b), as the interface consumed by its relative-ear induction.

Equations

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

def Schoenflies.TargetEarStep {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (H : Graph Plane γ) (Hdraw : γ → ℝ → Plane) : Prop

One target ear insertion, expressed as the step consumed by relative-ear induction.

Equations

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

structure Schoenflies.TargetEarStepData {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (B H : Graph Plane γ) (Hdraw : γ → ℝ → Plane) (a : Plane) (D : List γ) : Type u_1

Complete constructor data for adjoining one target ear to a partial reverse transfer.

• splitData : T.str.SplitData

  The common abstract face split.

• srcPos : γ → Plane

  The two realizations of its new ear.

• srcDraw : γ → ℝ → Plane

  Parametrizations of the matching source ear.

• tgtPos : γ → Plane

  Positions of the target ear vertices.

• tgtDraw : γ → ℝ → Plane

  Parametrizations of the target ear edges.

• srcCrosscut : self.splitData.EarCrosscut T.src self.srcPos self.srcDraw

  Each realized ear is a crosscut of the corresponding old face.

• tgtCrosscut : self.splitData.EarCrosscut T.tgt self.tgtPos self.tgtDraw
• earHomeo : self.splitData.EarHomeo self.srcPos self.srcDraw self.tgtPos self.tgtDraw

  The source-to-target matching consumed by GeneratedPair.split.

• srcEdgePolygonal ⦃e : γ⦄ : e ∈ self.splitData.ear.edgeSet → IsPolygonal (Graph.edgeArc self.srcDraw e)

  Both realized ears have polygonal edges.

• tgtEdgePolygonal ⦃e : γ⦄ : e ∈ self.splitData.ear.edgeSet → IsPolygonal (Graph.edgeArc self.tgtDraw e)
• tgtEarSet_eq : self.splitData.earSet self.tgtPos self.tgtDraw = Graph.edgesCover Hdraw D

  The target ear realizes exactly the ambient target path.

• vertexSet_subset : (B.union (H.pathGraphOf a D)).vertexSet ⊆ (CellStructure.SplitData.realize T.tgt self.splitData self.tgtPos self.tgtDraw ⋯).graph.vertexSet

  All vertices of the enlarged target graph occur in the split realization.

noncomputable def Schoenflies.TargetEarStepData.pair {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {B H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} {a : Plane} {D : List γ} (w : TargetEarStepData T B H Hdraw a D) : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom

Assemble the generated pair exposed by one reverse-ear construction.

Equations

• w.pair = T.split ⋯ w.splitData w.srcPos w.srcDraw w.tgtPos w.tgtDraw ⋯ ⋯ w.earHomeo ⋯ ⋯

@[simp]

theorem Schoenflies.TargetEarStepData.pair_src {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {B H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} {a : Plane} {D : List γ} (w : TargetEarStepData T B H Hdraw a D) : w.pair.src = CellStructure.SplitData.realize T.src w.splitData w.srcPos w.srcDraw ⋯

@[simp]

theorem Schoenflies.TargetEarStepData.pair_tgt {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {B H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} {a : Plane} {D : List γ} (w : TargetEarStepData T B H Hdraw a D) : w.pair.tgt = CellStructure.SplitData.realize T.tgt w.splitData w.tgtPos w.tgtDraw ⋯

theorem Schoenflies.TargetEarStepData.isTargetPartialTransferOf_pair {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {B H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} {a : Plane} {D : List γ} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {b : Plane} {par : γ → γ} (w : TargetEarStepData T B H Hdraw a D) (hdraw : H.IsDrawing Hdraw) (hpath : H.IsPath a D b) (hab : a ≠ b) (hT : IsTargetPartialTransferOf T P B Hdraw par) : IsTargetPartialTransferOf w.pair P (B.union (H.pathGraphOf a D)) Hdraw (par ∘ w.splitData.parent)

The assembled pair realizes the enlarged target subgraph and refines the original pair.

def Schoenflies.TargetEarStepConstruction {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (H : Graph Plane γ) (Hdraw : γ → ℝ → Plane) (_hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) : Prop

The nontrivial reverse-ear constructor, before the already-present-edge branch is folded back in.

Equations

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

theorem Schoenflies.targetEarStep_of_data {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (hbuild : TargetEarStepConstruction P H Hdraw hH) : TargetEarStep P H Hdraw

Fold the explicit nontrivial reverse-ear constructor into the total TargetEarStep interface.

Locating and realizing the target half of a reverse ear

theorem Schoenflies.exists_target_face_of_ear {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {B H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} {a b : Plane} {D : List γ} {par : γ → γ} (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (hBH : B ≤ H) (hpath : H.IsPath a D b) (hab : a ≠ b) (haB : a ∈ B.vertexSet) (hbB : b ∈ B.vertexSet) (hint : ∀ y ∈ H.walkVertices a D, y ≠ a → y ≠ b → y ∉ B.vertexSet) (hnew : ∀ g ∈ D, g ∉ B.edgeSet) (hT : IsTargetPartialTransferOf T P B Hdraw par) : ∃ (u : γ) (v : γ) (F : γ), u ∈ T.str.skel.vertexSet ∧ v ∈ T.str.skel.vertexSet ∧ u ≠ v ∧ T.tgt.pos u = a ∧ T.tgt.pos v = b ∧ F ∈ T.str.faces ∧ Graph.edgesCover Hdraw D \ {a, b} ⊆ T.tgt.cell F ∧ T.str.sub u F ∧ T.str.sub v F

A nontrivial target ear lies in one current target face and determines its two abstract endpoint vertices.

theorem Schoenflies.target_ear_edge_not_outer {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} {a b : Plane} {D : List γ} {F : γ} (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (hpath : H.IsPath a D b) (hF : F ∈ T.str.faces) (hinside : Graph.edgesCover Hdraw D \ {a, b} ⊆ T.tgt.cell F) (e : γ) : e ∈ D → ¬Graph.edgeArc Hdraw e ⊆ tgtOuter

No edge of a genuine target ear is contained in the outer curve. Such an edge would lie simultaneously in the old target skeleton and in the open current face.

theorem Schoenflies.target_ear_edge_polygonal {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} {a b : Plane} {D : List γ} {F : γ} (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (hpath : H.IsPath a D b) (hF : F ∈ T.str.faces) (hinside : Graph.edgesCover Hdraw D \ {a, b} ⊆ T.tgt.cell F) (e : γ) : e ∈ D → IsPolygonal (Graph.edgeArc Hdraw e)

Every edge of a genuine target ear is polygonal.

def Schoenflies.TargetBoundaryAnchored {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {β : Type u_2} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (H : Graph Plane β) (Hdraw : β → ℝ → Plane) : Prop

Every boundary endpoint of a nonouter ambient target edge comes from a strongly accessible source anchor. The stage construction will discharge this from the fresh-point list of its anchored square mesh.

Equations

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

def Schoenflies.NewTargetBoundaryAnchored {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {β : Type u_2} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (base : Set Plane) (H : Graph Plane β) (Hdraw : β → ℝ → Plane) : Prop

The relative anchoring condition used by reverse ear insertion. Only genuinely new ambient edges need to end at prescribed strongly accessible anchors; edges already covering the original target skeleton are irrelevant to the next ear.

Equations

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

theorem Schoenflies.TargetBoundaryAnchored.new {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {β : Type u_2} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {H : Graph Plane β} {Hdraw : β → ℝ → Plane} (h : TargetBoundaryAnchored P H Hdraw) (base : Set Plane) : NewTargetBoundaryAnchored P base H Hdraw

Anchoring every nonouter boundary edge implies the relative new-edge condition.

def Schoenflies.NonouterIncidenceUniqueAtBoundary {β : Type u_2} (H : Graph Plane β) (Hdraw : β → ℝ → Plane) (outer : Set Plane) : Prop

At a point of the distinguished boundary, there is at most one incident ambient edge not contained in that boundary. The ambient edge-name type is deliberately independent of the cell-name type.

Equations

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

def Schoenflies.NoNewNonouterIncidenceAtBoundary {β : Type u_2} (base : Set Plane) (H : Graph Plane β) (Hdraw : β → ℝ → Plane) (outer : Set Plane) : Prop

The relative boundary-incidence condition actually used by reverse ear insertion. A new nonouter ambient edge cannot meet, at the distinguished boundary, a nonouter edge already in the current trace. Unlike NonouterIncidenceUniqueAtBoundary, this permits several old nonouter edges at an old boundary vertex, which is essential for target-mesh overlays.

Equations

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

theorem Schoenflies.NonouterIncidenceUniqueAtBoundary.noNew {β : Type u_2} {H : Graph Plane β} {Hdraw : β → ℝ → Plane} {outer : Set Plane} (h : NonouterIncidenceUniqueAtBoundary H Hdraw outer) (base : Set Plane) : NoNewNonouterIncidenceAtBoundary base H Hdraw outer

Global uniqueness implies the weaker relative no-new-incidence condition.

theorem Schoenflies.edge_mem_of_edgeArc_subset_pointSet {β : Type u_2} {G B : Graph Plane β} {drawing : β → ℝ → Plane} (hdraw : G.IsDrawing drawing) (hBG : B ≤ G) {e : β} (he : e ∈ G.edgeSet) (hsub : Graph.edgeArc drawing e ⊆ B.pointSet drawing) : e ∈ B.edgeSet

An edge of a plane graph whose whole carrier is already covered by a subgraph is itself an edge of that subgraph. An interior point of the arc cannot be a subgraph vertex, nor lie on a different subgraph edge, by the drawing intersection axioms.

theorem Schoenflies.eq_of_edgeArc_subset {β : Type u_2} {G : Graph Plane β} {drawing : β → ℝ → Plane} (hdraw : G.IsDrawing drawing) {e f : β} (he : e ∈ G.edgeSet) (hf : f ∈ G.edgeSet) (hsub : Graph.edgeArc drawing e ⊆ Graph.edgeArc drawing f) : e = f

In a plane drawing, an edge carrier cannot be contained in the carrier of a distinct edge.

theorem Schoenflies.TargetBoundaryAnchored.relabelEdges {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {β : Type u_2} {δ : Type u_3} [Nonempty β] {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {H : Graph Plane β} {Hdraw : β → ℝ → Plane} {f : β → δ} (h : TargetBoundaryAnchored P H Hdraw) (hf : Set.InjOn f H.edgeSet) : TargetBoundaryAnchored P (H.relabelEdges f hf) (H.relabelDrawing f Hdraw)

Boundary anchoring is geometric, hence survives an injective change of the ambient edge names.

theorem Schoenflies.NonouterIncidenceUniqueAtBoundary.relabelEdges {β : Type u_2} {δ : Type u_3} [Nonempty β] {H : Graph Plane β} {Hdraw : β → ℝ → Plane} {outer : Set Plane} {f : β → δ} (h : NonouterIncidenceUniqueAtBoundary H Hdraw outer) (hf : Set.InjOn f H.edgeSet) : NonouterIncidenceUniqueAtBoundary (H.relabelEdges f hf) (H.relabelDrawing f Hdraw) outer

Uniqueness of the nonouter boundary edge is likewise invariant under injective edge relabelling.

structure Schoenflies.TargetSideEarStepData {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (B H : Graph Plane γ) (Hdraw : γ → ℝ → Plane) (a b : Plane) (D : List γ) : Type u_1

The one-sided constructor data obtained by realizing the ambient target path.

• splitData : T.str.SplitData

  Abstract split realizing the target ear.

• tgtPos : γ → Plane

  Positions of the new target vertices.

• tgtDraw : γ → ℝ → Plane

  Parametrizations of the new target edges.

• tgtCrosscut : self.splitData.EarCrosscut T.tgt self.tgtPos self.tgtDraw
• tgtEdgePolygonal ⦃e : γ⦄ : e ∈ self.splitData.ear.edgeSet → IsPolygonal (Graph.edgeArc self.tgtDraw e)
• target_pos_source : T.tgt.pos self.splitData.source = a

  The two old abstract endpoints retain the orientation of the ambient target path.

• target_pos_target : T.tgt.pos self.splitData.target = b
• tgtEarSet_eq : self.splitData.earSet self.tgtPos self.tgtDraw = Graph.edgesCover Hdraw D
• vertexSet_subset : (B.union (H.pathGraphOf a D)).vertexSet ⊆ (CellStructure.SplitData.realize T.tgt self.splitData self.tgtPos self.tgtDraw ⋯).graph.vertexSet

theorem Schoenflies.exists_targetSideEarStepData {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} [Infinite γ] (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (H : Graph Plane γ) (Hdraw : γ → ℝ → Plane) (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (B : Graph Plane γ) (a b : Plane) (D : List γ) : B.IsTwoConnected → B ≤ H → H.IsPath a D b → a ≠ b → a ∈ B.vertexSet → b ∈ B.vertexSet → (∀ y ∈ H.walkVertices a D, y ≠ a → y ≠ b → y ∉ B.vertexSet) → (∀ g ∈ D, g ∉ B.edgeSet) → ∀ (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (par : γ → γ), IsTargetPartialTransferOf T P B Hdraw par → Nonempty (TargetSideEarStepData T B H Hdraw a b D)

Injectively rename a nontrivial ambient target ear with fresh abstract cells and realize it as a crosscut of the target face that contains its open arc.

theorem Schoenflies.GeneratedPair.target_pos_mem_outer_of_source_pos_mem_outer {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) {v : γ} (hv : v ∈ T.str.skel.vertexSet) (hx : T.src.pos v ∈ srcOuter) : T.tgt.pos v ∈ tgtOuter

The skeleton homeomorphism sends an abstract vertex on the source outer curve to the corresponding abstract vertex on the target outer curve.

theorem Schoenflies.targetEarEndpointStronglyAccessible_of_newBoundaryAnchored {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {B H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} {a b : Plane} {D : List γ} {par : γ → γ} (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (hanchor : NewTargetBoundaryAnchored P P.tgt.skeletonSet H Hdraw) (hBH : B ≤ H) (hnew : ∀ g ∈ D, g ∉ B.edgeSet) (hpath : H.IsPath a D b) (hab : a ≠ b) (hT : IsTargetPartialTransferOf T P B Hdraw par) (w : TargetSideEarStepData T B H Hdraw a b D) : (T.src.pos w.splitData.source ∈ srcOuter → StronglyAccessible (srcDom \ srcOuter) (T.src.pos w.splitData.source)) ∧ (T.src.pos w.splitData.target ∈ srcOuter → StronglyAccessible (srcDom \ srcOuter) (T.src.pos w.splitData.target))

The relative anchored-boundary condition supplies the strong-accessibility half of readiness at both outer endpoints of a nontrivial target ear. Compatibility of the evolving skeleton map with the original one identifies those endpoints with the original inverse images.

The exact geometric obligation on the source side

def Schoenflies.CellStructure.OuterOnlyAt {γ : Type u_1} (S : CellStructure γ) (v : γ) : Prop

An abstract skeleton vertex is outer-only when every current edge incident with it belongs to the distinguished outer graph.

Equations

• S.OuterOnlyAt v = ∀ {e : γ}, S.skel.Inc e v → e ∈ S.outerGraph.edgeSet

def Schoenflies.CellStructure.OuterIncidenceAtMostTwo {γ : Type u_1} (S : CellStructure γ) (v : γ) : Prop

At most two distinct outer edges are incident with the vertex. This is the exact local consequence of "the distinguished outer graph is a cycle" used by reverse transfer.

Equations

• S.OuterIncidenceAtMostTwo v = ∀ ⦃e f g : γ⦄, S.outerGraph.Inc e v → S.outerGraph.Inc f v → S.outerGraph.Inc g v → e = f ∨ e = g ∨ f = g

def Schoenflies.CellStructure.OuterIncidenceAtMostTwoEverywhere {γ : Type u_1} (S : CellStructure γ) : Prop

The distinguished outer graph is locally at most two-branched at every vertex.

Equations

• S.OuterIncidenceAtMostTwoEverywhere = ∀ (v : γ), S.OuterIncidenceAtMostTwo v

def Schoenflies.CellStructure.OuterEdgesFormCycle {γ : Type u_1} (S : CellStructure γ) : Prop

The edge set of the distinguished outer graph is exactly one simple cycle. Isolated vertices are intentionally irrelevant: reverse transfer only reads edge incidence.

Equations

• S.OuterEdgesFormCycle = ∃ (e : γ) (u : γ) (v : γ) (D : List γ), S.outerGraph.IsCycleThrough e u v D ∧ S.outerGraph.edgeSet = {f : γ | f ∈ e :: D}

theorem Schoenflies.CellStructure.OuterEdgesFormCycle.outerIncidenceAtMostTwoEverywhere {γ : Type u_1} {S : CellStructure γ} (h : S.OuterEdgesFormCycle) : S.OuterIncidenceAtMostTwoEverywhere

A graph whose outer edges form one simple cycle is locally at most two-branched. Rotate the cycle to one incident edge; every other edge at that endpoint lies on the complementary simple path, which has only one incident edge at either end.

theorem Schoenflies.CellStructure.SubdivData.exists_substWalk_of_isWalk {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) {u v : γ} {W : List γ} (hW : S.skel.IsWalk u W v) : ∃ (W' : List γ), d.SubstWalk u W W'

Every abstract walk admits the orientation-aware edge substitution prescribed by a subdivision.

theorem Schoenflies.CellStructure.SubdivData.SubstWalk.newEdges_mem_output_of_mem_input {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} {u : γ} {W W' : List γ} (hsub : d.SubstWalk u W W') (he : d.edge ∈ W) : d.newEdge₁ ∈ W' ∧ d.newEdge₂ ∈ W'

If the subdivided edge occurs in the input, both replacement edges occur in the output.

theorem Schoenflies.CellStructure.SubdivData.SubstWalk.mem_output_iff_of_mem_input {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} {u x : γ} {W W' : List γ} (hsub : d.SubstWalk u W W') (he : d.edge ∈ W) : x ∈ W' ↔ x = d.newEdge₁ ∨ x = d.newEdge₂ ∨ x ∈ W ∧ x ≠ d.edge

With the subdivided edge present, the output edge names are exactly the two replacements and the surviving input names.

theorem Schoenflies.CellStructure.SubdivData.outerEdgesFormCycle {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) (hcycle : S.OuterEdgesFormCycle) : (S.subdivideEdge d).OuterEdgesFormCycle

Edge subdivision preserves the fact that the distinguished outer edges form one simple cycle. When the subdivided edge is outer, substitute it in the closed cycle walk and pull the resulting cycle down from the new skeleton to the new outer graph.

theorem Schoenflies.CellStructure.SplitData.outerEdgesFormCycle {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) (hcycle : S.OuterEdgesFormCycle) : (S.splitFace d).OuterEdgesFormCycle

Splitting a face leaves the distinguished outer graph unchanged.

theorem Schoenflies.GeneratedStructure.outerEdgesFormCycle {γ : Type u_1} {S₀ S : CellStructure γ} (h : GeneratedStructure S₀ S) (h₀ : S₀.OuterEdgesFormCycle) : S.OuterEdgesFormCycle

Every generated structure keeps one simple cycle as its distinguished outer edge set.

theorem Schoenflies.GeneratedStructure.outerIncidenceAtMostTwoEverywhere {γ : Type u_1} {S₀ S : CellStructure γ} (h : GeneratedStructure S₀ S) (h₀ : S₀.OuterEdgesFormCycle) : S.OuterIncidenceAtMostTwoEverywhere

The local two-branch condition needed by square-mesh reverse transfer is therefore a generated-structure invariant as soon as the base outer edges form a simple cycle.

theorem Schoenflies.CellStructure.FaceCycle.exists_distinct_incident_edges {γ : Type u_1} {S : CellStructure γ} {F v : γ} (c : S.FaceCycle F) (hloopless : ∀ ⦃e x y : γ⦄, S.skel.IsLink e x y → x ≠ y) (hv : v ∈ S.skel.vertexSet) (hvF : S.sub v F) : ∃ (e : γ) (f : γ), e ≠ f ∧ e ∈ c.edge :: c.walk ∧ f ∈ c.edge :: c.walk ∧ S.skel.Inc e v ∧ S.skel.Inc f v

A vertex on a nonloop simple cycle has two distinct incident cycle edges. The face-cycle application obtains nonloopness from either geometric realization.

theorem Schoenflies.IsTargetPartialTransferOf.exists_ambient_nonouter_incident {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {B : Graph Plane γ} {Hdraw : γ → ℝ → Plane} {par : γ → γ} [B.Finite] (hT : IsTargetPartialTransferOf T P B Hdraw par) (hBdraw : B.IsDrawing Hdraw) {v e : γ} (hvB : T.tgt.pos v ∈ B.vertexSet) (hvOuter : T.tgt.pos v ∈ tgtOuter) (hinc : T.str.skel.Inc e v) (heOuter : e ∉ T.str.outerGraph.edgeSet) : ∃ f ∈ B.edgeSet, B.Inc f (T.tgt.pos v) ∧ ¬Graph.edgeArc Hdraw f ⊆ tgtOuter

A nonouter edge of the evolving abstract skeleton incident at a current ambient vertex produces a nonouter edge of the ambient graph incident at the same geometric point. No edge labels need to agree: a sufficiently small vertex square meets only ambient edges incident at that vertex, while the open cell of the abstract edge accumulates at its endpoint.

theorem Schoenflies.targetEarEndpointsOuterOnly_of_noNewNonouterIncidence {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (hnoNew : NoNewNonouterIncidenceAtBoundary P.tgt.skeletonSet H Hdraw tgtOuter) {B : Graph Plane γ} {a b : Plane} {D : List γ} {par : γ → γ} (hBH : B ≤ H) (hpath : H.IsPath a D b) (hab : a ≠ b) (haB : a ∈ B.vertexSet) (hbB : b ∈ B.vertexSet) (hnew : ∀ g ∈ D, g ∉ B.edgeSet) {T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} (hT : IsTargetPartialTransferOf T P B Hdraw par) (w : TargetSideEarStepData T B H Hdraw a b D) : (T.src.pos w.splitData.source ∈ srcOuter → T.str.OuterOnlyAt w.splitData.source) ∧ (T.src.pos w.splitData.target ∈ srcOuter → T.str.OuterOnlyAt w.splitData.target)

If no new nonouter ambient edge can coexist at the boundary with a nonouter edge of the current trace, then both boundary endpoints of the next reverse ear are outer-only in the current abstract skeleton. Any current nonouter abstract edge would reflect to just such a current ambient edge.

theorem Schoenflies.targetEarEndpointsOuterOnly_of_nonouterIncidenceUnique {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (hunique : NonouterIncidenceUniqueAtBoundary H Hdraw tgtOuter) {B : Graph Plane γ} {a b : Plane} {D : List γ} {par : γ → γ} (hBH : B ≤ H) (hpath : H.IsPath a D b) (hab : a ≠ b) (haB : a ∈ B.vertexSet) (hbB : b ∈ B.vertexSet) (hnew : ∀ g ∈ D, g ∉ B.edgeSet) {T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} (hT : IsTargetPartialTransferOf T P B Hdraw par) (w : TargetSideEarStepData T B H Hdraw a b D) : (T.src.pos w.splitData.source ∈ srcOuter → T.str.OuterOnlyAt w.splitData.source) ∧ (T.src.pos w.splitData.target ∈ srcOuter → T.str.OuterOnlyAt w.splitData.target)

Global uniqueness of the nonouter ambient edge is a convenient sufficient condition for the relative boundary-incidence hypothesis used above.

theorem Schoenflies.GeneratedPair.unique_source_face_of_outerOnly {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) {v F : γ} (hv : v ∈ T.str.skel.vertexSet) (hF : F ∈ T.str.faces) (hvF : T.str.sub v F) (houter : T.str.OuterOnlyAt v) (htwo : T.str.OuterIncidenceAtMostTwo v) (R : Set Plane) : R ∈ {A : Set Plane | ∃ Z ∈ T.str.faces, A = T.src.cell Z} → T.src.pos v ∈ closure R → R = T.src.cell F

At an outer-only vertex with at most two outer branches, the selected incident face is the only incident face. Each simple face boundary contributes two distinct edges at the vertex; the two-branch bound forces two such face boundaries to share an outer edge, and CombInvariants.outerEdge_unique then identifies their face names.

def Schoenflies.GeneratedPair.sourceNonboundaryVertices {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) : Set Plane

Source vertices incident with a nonboundary edge. Outer-only vertices are deliberately excluded: a fresh anchor must not enter the compact set merely because it is already a vertex of the outer cycle.

Equations

• T.sourceNonboundaryVertices = {x : Schoenflies.Plane | ∃ e ∈ T.src.graph.edgeSet, e ∉ T.str.outerGraph.edgeSet ∧ T.src.graph.Inc e x}

def Schoenflies.GeneratedPair.sourceNonboundaryGraph {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) : Graph Plane γ

The current source graph with outer edges and outer-only vertices removed. Its point set is the compact union of the closed nonboundary edges used in the fresh-anchor argument.

Equations

• T.sourceNonboundaryGraph = (T.src.graph.deleteEdges T.str.outerGraph.edgeSet).induce T.sourceNonboundaryVertices

theorem Schoenflies.GeneratedPair.sourceNonboundaryGraph_le {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) : T.sourceNonboundaryGraph ≤ T.src.graph

instance Schoenflies.GeneratedPair.sourceNonboundaryGraph_finite {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) : T.sourceNonboundaryGraph.Finite

theorem Schoenflies.GeneratedPair.source_pos_notMem_nonboundaryGraph_of_outerOnlyAt {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) {v : γ} (hv : v ∈ T.str.skel.vertexSet) (houter : T.str.OuterOnlyAt v) : T.src.pos v ∉ T.sourceNonboundaryGraph.pointSet T.src.drawing

An outer-only abstract vertex is absent from the compact nonboundary-edge carrier. The point-set statement includes the possible case where the vertex lies on the arc of an edge; the drawing axiom turns that case back into incidence with the same edge.

theorem Schoenflies.GeneratedPair.skeletonSet_eq_sourceNonboundaryGraph_union {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) : T.src.skeletonSet = T.sourceNonboundaryGraph.pointSet T.src.drawing ∪ srcOuter

The source skeleton is the union of its compact nonboundary-edge carrier and its outer curve.

theorem Schoenflies.GeneratedPair.isCompact_sourceNonboundaryGraph {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) : IsCompact (T.sourceNonboundaryGraph.pointSet T.src.drawing)

theorem Schoenflies.GeneratedPair.source_cellsAbsorbIn_nonboundary {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) : CellsAbsorbIn (srcDom \ srcOuter) (T.sourceNonboundaryGraph.pointSet T.src.drawing) {A : Set Plane | ∃ F ∈ T.str.faces, A = T.src.cell F}

Inside the open Jordan domain, avoiding the compact nonboundary-edge carrier is equivalent to avoiding the whole current skeleton; the remaining part of the latter is the outer curve.

theorem Schoenflies.GeneratedPair.exists_source_face_of_mem_interior_notMem_nonboundary {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) {x : Plane} (hx : x ∈ srcDom \ srcOuter) (hxCore : x ∉ T.sourceNonboundaryGraph.pointSet T.src.drawing) : ∃ R ∈ {A : Set Plane | ∃ F ∈ T.str.faces, A = T.src.cell F}, x ∈ R

Every point of the open source domain outside the compact nonboundary-edge carrier lies in one current source face.

theorem Schoenflies.GeneratedPair.source_polyAccessible_of_fresh {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) {F : γ} {x : Plane} (hstrong : StronglyAccessible (srcDom \ srcOuter) x) (hfresh : x ∉ T.sourceNonboundaryGraph.pointSet T.src.drawing) (hunique : ∀ R ∈ {A : Set Plane | ∃ Z ∈ T.str.faces, A = T.src.cell Z}, x ∈ closure R → R = T.src.cell F) : PolyAccessible (T.src.cell F) x

A fresh strongly accessible boundary anchor is accessible from its unique incident current source face. Compactness, absorption, and coverage are all discharged from the generated-pair invariants; the three hypotheses are exactly the data maintained by the prescribed ear order.

theorem Schoenflies.GeneratedPair.source_polyAccessible_of_notMem_outer {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) {F : γ} {x : Plane} (hF : F ∈ T.str.faces) (hx : x ∈ closure (T.src.cell F)) (hxOuter : x ∉ srcOuter) : PolyAccessible (T.src.cell F) x

A point in the closure of a current source face is polygonally accessible whenever it is off the wild outer curve. The polygonal graph used by polygonal_side_accessibility is the current skeleton with its outer edges deleted; adjoining the compact outer curve recovers the whole source skeleton.

def Schoenflies.GeneratedPair.SourceEndpointReady {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (F : γ) (x : Plane) : Prop

The two ways a source endpoint is ready for a reverse ear: it is off the wild curve, or it is a fresh strongly accessible anchor incident with one prescribed current face.

Equations

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

def Schoenflies.GeneratedPair.SourceEndpointFreshCombinatorics {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (F : γ) (x : Plane) : Prop

The two genuinely evolving obligations at a wild-boundary endpoint: no nonboundary edge has reached it yet, and the next ear's face is its unique incident current source face.

Equations

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

def Schoenflies.TargetEarFreshCombinatorics {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (H : Graph Plane γ) (Hdraw : γ → ℝ → Plane) : Prop

The remaining prescribed-ear combinatorics after boundary anchoring has supplied strong accessibility: both outer endpoints are fresh and incident with the selected face alone.

Equations

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

theorem Schoenflies.targetEarFreshCombinatorics_of_noNewNonouterIncidence_of_outerIncidenceAtMostTwo {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (hnoNew : NoNewNonouterIncidenceAtBoundary P.tgt.skeletonSet H Hdraw tgtOuter) (htwo : ∀ (S : CellStructure γ), GeneratedStructure S₀ S → S.OuterIncidenceAtMostTwoEverywhere) : TargetEarFreshCombinatorics P H Hdraw

The relative no-new-incidence boundary condition, together with the static two-branch invariant of generated outer graphs, supplies all reverse-ear fresh combinatorics.

theorem Schoenflies.targetEarFreshCombinatorics_of_nonouterIncidenceUnique_of_outerIncidenceAtMostTwo {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (hunique : NonouterIncidenceUniqueAtBoundary H Hdraw tgtOuter) (htwo : ∀ (S : CellStructure γ), GeneratedStructure S₀ S → S.OuterIncidenceAtMostTwoEverywhere) : TargetEarFreshCombinatorics P H Hdraw

Global uniqueness is a sufficient special case of the relative no-new-incidence condition.

theorem Schoenflies.targetEarFreshCombinatorics_of_noNewNonouterIncidence_of_outerCycle {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (hnoNew : NoNewNonouterIncidenceAtBoundary P.tgt.skeletonSet H Hdraw tgtOuter) (hcycle : S₀.OuterEdgesFormCycle) : TargetEarFreshCombinatorics P H Hdraw

The relative no-new-incidence condition and an outer cycle on the base structure supply the reverse-ear fresh combinatorics.

theorem Schoenflies.targetEarFreshCombinatorics_of_nonouterIncidenceUnique_of_outerCycle {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (hunique : NonouterIncidenceUniqueAtBoundary H Hdraw tgtOuter) (hcycle : S₀.OuterEdgesFormCycle) : TargetEarFreshCombinatorics P H Hdraw

The preceding reverse-ear combinatorics follows from the natural base invariant that the distinguished outer edges form one simple cycle.

def Schoenflies.TargetEarFreshInvariant {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (H : Graph Plane γ) (Hdraw : γ → ℝ → Plane) : Prop

The combinatorial/anchoring invariant still required from the prescribed target ear order: both source endpoints selected by every nontrivial target ear are ready in the preceding sense.

Equations

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

theorem Schoenflies.targetEarFreshInvariant_of_newBoundaryAnchored {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (H : Graph Plane γ) (Hdraw : γ → ℝ → Plane) (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (hanchor : NewTargetBoundaryAnchored P P.tgt.skeletonSet H Hdraw) (hcomb : TargetEarFreshCombinatorics P H Hdraw) : TargetEarFreshInvariant P H Hdraw

Relative anchoring of new ambient boundary edges and the remaining fresh-incidence combinatorics together give the complete reverse-ear readiness invariant.

theorem Schoenflies.targetEarFreshInvariant_of_boundaryAnchored {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (H : Graph Plane γ) (Hdraw : γ → ℝ → Plane) (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (hanchor : TargetBoundaryAnchored P H Hdraw) (hcomb : TargetEarFreshCombinatorics P H Hdraw) : TargetEarFreshInvariant P H Hdraw

Anchoring every nonouter boundary edge is a sufficient special case of relative new-edge anchoring.

def Schoenflies.TargetEarEndpointAccessibility {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (H : Graph Plane γ) (Hdraw : γ → ℝ → Plane) : Prop

Both source endpoints of every nontrivial target ear are polygonally accessible from the source face selected by that ear. This is the geometric invariant direction (b) must maintain: off the wild curve it follows from polygonal-side accessibility, while a fresh wild-boundary endpoint is supplied by polyAccessible_of_stronglyAccessible.

Equations

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

theorem Schoenflies.targetEarEndpointAccessibility_of_freshInvariant {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (H : Graph Plane γ) (Hdraw : γ → ℝ → Plane) (hfresh : TargetEarFreshInvariant P H Hdraw) : TargetEarEndpointAccessibility P H Hdraw

The fresh-anchor invariant implies the endpoint-accessibility invariant: the off-curve branch uses polygonal-side accessibility, and the fresh branch uses the compact carrier and unique-face theorem above.

theorem Schoenflies.targetEarStepConstruction_of_endpointAccessibility {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} [Infinite γ] (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (H : Graph Plane γ) (Hdraw : γ → ℝ → Plane) (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (haccess : TargetEarEndpointAccessibility P H Hdraw) : TargetEarStepConstruction P H Hdraw hH

Endpoint accessibility supplies the missing source crosscut, after which the already-proved arc matching and split constructor complete one nontrivial reverse ear.

theorem Schoenflies.targetEarStep_of_endpointAccessibility {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} [Infinite γ] (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (H : Graph Plane γ) (Hdraw : γ → ℝ → Plane) (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (haccess : TargetEarEndpointAccessibility P H Hdraw) : TargetEarStep P H Hdraw

One reverse ear follows from the endpoint-accessibility invariant.

theorem Schoenflies.targetEarStep_of_freshInvariant {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} [Infinite γ] (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (H : Graph Plane γ) (Hdraw : γ → ℝ → Plane) (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (hfresh : TargetEarFreshInvariant P H Hdraw) : TargetEarStep P H Hdraw

One reverse ear follows from the concrete fresh-anchor/unique-face invariant.

structure Schoenflies.TargetCommonSubdivisionData {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (H : Graph Plane γ) (Hdraw : γ → ℝ → Plane) : Type u_1

Explicit output data for the target common-subdivision construction.

• graph : Graph Plane γ

  The part of H supported on the old target skeleton.

• pair : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom

  The matched pair after inserting every vertex of graph.

• parent : γ → γ

  The composite parent map from the subdivided pair to P.

• graph_isTwoConnected : self.graph.IsTwoConnected

  The traced graph remains 2-connected.

• graph_le : self.graph ≤ H

  The traced graph is a subgraph of the given target extension.

• isTargetPartialTransferOf : IsTargetPartialTransferOf self.pair P self.graph Hdraw self.parent

  The refined pair realizes the traced target graph.

noncomputable def Schoenflies.targetCommonSubdivisionData {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} [Infinite γ] {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) : TargetCommonSubdivisionData P H Hdraw

Construct the target trace, its matched subdivision, and the composite parent map.

Equations

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

theorem Schoenflies.targetCommonSubdivision {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} [Infinite γ] {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) : TargetCommonSubdivision P H Hdraw

Step 1 of finite transfer, direction (b): construct the target common subdivision.

theorem Schoenflies.targetTransferOfEars {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (hsub : TargetCommonSubdivision P H Hdraw) (hstep : TargetEarStep P H Hdraw) : ∃ (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (par : γ → γ), IsTargetPartialTransferOf T P H Hdraw par

Iterate a target ear step from a common subdivision through the whole extension graph.

theorem Schoenflies.finite_transfer_toward_source_of_targetEarStep {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} [Infinite γ] {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (hstep : TargetEarStep P H Hdraw) : ∃ (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (par : γ → γ), IsTargetTransferOf T P H Hdraw par

Direction (b), assuming only the target ear step.

theorem Schoenflies.finite_transfer_toward_source_of_endpointAccessibility {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} [Infinite γ] {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (haccess : TargetEarEndpointAccessibility P H Hdraw) : ∃ (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (par : γ → γ), IsTargetTransferOf T P H Hdraw par

Direction (b), reduced to the precise geometric endpoint-accessibility invariant maintained by the prescribed outer-cycle ear order.

theorem Schoenflies.finite_transfer_toward_source_of_freshInvariant {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} [Infinite γ] {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (hfresh : TargetEarFreshInvariant P H Hdraw) : ∃ (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (par : γ → γ), IsTargetTransferOf T P H Hdraw par

Direction (b), reduced to the prescribed ear order's concrete fresh-anchor and unique-incident-face invariant. All geometric accessibility and reverse-split construction is discharged.

theorem Schoenflies.finite_transfer_toward_source_of_newBoundaryAnchored {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} [Infinite γ] {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (hanchor : NewTargetBoundaryAnchored P P.tgt.skeletonSet H Hdraw) (hcomb : TargetEarFreshCombinatorics P H Hdraw) : ∃ (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (par : γ → γ), IsTargetTransferOf T P H Hdraw par

Direction (b), with strong accessibility discharged by relative anchoring of new target boundary edges. The only remaining hypothesis is the fresh-carrier and unique-face combinatorics of the ear order.

theorem Schoenflies.finite_transfer_toward_source_of_boundaryAnchored {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} [Infinite γ] {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (hanchor : TargetBoundaryAnchored P H Hdraw) (hcomb : TargetEarFreshCombinatorics P H Hdraw) : ∃ (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (par : γ → γ), IsTargetTransferOf T P H Hdraw par

Anchoring every nonouter target-boundary edge is a sufficient special case.

theorem Schoenflies.finite_transfer_toward_source_of_relativeBoundaryGeometry {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} [Infinite γ] {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (hanchor : NewTargetBoundaryAnchored P P.tgt.skeletonSet H Hdraw) (hnoNew : NoNewNonouterIncidenceAtBoundary P.tgt.skeletonSet H Hdraw tgtOuter) (hcycle : S₀.OuterEdgesFormCycle) : ∃ (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (par : γ → γ), IsTargetTransferOf T P H Hdraw par

Finite transfer, direction (b), from relative ambient boundary geometry. Boundary endpoints must be anchored, and a genuinely new nonouter edge must not coexist there with a nonouter edge already in the current trace. The abstract base needs one distinguished outer cycle.

theorem Schoenflies.finite_transfer_toward_source_of_boundaryGeometry {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} [Infinite γ] {P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (hH : IsSourceExtension P.tgt tgtOuter tgtDom H Hdraw) (hanchor : TargetBoundaryAnchored P H Hdraw) (hunique : NonouterIncidenceUniqueAtBoundary H Hdraw tgtOuter) (hcycle : S₀.OuterEdgesFormCycle) : ∃ (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (par : γ → γ), IsTargetTransferOf T P H Hdraw par

Finite transfer, direction (b), from name-independent ambient boundary geometry. Global uniqueness of the incident nonouter edge implies the relative condition used by reverse ear insertion.