Finite transfer, direction (a): toward the square

thm:finite-transfer is the largest single statement of the manuscript. This module states it — in full, with every hypothesis — for direction (a) only, and proves as much of its four-step proof as is within reach of what is on main.

Direction (b) is deliberately absent: its extra accessibility problem at the wild source boundary needs lem:tangent-cone, lem:compact-separation(c) and the fresh-point bookkeeping of the target mesh, none of which enters (a).

The statement, and how it is read

The blueprint's (a) reads: let (Γ, Γ') be a generated matched cellulation; suppose H is a finite 2-connected plane graph containing a subdivision of Γ, with outer cycle C, with every nonboundary edge polygonal, and with |H| ∖ C connected; then the common subdivision can be made on Γ', and H can be transferred to an admissible target realization H'; the resulting generated matched cellulation refines the old one by explicit parent maps.

Four objects carry that sentence.

• Schoenflies.CellStructure.Realization.IsWeaklyAdmissible and Schoenflies.CellStructure.Realization.IsAdmissible — def:admissible-graph. The weak form is exactly the strong one with connectedness of the open nonboundary part waived, which is what def:generated-structure requires of an intermediate stage and what rem:intermediate-disconnection insists on.
• Schoenflies.GeneratedPair — a generated matched cell structure with its geometry: the abstract structure, its two realizations, the skeleton homeomorphism, and the two cell decompositions. This is the Lean form of "(Γ, Γ') is a generated matched cellulation". It is a bundle of data, not an existential: every consumer reads .src, .tgt, .homeo by name.
• Schoenflies.IsSourceExtension — the hypotheses on H.
• Schoenflies.IsTransferOf — the conclusion, relating the new pair to the old one by an explicit parent map.

The one place where the Lean statement is weaker in form than the prose, and deliberately so: "H can be transferred" is recorded as T.src.skeletonSet = pointSet H Hdraw, an equality of point sets, rather than as a graph isomorphism onto H. The reason is step 1: the common subdivision inserts a vertex at every intersection of a new edge with an old one, so the source realization of the transferred structure realizes a subdivision of H, never H itself. What survives verbatim is what the construction uses downstream — the occupied set, the 2-connectivity (which lem:combinatorial-invariance moves to the target) and the refinement.

What is proved here

• Step 1, the overlay — Schoenflies.exists_overlay_of_biUnion_finite: the union of finitely many nondegenerate polygonal sets is the point set of a finite plane graph drawn by straight segments. That is lem:polygonal-overlay in the form step 1 needs, bridging Schoenflies.polygonal_overlay, which is stated for a list of segments, to the finite family of polygonal arcs a skeleton stage arrives as.
• Step 4, target side — Schoenflies.exists_target_crosscut and Schoenflies.exists_target_crosscut_split. In direction (a) the target face F* is a polygonal Jordan region in the square by lem:cellulation-invariants(vii); every point of its boundary is polygonally accessible from its interior by lem:polygonal-side-accessibility (target half); and lem:accessible-endpoints gives a polygonal crosscut P* ⊆ closure F* from v* to w*, which by thm:general-crosscut splits F* into exactly the two Jordan regions bounded by P* and the two boundary paths. These constructions supply the complete target-side argument.
• The second sentence of step 2 — …IsCellDecomposition.exists_unique_face_subset_cell and …IsCellDecomposition.exists_face_of_ear: the interior of an ear lies in one current face, because it is connected and disjoint from the current skeleton, and its two endpoints then lie on that face's boundary cycle. IsCellDecomposition.cellsAbsorb derives the formerly named CellsAbsorb premise from the maintained cell-decomposition and Jordan-face invariants, so this requires no additional interface.
• One ear insertion, step 3 — exists_sourceEarStepData, EarCrosscut.exists_matched_target, earStepConstruction, and earStep. The ambient source path is given fresh abstract cell names, its face split is realized on both sides, and a parameter-matching homeomorphism divides the target polygonal crosscut into exactly the same abstract edges. Matching source and target crosscuts then produce the next pair, compose both refinement maps, preserve every bundle invariant, and enlarge the occupied source graph by exactly the supplied ear, under the necessary [Infinite γ] name supply.
• The last paragraph of the proof — Schoenflies.GeneratedPair.src_isAdmissible and Schoenflies.GeneratedPair.tgt_isAdmissible. Admissibility of the final object is recovered from lem:combinatorial-invariance: the reproduced realization has the same 2-connectivity and the same connectedness of the open nonboundary part as the given one. This uses only the hypotheses of the finite-transfer statement.
• The induction scheme, steps 2 and 3 — Schoenflies.transfer_of_ears. With earStep supplying each insertion, lem:relative-ear in its iterated form (Graph.IsTwoConnected.ear_decomposition) transfers the whole extension. This is the backbone of the induction, and it honours rem:intermediate-disconnection: the invariant carried through the induction, Schoenflies.IsPartialTransferOf, asks only for weak admissibility, and connectedness of the open nonboundary part is restored only at the very end.

Completion of step 1

This module keeps Schoenflies.CommonSubdivision as the compositional interface consumed by the ear induction. Schoenflies/CommonSubdivision.lean constructs it: it traces the part of H supported on the old skeleton, proves that trace 2-connected, and carries all of its finitely many vertices through matched source/target edge subdivisions. Consequently direction (a) is exposed there as Schoenflies.finite_transfer_toward_square.

Blueprint

• Schoenflies.CellStructure.Realization.IsWeaklyAdmissible, Schoenflies.CellStructure.Realization.IsAdmissible — def:admissible-graph.
• Schoenflies.GeneratedPair — def:generated-structure with its two realizations, def:matched-pair and def:matched-cellulation folded in.
• Schoenflies.IsSourceExtension — the hypotheses of thm:finite-transfer(a) on H.
• Schoenflies.IsPartialTransferOf, Schoenflies.IsTransferOf — the conclusion of thm:finite-transfer, at an intermediate stage and at the end.
• Schoenflies.exists_target_crosscut, Schoenflies.exists_target_crosscut_split — the fourth paragraph of the proof of thm:finite-transfer, direction (a): lem:cellulation-invariants(vii) + lem:polygonal-side-accessibility + lem:accessible-endpoints + thm:general-crosscut.
• Schoenflies.CellStructure.Realization.IsCellDecomposition.exists_unique_face_subset_cell, …IsCellDecomposition.exists_face_of_ear, …IsCellDecomposition.sub_of_pos_mem_closure_cell — "the interior of each ear lies in one current face", with the two supporting facts Schoenflies.CellStructure.Realization.cell_subset_skeletonSet (hoisted to Schoenflies/CombinatorialInvariance.lean) and Schoenflies.CellStructure.Realization.mem_faces_of_notMem_skeletonSet.
• Schoenflies.CellStructure.Realization.pos_mem_closure_cell_congr, Schoenflies.exists_target_ear — "let F*, v*, w* be the corresponding face and endpoints in the other realization", and the whole fourth paragraph assembled from the source-side data.
• Schoenflies.GeneratedPair.src_isAdmissible, Schoenflies.GeneratedPair.tgt_isAdmissible — the last paragraph of the proof, via lem:combinatorial-invariance.
• Schoenflies.exists_overlay_of_biUnion_finite — lem:polygonal-overlay and rem:polygonal-overlay-convention, for a finite family of polygonal sets: the first half of step 1.
• Schoenflies.earStep — step 3; Schoenflies.CommonSubdivision — the step-1 interface, discharged by Schoenflies.commonSubdivision in CommonSubdivision.lean.
• Schoenflies.transfer_of_ears_of_commonSubdivision_of_earStep, Schoenflies.finite_transfer_toward_square_of_commonSubdivision_of_earStep — the finite-transfer induction parametrized by its two construction interfaces.

def:admissible-graph

An admissible graph in the closed Jordan domain is a finite 2-connected plane graph whose outer cycle is C, whose edges not contained in C are polygonal arcs with interiors in D, and whose open nonboundary part |Γ| ∖ C is connected. A weakly admissible graph satisfies everything but the last clause.

outer is the realized outer cycle and dom the closed domain; the open domain is dom ∖ outer. On the source side that reads C and C ∪ D; on the target side S and Q.

structure Schoenflies.CellStructure.Realization.IsWeaklyAdmissible {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) (outer dom : Set Plane) : Prop

A weakly admissible realization — def:admissible-graph with connectedness of the open nonboundary part waived, which is what def:generated-structure requires of every intermediate stage (rem:intermediate-disconnection).

• isTwoConnected : R.graph.IsTwoConnected

  The drawn skeleton is 2-connected.

• outerSet_eq : R.outerSet = outer

  The realized outer cycle is the prescribed curve.

• isPolygonal ⦃e : γ⦄ : e ∈ S.skel.edgeSet → e ∉ S.outerGraph.edgeSet → IsPolygonal (Graph.edgeArc R.drawing e)

  Every nonboundary edge is a polygonal arc.

• cell_subset ⦃e : γ⦄ : e ∈ S.skel.edgeSet → e ∉ S.outerGraph.edgeSet → R.cell e ⊆ dom \ outer

  Every nonboundary edge has its interior in the open domain. Endpoints may lie on the outer cycle, as for a crosscut.

• skeletonSet_subset : R.skeletonSet ⊆ dom

  The whole skeleton lies in the closed domain.

structure Schoenflies.CellStructure.Realization.IsAdmissible {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) (outer dom : Set Plane) extends R.IsWeaklyAdmissible outer dom : Prop

An admissible realization — def:admissible-graph in full.

• isTwoConnected : R.graph.IsTwoConnected
• outerSet_eq : R.outerSet = outer
• isPolygonal ⦃e : γ⦄ : e ∈ S.skel.edgeSet → e ∉ S.outerGraph.edgeSet → IsPolygonal (Graph.edgeArc R.drawing e)
• cell_subset ⦃e : γ⦄ : e ∈ S.skel.edgeSet → e ∉ S.outerGraph.edgeSet → R.cell e ⊆ dom \ outer
• skeletonSet_subset : R.skeletonSet ⊆ dom
• isConnected_nonboundary : IsConnected R.nonboundary

  The open nonboundary part |Γ| ∖ C is connected.

theorem Schoenflies.CellStructure.SplitData.EarCrosscut.isWeaklyAdmissible_realize {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {outer dom : Set Plane} {earPos : γ → Plane} {earDraw : γ → ℝ → Plane} (hE : d.EarCrosscut R earPos earDraw) (hR : R.IsWeaklyAdmissible outer dom) (hcd : R.IsCellDecomposition dom) (hpoly : ∀ ⦃e : γ⦄, e ∈ d.ear.edgeSet → IsPolygonal (Graph.edgeArc earDraw e)) : (realize R d earPos earDraw hE).IsWeaklyAdmissible outer dom

Weak admissibility is preserved by adjoining a polygonal ear inside one old face. This is the geometric bookkeeping common to the source and target halves of every ear step.

theorem Schoenflies.CellStructure.SplitData.EarCrosscut.exists_matched_target {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R₁ R₂ : S.Realization} {srcPos : γ → Plane} {srcDraw : γ → ℝ → Plane} (hsrc : d.EarCrosscut R₁ srcPos srcDraw) {A : Set Plane} (hApoly : IsPolygonal A) (hAarc : IsArcBetween A (R₂.pos d.source) (R₂.pos d.target)) (hAsub : A \ {R₂.pos d.source, R₂.pos d.target} ⊆ R₂.cell d.face) (hdisj : Disjoint (R₂.cell d.face) R₂.skeletonSet) : ∃ (tgtPos : γ → Plane) (tgtDraw : γ → ℝ → Plane) (x : d.EarHomeo srcPos srcDraw tgtPos tgtDraw), d.EarCrosscut R₂ tgtPos tgtDraw ∧ ∀ ⦃e : γ⦄, e ∈ d.ear.edgeSet → IsPolygonal (Graph.edgeArc tgtDraw e)

A set-level target crosscut can be divided into exactly the abstract edges of an already drawn source ear. The division is obtained by matching the parameters of the two whole arcs: each target edge is the image of its source counterpart. Closed subarcs of the polygonal target crosscut are polygonal, so no relation between the number of straight segments on the two sides is needed.

Where an ear can lie

The interior of each ear lies in one current face, because it is connected and disjoint from the current skeleton. That is the second sentence of step 2, and it is proved here for an arbitrary connected subset of the closed domain missing the skeleton.

The only input beyond assertion (i) is Schoenflies.CellsAbsorb — assertion (i) in the "a connected set disjoint from the skeleton that meets a 2-cell lies in it" reading, which Schoenflies/SkeletonAccess.lean also carries as its single hypothesis and which Schoenflies.cellsAbsorb_of_isComponent_in discharges on the target side.

theorem Schoenflies.CellStructure.Realization.mem_faces_of_notMem_skeletonSet {γ : Type u_1} {S : CellStructure γ} {σ : γ} {z : Plane} (R : S.Realization) (hσ : σ ∈ S.cells) (hz : z ∈ R.cell σ) (hznot : z ∉ R.skeletonSet) : σ ∈ S.faces

A cell whose open part contains a point off the skeleton is a 2-cell.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.frontier_cell_subset_skeletonSet {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {F : γ} (h : R.IsCellDecomposition D) (hJ : R.IsFaceJordan) (hF : F ∈ S.faces) : frontier (R.cell F) ⊆ R.skeletonSet

The frontier of a Jordan face is part of the realized 1-skeleton. Assertion (i) writes the frontier as the union of strict subcells; assertion (vii) rules out a second face among those subcells, leaving only vertices and edges.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.cellsAbsorb {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} (h : R.IsCellDecomposition D) (hJ : R.IsFaceJordan) : CellsAbsorb R.skeletonSet {A : Set Plane | ∃ F ∈ S.faces, A = R.cell F}

Assertions (i) and (vii) discharge the CellsAbsorb reading of the cellulation invariant: a connected set missing the skeleton cannot cross the Jordan frontier of a face it meets.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.face_eq_connectedComponentIn {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D Q : Set Plane} {F : γ} (h : R.IsCellDecomposition D) (hJ : R.IsFaceJordan) (hF : F ∈ S.faces) (hFQ : R.cell F ⊆ Q) (z : Plane) (hz : z ∈ R.cell F) : R.cell F = connectedComponentIn (Q \ R.skeletonSet) z

A Jordan face contained in an ambient open set Q is a connected component of Q \ skeleton as soon as its frontier belongs to the skeleton.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.sub_of_pos_mem_closure_cell {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} (h : R.IsCellDecomposition D) {a F : γ} (ha : a ∈ S.skel.vertexSet) (hF : F ∈ S.faces) (hmem : R.pos a ∈ closure (R.cell F)) : S.sub a F

A 0-cell in the closure of an open 2-cell is a subcell of it — assertion (ix) read at a vertex. This is how an ear's endpoint is recognised as lying on the boundary cycle of the face its interior occupies.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.exists_unique_face_subset_cell {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D N : Set Plane} (h : R.IsCellDecomposition D) (hcells : CellsAbsorb R.skeletonSet {A : Set Plane | ∃ F ∈ S.faces, A = R.cell F}) (hN : IsPreconnected N) (hNne : N.Nonempty) (hND : N ⊆ D) (hNdisj : Disjoint N R.skeletonSet) : ∃ F ∈ S.faces, N ⊆ R.cell F ∧ ∀ T ∈ S.faces, N ⊆ R.cell T → T = F

An ear lies in a single current face. A nonempty connected subset of the closed domain disjoint from the realized skeleton lies inside one open 2-cell, and inside only that one.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.exists_face_of_ear {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D N : Set Plane} (h : R.IsCellDecomposition D) (hcells : CellsAbsorb R.skeletonSet {A : Set Plane | ∃ F ∈ S.faces, A = R.cell F}) (hN : IsPreconnected N) (hNne : N.Nonempty) (hND : N ⊆ D) (hNdisj : Disjoint N R.skeletonSet) {a b : γ} (ha : a ∈ S.skel.vertexSet) (hb : b ∈ S.skel.vertexSet) (hacl : R.pos a ∈ closure N) (hbcl : R.pos b ∈ closure N) : ∃ F ∈ S.faces, N ⊆ R.cell F ∧ S.sub a F ∧ S.sub b F ∧ ∀ T ∈ S.faces, N ⊆ R.cell T → T = F

One ear, placed — the source-side input of the induction step. The open part N of the ear is connected, inside the closed domain and disjoint from the current skeleton, so it lies in a unique current 2-cell F; and each endpoint of the ear, being a 0-cell in the closure of N, is a subcell of F, i.e. lies on its boundary cycle.

Feeding the two S.sub conclusions back through IsCellDecomposition.subset_closure in the other realization is exactly Schoenflies.exists_target_ear's two closure hypotheses.

A generated matched cell structure, with its geometry

def:generated-structure says what the abstract object is; GeneratedStructure in Schoenflies/GeneratedStructure.lean is that. What a transfer produces, and what the finite-transfer theorem consumes, is the abstract object together with its two realizations, the skeleton homeomorphism between them, and the two cell decompositions of lem:cellulation-invariants(i). That bundle is GeneratedPair.

It is data, not a Prop: a consumer reads .src, .tgt, .homeo, .str by name.

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

A generated matched cell structure with its two realizations. The Lean form of "(Γ, Γ') is a generated matched cellulation", except that only weak admissibility is a field — rem:intermediate-disconnection — with the connected form carried separately by the consumers that have it.

• str : CellStructure γ

  The abstract cell structure.

• generated : GeneratedStructure S₀ self.str

  It is generated from the base by a finite sequence of elementary operations.

• str_combInvariants : self.str.CombInvariants

  The maintained combinatorial invariants of the current abstract structure.

• str_boundaryCycles : self.str.BoundaryCycles

  Every current face has a simple cyclic abstract boundary.

• src : self.str.Realization

  The realization in the closed Jordan domain.

• tgt : self.str.Realization

  The realization in the closed square.

• homeo : CellStructure.SkeletonHomeo self.src self.tgt

  The skeleton homeomorphism g : |Γ| → |Γ'| of def:matched-pair.

• src_isCellDecomposition : self.src.IsCellDecomposition srcDom

  Assertion (i) on the source side.

• tgt_isCellDecomposition : self.tgt.IsCellDecomposition tgtDom

  Assertion (i) on the target side.

• src_isFaceJordan : self.src.IsFaceJordan

  Assertion (vii) on the source side: every face is the inside of its Jordan frontier.

• tgt_isFaceJordan : self.tgt.IsFaceJordan

  Assertion (vii) on the target side. A split needs this geometric information in addition to the cell-decomposition clauses.

• tgtInterior_isOpen : IsOpen (tgtDom \ tgtOuter)

  The open part of the target domain.

• tgtInterior_frontier_subset : frontier (tgtDom \ tgtOuter) ⊆ self.tgt.skeletonSet

  Its frontier is already part of the target skeleton.

• tgt_isPolygonal ⦃e : γ⦄ : e ∈ self.str.skel.edgeSet → IsPolygonal (Graph.edgeArc self.tgt.drawing e)

  Every target edge is polygonal, including the distinguished outer edges.

• src_isWeaklyAdmissible : self.src.IsWeaklyAdmissible srcOuter srcDom

  The source realization is weakly admissible.

• tgt_isWeaklyAdmissible : self.tgt.IsWeaklyAdmissible tgtOuter tgtDom

  The target realization is weakly admissible.

theorem Schoenflies.GeneratedPair.combInvariants {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (h₀ : S₀.CombInvariants) : P.str.CombInvariants

The combinatorial invariants hold at every generated stage, once they hold at the base — Schoenflies.GeneratedStructure.combInvariants, read off the bundle.

theorem Schoenflies.GeneratedPair.boundaryCycles {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (hcycles : S₀.BoundaryCycles) (h₀ : S₀.CombInvariants) : P.str.BoundaryCycles

Every face of a generated pair has a simple cyclic boundary once this is true at the base. This is the source of the two abstract boundary paths consumed by an ear split.

theorem Schoenflies.GeneratedPair.src_nonboundary_eq {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) : P.src.nonboundary = P.src.skeletonSet \ srcOuter

The open nonboundary part of the source realization, read off the two clauses that pin the skeleton and the outer cycle.

theorem Schoenflies.GeneratedPair.tgt_isAdmissible {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (h : IsConnected P.src.nonboundary) : P.tgt.IsAdmissible tgtOuter tgtDom

The last paragraph of the proof of thm:finite-transfer, target half. Once the source realization's open nonboundary part is connected, so is the target's — this is part (b) of lem:combinatorial-invariance — and the target realization, weakly admissible by construction, is therefore admissible.

theorem Schoenflies.GeneratedPair.src_isAdmissible {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (h : IsConnected P.src.nonboundary) : P.src.IsAdmissible srcOuter srcDom

The last paragraph of the proof, source half.

theorem Schoenflies.GeneratedPair.tgt_face_subset_interior {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) {F : γ} (hF : F ∈ P.str.faces) : P.tgt.cell F ⊆ tgtDom \ tgtOuter

Every target face lies in the open part of the prescribed target domain.

theorem Schoenflies.GeneratedPair.tgt_face_isComponent {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) {F : γ} (hF : F ∈ P.str.faces) : P.tgt.cell F ⊆ tgtDom \ tgtOuter ∧ ∃ (z : Plane), P.tgt.cell F = connectedComponentIn ((tgtDom \ tgtOuter) \ P.tgt.skeletonSet) z

Target faces have the component presentation consumed by polygonal side accessibility.

The matched split constructor

RealizeSplit and MatchedSplit construct the two new realizations and their skeleton homeomorphism. The definition below is the missing bundle-level constructor: it installs those objects in a GeneratedPair and records the propagated cell-decomposition and Jordan-face invariants. Weak admissibility is then derived from the old pair and the two polygonal ear drawings by EarCrosscut.isWeaklyAdmissible_realize.

noncomputable def Schoenflies.GeneratedPair.split {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (hS : P.str.CombInvariants) (d : P.str.SplitData) (srcPos : γ → Plane) (srcDraw : γ → ℝ → Plane) (tgtPos : γ → Plane) (tgtDraw : γ → ℝ → Plane) (hsrc : d.EarCrosscut P.src srcPos srcDraw) (htgt : d.EarCrosscut P.tgt tgtPos tgtDraw) (m : d.EarHomeo srcPos srcDraw tgtPos tgtDraw) (hsrcEdgePoly : ∀ ⦃e : γ⦄, e ∈ d.ear.edgeSet → IsPolygonal (Graph.edgeArc srcDraw e)) (htgtEdgePoly : ∀ ⦃e : γ⦄, e ∈ d.ear.edgeSet → IsPolygonal (Graph.edgeArc tgtDraw e)) : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom

Build the next generated pair from matching geometric realizations of one abstract face split.

Equations

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

@[simp]

theorem Schoenflies.GeneratedPair.split_str {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (hS : P.str.CombInvariants) (d : P.str.SplitData) (srcPos : γ → Plane) (srcDraw : γ → ℝ → Plane) (tgtPos : γ → Plane) (tgtDraw : γ → ℝ → Plane) (hsrc : d.EarCrosscut P.src srcPos srcDraw) (htgt : d.EarCrosscut P.tgt tgtPos tgtDraw) (m : d.EarHomeo srcPos srcDraw tgtPos tgtDraw) (hsrcEdgePoly : ∀ ⦃e : γ⦄, e ∈ d.ear.edgeSet → IsPolygonal (Graph.edgeArc srcDraw e)) (htgtEdgePoly : ∀ ⦃e : γ⦄, e ∈ d.ear.edgeSet → IsPolygonal (Graph.edgeArc tgtDraw e)) : (P.split hS d srcPos srcDraw tgtPos tgtDraw hsrc htgt m hsrcEdgePoly htgtEdgePoly).str = P.str.splitFace d

The hypotheses of direction (a) on the given extension

H is a finite 2-connected plane graph containing a subdivision of Γ, with outer cycle C, with every nonboundary edge polygonal, and with |H| ∖ C connected.

"Contains a subdivision of Γ" is recorded by three clauses: every old vertex is a vertex of H; the old skeleton is inside |H|; and any edge of H whose nonvertex part meets an open old edge lies inside that old edge. Together those say that each old edge is cut into a chain of H-edges. A transverse crossing is allowed only at a vertex of H, exactly as produced by the polygonal overlay.

"With outer cycle C, with every nonboundary edge polygonal" is edge_dichotomy: each edge of H either lies inside the outer curve or is polygonal with its interior in the open domain. Recording the outer cycle as a subgraph would put data inside a Prop; this reading is what every step of the proof actually uses, and outer ⊆ pointSet H Hdraw comes for free from skeletonSet_subset.

structure Schoenflies.IsSourceExtension {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) (outer dom : Set Plane) (H : Graph Plane γ) (Hdraw : γ → ℝ → Plane) : Prop

The hypotheses of thm:finite-transfer(a) on the extension H.

• finite : H.Finite

  H is finite.

• isDrawing : H.IsDrawing Hdraw

  H is a plane graph.

• isTwoConnected : H.IsTwoConnected

  H is 2-connected.

• vertexSet_subset : R.graph.vertexSet ⊆ H.vertexSet

  Every 0-cell of Γ is a vertex of H.

• skeletonSet_subset : R.skeletonSet ⊆ H.pointSet Hdraw

  |Γ| ⊆ |H|.

• edge_subset ⦃e : γ⦄ : e ∈ S.skel.edgeSet → ∀ ⦃f : γ⦄, f ∈ H.edgeSet → (Graph.edgeArc Hdraw f ∩ (R.cell e \ H.vertexSet)).Nonempty → Graph.edgeArc Hdraw f ⊆ Graph.edgeArc R.drawing e

  An edge of H whose interior meets an open edge of Γ runs inside it. Intersections at vertices of H are deliberately excluded: a transverse crossing is first made a vertex by the polygonal overlay, and does not make either of its two incident branches part of the old edge.

• pointSet_subset : H.pointSet Hdraw ⊆ dom

  H is drawn in the closed domain.

• edge_dichotomy ⦃f : γ⦄ : f ∈ H.edgeSet → Graph.edgeArc Hdraw f ⊆ outer ∨ IsPolygonal (Graph.edgeArc Hdraw f) ∧ Graph.edgeArc Hdraw f \ H.vertexSet ⊆ dom \ outer

  Each edge of H is an outer edge or a polygonal nonboundary edge with interior in the open domain.

• isConnected : IsConnected (H.pointSet Hdraw \ outer)

  |H| ∖ C is connected.

theorem Schoenflies.IsSourceExtension.not_isLoopAt {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {outer dom : Set Plane} {H : Graph Plane γ} {Hdraw : γ → ℝ → Plane} (h : IsSourceExtension R outer dom H Hdraw) ⦃f : γ⦄ ⦃x : Plane⦄ : ¬H.IsLoopAt f x

A plane graph has no loops, so lem:relative-ear applies to H.

The conclusion

IsPartialTransferOf T P B par is the invariant the induction of steps 2–3 carries: T is a generated pair refining P along par whose source realization occupies exactly what the current subgraph B of H occupies. It asks for no connectedness of the open nonboundary part — rem:intermediate-disconnection — because an ear with both endpoints on the outer cycle really does disconnect it, and later ears reconnect it.

IsTransferOf is the same with admissibility of both final realizations added; that is the theorem's conclusion, and GeneratedPair.src_isAdmissible / GeneratedPair.tgt_isAdmissible are what produce it from the connectedness hypothesis on H.

theorem Schoenflies.exists_injective_avoiding {γ : Type u_1} [Infinite γ] (used : Set γ) (hused : used.Finite) (ι : Type u_2) [Finite ι] : ∃ (fresh : ι → γ), Function.Injective fresh ∧ ∀ (i : ι), fresh i ∉ used

A finite family of fresh names can be chosen injectively outside any finite used set. This is the name-supply lemma used by the concrete ear relabelling: vertex, edge, and face requests are put in one finite sum type so their chosen names are automatically pairwise distinct.

theorem Schoenflies.exists_injOn_avoiding {γ : Type u_1} {α : Type u_2} [Infinite γ] (used : Set γ) (hused : used.Finite) {s : Set α} (hs : s.Finite) (fallback : γ) : ∃ (name : α → γ), Set.InjOn name s ∧ ∀ x ∈ s, name x ∉ used

Extend a finite injection of fresh names to a total function for graph relabelling.

theorem Schoenflies.exists_injective_pinned_avoiding {γ : Type u_1} {α : Type u_2} [Infinite γ] {used : Set γ} (hused : used.Finite) {u v : γ} (hu : u ∈ used) (hv : v ∈ used) (huv : u ≠ v) {s : Set α} (hs : s.Finite) {a b : α} (hab : a ≠ b) : ∃ (name : α → γ), name a = u ∧ name b = v ∧ Set.InjOn name s ∧ ∀ x ∈ s, x ≠ a → x ≠ b → name x ∉ used

Extend two prescribed, distinct names to an injection on a finite set, with every other value fresh outside a prescribed finite set.

structure Schoenflies.IsPartialTransferOf {γ : 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 stage of the transfer.

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

  The new source realization refines the old one along par — assertion (iv).

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

  The new target realization refines the old one along the same parent map. That sharing is lem:refinement-compatibility(c).

• 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.src.skeletonSet = B.pointSet Hdraw

  The new source skeleton occupies exactly what the current subgraph occupies.

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

  Every vertex of the current subgraph is a 0-cell of the new structure: the new structure realizes a subdivision of B, so it has at least B's vertices.

The output data of one realized ear

The former EarStep interface ended directly in an existential GeneratedPair. That hid all of the actual constructor data and made the last half of the proof impossible to reuse or inspect. EarStepData exposes the abstract split, its two geometric crosscuts, and the chosen map between them. Its pair and isPartialTransferOf_pair declarations below perform the assembly.

structure Schoenflies.EarStepData {γ : 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 the geometric path D to a partial transfer.

• splitData : T.str.SplitData

  The abstract face split, including the freshly named copy of the ear.

• srcPos : γ → Plane

  The source positions and edge parametrizations of that abstract ear.

• srcDraw : γ → ℝ → Plane

  Edge parametrizations of the new source ear.

• tgtPos : γ → Plane

  The target positions and edge parametrizations.

• tgtDraw : γ → ℝ → Plane

  Edge parametrizations of the matched target ear.

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

  Both drawings are crosscuts 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 cellwise homeomorphism used to extend the old skeleton homeomorphism.

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

  Every edge of both realized ears is polygonal.

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

  The relabelled source ear occupies exactly the path supplied by the ambient graph.

• vertexSet_subset : (B.union (H.pathGraphOf a D)).vertexSet ⊆ (CellStructure.SplitData.realize T.src self.splitData self.srcPos self.srcDraw ⋯).graph.vertexSet

  Every old or newly introduced graph vertex is a vertex of the new realization.

noncomputable def Schoenflies.EarStepData.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 : EarStepData T B H Hdraw a D) : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom

The generated pair assembled from the data of one realized ear.

Equations

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

@[simp]

theorem Schoenflies.EarStepData.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 : EarStepData T B H Hdraw a D) : w.pair.src = CellStructure.SplitData.realize T.src w.splitData w.srcPos w.srcDraw ⋯

@[simp]

theorem Schoenflies.EarStepData.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 : EarStepData T B H Hdraw a D) : w.pair.tgt = CellStructure.SplitData.realize T.tgt w.splitData w.tgtPos w.tgtDraw ⋯

theorem Schoenflies.EarStepData.isPartialTransferOf_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 : EarStepData T B H Hdraw a D) (hdraw : H.IsDrawing Hdraw) (hpath : H.IsPath a D b) (hab : a ≠ b) (hT : IsPartialTransferOf T P B Hdraw par) : IsPartialTransferOf w.pair P (B.union (H.pathGraphOf a D)) Hdraw (par ∘ w.splitData.parent)

The exposed constructor data really performs one EarStep: the pair it builds refines the original pair along the composite parent map, occupies the enlarged source graph, and contains all of that graph's vertices as 0-cells.

Locating the source face of a graph-theoretic ear

theorem Schoenflies.exists_source_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.src srcOuter srcDom 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 : IsPartialTransferOf T P B Hdraw par) : ∃ (u : γ) (v : γ) (F : γ), u ∈ T.str.skel.vertexSet ∧ v ∈ T.str.skel.vertexSet ∧ u ≠ v ∧ T.src.pos u = a ∧ T.src.pos v = b ∧ F ∈ T.str.faces ∧ Graph.edgesCover Hdraw D \ {a, b} ⊆ T.src.cell F ∧ T.str.sub u F ∧ T.str.sub v F

A nontrivial graph-theoretic ear determines two abstract endpoint vertices and a unique source face containing its open arc. This is the complete source-side input needed to choose the boundary paths of SplitData; in particular CellsAbsorb is no longer an extra hypothesis.

theorem Schoenflies.source_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.src srcOuter srcDom H Hdraw) (hpath : H.IsPath a D b) (hF : F ∈ T.str.faces) (hinside : Graph.edgesCover Hdraw D \ {a, b} ⊆ T.src.cell F) (e : γ) : e ∈ D → IsPolygonal (Graph.edgeArc Hdraw e)

Every edge of a genuine source ear is polygonal. The source-extension dichotomy allows an edge to be nonpolygonal only when its whole arc lies in the outer curve. But that curve is in the current skeleton, whereas the open ear lies in one current face and hence misses the skeleton; a nondegenerate drawn edge cannot then remain.

structure Schoenflies.IsTransferOf {γ : 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.IsPartialTransferOf T P H Hdraw par : Prop

The conclusion of thm:finite-transfer(a).

• 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.src.skeletonSet = H.pointSet Hdraw
• vertexSet_subset : H.vertexSet ⊆ T.src.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 — "H can be transferred to an admissible target realization H'".

The two assumed steps

Both are strictly weaker than thm:finite-transfer(a) itself, and both are statements a later module can discharge without circularity.

CommonSubdivision is step 1: after overlaying the proposed polygonal nonboundary edges with the old polygonal nonboundary skeleton and subdividing at every intersection — and transferring each new point to the other realization along the chosen edge parametrization — the old skeleton is literally a subgraph of the new one on both sides. In Lean that is: some 2-connected subgraph K ≤ H carries a generated pair refining the given one. It is not the theorem: it makes only edge subdivisions, inserts no ear, and its conclusion is about a subgraph of H, not about H.

EarStep is step 3: one ear insertion — at most two edge subdivisions followed by one 2-cell split — carries a partial transfer of B to a partial transfer of B with the ear glued on. Its geometric core in direction (a) is Schoenflies.exists_target_crosscut_split below, which is proved here; only the abstract-data bookkeeping around it is assumed.

The predicates describe transfer data independently of whether that data exists. Their constructors require [Infinite γ] to supply fresh cell names. Keeping infinitude on those existence theorems, rather than as an unused parameter of the predicates, makes that boundary explicit.

def Schoenflies.CommonSubdivision {γ : 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, the common subdivision, as an interface.

Equations

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

def Schoenflies.EarStep {γ : 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 3, one ear insertion, as an interface.

The data handed to the step is exactly what Graph.IsTwoConnected.ear_decomposition supplies: the current subgraph B, the ear D as a path of H between two distinct vertices of B, and the freshness of the ear's interior — which is what makes the ear's interior lie in a single current face, since it is connected and disjoint from the current skeleton.

Constructing this step requires a supply of fresh cell names; the existence theorems carry Infinite γ.

Equations

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

def Schoenflies.EarStepConstruction {γ : 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.src srcOuter srcDom H Hdraw) : Prop

The constructive content needed in the nontrivial branch of EarStep: for an ear whose edges are genuinely new, produce the explicit split and its two realized crosscuts. The degenerate branch in which the proposed path was already in B is handled by earStep_of_data.

Equations

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

structure Schoenflies.SourceEarStepData {γ : 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

A realized source ear and its compatibility with the ambient path.

• splitData : T.str.SplitData

  Abstract split introducing the source ear and its two faces.

• srcPos : γ → Plane

  Positions of the new source vertices.

• srcDraw : γ → ℝ → Plane

  Parametrizations of the new source edges.

• srcCrosscut : self.splitData.EarCrosscut T.src self.srcPos self.srcDraw
• srcEdgePolygonal ⦃e : γ⦄ : e ∈ self.splitData.ear.edgeSet → IsPolygonal (Graph.edgeArc self.srcDraw e)
• srcEarSet_eq : self.splitData.earSet self.srcPos self.srcDraw = Graph.edgesCover Hdraw D
• vertexSet_subset : (B.union (H.pathGraphOf a D)).vertexSet ⊆ (CellStructure.SplitData.realize T.src self.splitData self.srcPos self.srcDraw ⋯).graph.vertexSet

theorem Schoenflies.exists_sourceEarStepData {γ : 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.src srcOuter srcDom 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 : γ → γ), IsPartialTransferOf T P B Hdraw par → Nonempty (SourceEarStepData T B H Hdraw a D)

The ambient path is injectively renamed with fresh abstract vertex and edge cells, two more fresh names become the new faces, and the resulting abstract split is realized on the source.

theorem Schoenflies.earStep_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.src srcOuter srcDom H Hdraw) (hbuild : EarStepConstruction P H Hdraw hH) : EarStep P H Hdraw

EarStep, assembled from explicit constructor data. This is the end-to-end bookkeeping theorem: the nontrivial branch is realized by EarStepData.pair; if the proposed ear contains an old edge, Graph.ear_edges_notMem_or_union_eq shows that the union did not change and the current transfer itself is the answer.

Steps 2 and 3: the induction through the ear sequence

theorem Schoenflies.transfer_of_ears_of_commonSubdivision_of_earStep {γ : 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.src srcOuter srcDom H Hdraw) (hsub : CommonSubdivision P H Hdraw) (hstep : EarStep P H Hdraw) : ∃ (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (par : γ → γ), IsPartialTransferOf T P H Hdraw par

Steps 2 and 3 of the proof of thm:finite-transfer. By lem:relative-ear the new finite 2-connected graph is obtained from the old subdivided graph by a finite sequence of ears; each ear insertion is at most two edge subdivisions plus one 2-cell split, so every intermediate stage is a generated matched cell structure. Given step 1 and one ear, the whole extension transfers.

The invariant carried through the induction is IsPartialTransferOf, which does not mention connectedness of the open nonboundary part: rem:intermediate-disconnection says an intermediate stage may genuinely have it disconnected, and nothing here assumes otherwise.

thm:finite-transfer(a)

theorem Schoenflies.finite_transfer_toward_square_of_commonSubdivision_of_earStep {γ : 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.src srcOuter srcDom H Hdraw) (hsub : CommonSubdivision P H Hdraw) (hstep : EarStep P H Hdraw) : ∃ (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (par : γ → γ), IsTransferOf T P H Hdraw par

thm:finite-transfer, direction (a): transfer toward the square.

Let (Γ, Γ') be a generated matched cellulation. Suppose H is a finite 2-connected plane graph containing a subdivision of Γ, with outer cycle C, with every nonboundary edge polygonal, and with |H| ∖ C connected. Then the common subdivision can be made on Γ', and H can be transferred to an admissible target realization H'; the resulting generated matched cellulation refines the old one by an explicit parent map.

This compatibility form accepts both step interfaces as arguments. earStep discharges the second, while commonSubdivision in CommonSubdivision.lean discharges the first.

Step 4, direction (a): the target crosscut

In part (a), F* is a polygonal Jordan region in the square, by lem:cellulation-invariants(vii). Every point of its boundary is polygonally accessible from its interior. lem:accessible-endpoints therefore gives a polygonal crosscut P* ⊆ closure F* from v* to w*. Then: thm:general-crosscut says that the crosscut splits the face into exactly the two Jordan regions bounded by the crosscut together with those two paths.

That whole paragraph is proved below. It is stated for a target face — a member of a family of components of Q ∖ |G| for an ambient open region Q whose frontier belongs to the skeleton — because that is the shape Graph.polygonal_side_accessibility_target consumes, and it is the shape a target realization of a generated structure has: Q is the open square, |G| the target skeleton, and the family is the set of realized open 2-cells.

theorem Schoenflies.isOpen_isPreconnected_disjoint_of_target_cell {β : Type u_2} {G : Graph Plane β} {drawing : β → ℝ → Plane} {Q F : Set Plane} {cells : Set (Set Plane)} [G.Finite] (h : G.IsDrawing drawing) (hQ : IsOpen Q) (hcell : ∀ R ∈ cells, R ⊆ Q ∧ ∃ (z : Plane), R = connectedComponentIn (Q \ G.pointSet drawing) z) (hF : F ∈ cells) : IsOpen F ∧ IsPreconnected F ∧ Disjoint F (G.pointSet drawing)

A target 2-cell is an open connected set disjoint from the skeleton. Everything the crosscut construction needs about it, read off the presentation as a component of Q ∖ |G|.

theorem Schoenflies.exists_target_crosscut {β : Type u_2} {G : Graph Plane β} {drawing : β → ℝ → Plane} {Q F J : Set Plane} {cells : Set (Set Plane)} {v w : Plane} [G.Finite] (h : G.IsDrawing drawing) (hpoly : ∀ e ∈ G.edgeSet, IsPolygonal (Graph.edgeArc drawing e)) (hQ : IsOpen Q) (hQK : frontier Q ⊆ G.pointSet drawing) (hcell : ∀ R ∈ cells, R ⊆ Q ∧ ∃ (z : Plane), R = connectedComponentIn (Q \ G.pointSet drawing) z) (hF : F ∈ cells) (hJ : J ⊆ G.pointSet drawing) (hvw : v ≠ w) (hvJ : v ∈ J) (hwJ : w ∈ J) (hv : v ∈ closure F) (hw : w ∈ closure F) : ∃ (P : Set Plane), IsPolygonal P ∧ IsArcBetween P v w ∧ P \ {v, w} ⊆ F ∧ P ∩ J = {v, w}

The target crosscut of thm:finite-transfer(a), step 4. Two distinct points of a curve J inside the target skeleton, both in the closure of a target 2-cell F, are joined by a simple polygonal arc lying in F apart from its two endpoints and meeting J exactly there.

The three inputs are the three the blueprint names: lem:polygonal-side-accessibility on the target side for the accessibility of each endpoint, and lem:accessible-endpoints in its crosscut form for the join. Nothing is assumed.

theorem Schoenflies.exists_target_crosscut_split {β : Type u_2} {G : Graph Plane β} {drawing : β → ℝ → Plane} {Q F J A₁ A₂ : Set Plane} {cells : Set (Set Plane)} {v w : Plane} [G.Finite] (h : G.IsDrawing drawing) (hpoly : ∀ e ∈ G.edgeSet, IsPolygonal (Graph.edgeArc drawing e)) (hQ : IsOpen Q) (hQK : frontier Q ⊆ G.pointSet drawing) (hcell : ∀ R ∈ cells, R ⊆ Q ∧ ∃ (z : Plane), R = connectedComponentIn (Q \ G.pointSet drawing) z) (hF : F ∈ cells) (hJ : J ⊆ G.pointSet drawing) (hJc : IsJordanCurve J) (hFJ : F = inside J) (hvw : v ≠ w) (hvJ : v ∈ J) (hwJ : w ∈ J) (hv : v ∈ closure F) (hw : w ∈ closure F) (hcut : IsCutPair J v w A₁ A₂) : ∃ (P : Set Plane), IsPolygonal P ∧ IsArcBetween P v w ∧ P \ {v, w} ⊆ F ∧ P ∩ J = {v, w} ∧ IsCrosscut J P v w ∧ F = inside (A₁ ∪ P) ∪ inside (A₂ ∪ P) ∪ P \ {v, w} ∧ Disjoint (inside (A₁ ∪ P)) (inside (A₂ ∪ P)) ∧ Disjoint (inside (A₁ ∪ P)) (P \ {v, w}) ∧ Disjoint (inside (A₂ ∪ P)) (P \ {v, w}) ∧ IsOpen (inside (A₁ ∪ P)) ∧ IsOpen (inside (A₂ ∪ P)) ∧ (inside (A₁ ∪ P)).Nonempty ∧ (inside (A₂ ∪ P)).Nonempty ∧ closure (inside (A₁ ∪ P)) = inside (A₁ ∪ P) ∪ (A₁ ∪ P) ∧ closure (inside (A₂ ∪ P)) = inside (A₂ ∪ P) ∪ (A₂ ∪ P)

Step 4 in full: the target crosscut splits the target face into exactly two Jordan regions. By lem:cellulation-invariants(vii) the target 2-cell F is the bounded complementary region of the Jordan curve J realizing its boundary walk; the crosscut of Schoenflies.exists_target_crosscut is then a crosscut of J in the sense of thm:general-crosscut, which decomposes F into the two Jordan regions bounded by the crosscut together with the two boundary paths.

The conclusion is returned in the shape assertion (i) consumes at a 2-cell split (Schoenflies.crosscut_cell_partition): the old open 2-cell is the disjoint union of the two new open 2-cells and the open crosscut, each new 2-cell is open and nonempty, and the closure of each is that open 2-cell together with its own boundary curve.

theorem Schoenflies.GeneratedPair.exists_target_crosscut {γ : Type u_1} {S₀ : CellStructure γ} {srcOuter srcDom tgtOuter tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) {u v F : γ} (hu : u ∈ P.str.skel.vertexSet) (hv : v ∈ P.str.skel.vertexSet) (huv : u ≠ v) (hF : F ∈ P.str.faces) (huF : P.str.sub u F) (hvF : P.str.sub v F) : ∃ (A : Set Plane), IsPolygonal A ∧ IsArcBetween A (P.tgt.pos u) (P.tgt.pos v) ∧ A \ {P.tgt.pos u, P.tgt.pos v} ⊆ P.tgt.cell F ∧ A ∩ frontier (P.tgt.cell F) = {P.tgt.pos u, P.tgt.pos v}

A face and two distinct boundary vertices of a generated pair admit the target polygonal crosscut needed by an ear insertion. All accessibility hypotheses are discharged from the fields maintained by GeneratedPair.

Completing the ear step

theorem Schoenflies.earStepConstruction {γ : 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.src srcOuter srcDom H Hdraw) : EarStepConstruction P H Hdraw hH

The constructive ear interface. The source half is the freshly renamed path supplied by exists_sourceEarStepData; the target half is a polygonal crosscut of the corresponding face, divided edge-for-edge by EarCrosscut.exists_matched_target.

theorem Schoenflies.earStep {γ : 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.src srcOuter srcDom H Hdraw) : EarStep P H Hdraw

One ear insertion, with no remaining hypothesis.

theorem Schoenflies.transfer_of_ears_of_commonSubdivision {γ : 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.src srcOuter srcDom H Hdraw) (hsub : CommonSubdivision P H Hdraw) : ∃ (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (par : γ → γ), IsPartialTransferOf T P H Hdraw par

Steps 2 and 3 of finite transfer, parametrized by the step-1 interface.

theorem Schoenflies.finite_transfer_toward_square_of_commonSubdivision {γ : 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.src srcOuter srcDom H Hdraw) (hsub : CommonSubdivision P H Hdraw) : ∃ (T : GeneratedPair S₀ srcOuter srcDom tgtOuter tgtDom) (par : γ → γ), IsTransferOf T P H Hdraw par

Finite transfer toward the square from an explicitly supplied common subdivision.

The ear's endpoints, transferred

Let F*, v*, w* be the corresponding face and endpoints in the other realization. Under the representation of Schoenflies/CombinatorialInvariance.lean there is nothing to transport: F and the two endpoint 0-cells are cells of the one abstract structure both realizations realize, and assertion (ix) turns "the source endpoint lies on the boundary of the source face" into the abstract statement a ≼ F, which reads back in the target realization.

theorem Schoenflies.CellStructure.Realization.pos_mem_closure_cell_congr {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} {D₁ D₂ : Set Plane} {a F : γ} (h₁ : R₁.IsCellDecomposition D₁) (h₂ : R₂.IsCellDecomposition D₂) (ha : a ∈ S.skel.vertexSet) (hF : F ∈ S.faces) (hmem : R₁.pos a ∈ closure (R₁.cell F)) : R₂.pos a ∈ closure (R₂.cell F)

The endpoints of the ear transfer to the other realization. A 0-cell on the boundary of a 2-cell in one realization is on the boundary of the same 2-cell in the other.

theorem Schoenflies.exists_target_ear {γ : Type u_1} {S : CellStructure γ} {R₁ R₂ : S.Realization} {D₁ D₂ Q J A₁ A₂ : Set Plane} {a b F : γ} (h₁ : R₁.IsCellDecomposition D₁) (h₂ : R₂.IsCellDecomposition D₂) (hpoly : ∀ ⦃e : γ⦄, e ∈ S.skel.edgeSet → IsPolygonal (Graph.edgeArc R₂.drawing e)) (hQ : IsOpen Q) (hQK : frontier Q ⊆ R₂.skeletonSet) (hcell : ∀ T ∈ S.faces, R₂.cell T ⊆ Q ∧ ∃ (z : Plane), R₂.cell T = connectedComponentIn (Q \ R₂.skeletonSet) z) (hF : F ∈ S.faces) (hJ : J ⊆ R₂.skeletonSet) (hJc : IsJordanCurve J) (hFJ : R₂.cell F = inside J) (ha : a ∈ S.skel.vertexSet) (hb : b ∈ S.skel.vertexSet) (hab : R₂.pos a ≠ R₂.pos b) (haJ : R₂.pos a ∈ J) (hbJ : R₂.pos b ∈ J) (hacl : R₁.pos a ∈ closure (R₁.cell F)) (hbcl : R₁.pos b ∈ closure (R₁.cell F)) (hcut : IsCutPair J (R₂.pos a) (R₂.pos b) A₁ A₂) : ∃ (P : Set Plane), IsPolygonal P ∧ IsArcBetween P (R₂.pos a) (R₂.pos b) ∧ P \ {R₂.pos a, R₂.pos b} ⊆ R₂.cell F ∧ P ∩ J = {R₂.pos a, R₂.pos b} ∧ IsCrosscut J P (R₂.pos a) (R₂.pos b) ∧ R₂.cell F = inside (A₁ ∪ P) ∪ inside (A₂ ∪ P) ∪ P \ {R₂.pos a, R₂.pos b} ∧ Disjoint (inside (A₁ ∪ P)) (inside (A₂ ∪ P)) ∧ Disjoint (inside (A₁ ∪ P)) (P \ {R₂.pos a, R₂.pos b}) ∧ Disjoint (inside (A₂ ∪ P)) (P \ {R₂.pos a, R₂.pos b}) ∧ IsOpen (inside (A₁ ∪ P)) ∧ IsOpen (inside (A₂ ∪ P)) ∧ (inside (A₁ ∪ P)).Nonempty ∧ (inside (A₂ ∪ P)).Nonempty ∧ closure (inside (A₁ ∪ P)) = inside (A₁ ∪ P) ∪ (A₁ ∪ P) ∧ closure (inside (A₂ ∪ P)) = inside (A₂ ∪ P) ∪ (A₂ ∪ P)

The geometric half of one ear insertion, direction (a).

The source ear lies in a current source 2-cell F and its two endpoints are 0-cells on the boundary of F (hacl, hbcl). The target realization of F is a polygonal Jordan region in the open square Q (hFJ — assertion (vii)) whose 2-cells are the components of Q ∖ |Γ'| (hcell — assertion (i) on the target side). Then the corresponding target endpoints are joined by a polygonal crosscut inside the closure of the target face, which splits that face into exactly the two Jordan regions bounded by the crosscut and the two boundary paths.

This is the fourth paragraph of the blueprint's proof of thm:finite-transfer(a), assembled; what is left of the induction step is the abstract-data bookkeeping around it.

Step 1: the overlay

By lem:polygonal-overlay, using the convention of rem:polygonal-overlay-convention, first overlay the proposed polygonal nonboundary edges with the old polygonal nonboundary skeleton and subdivide at all intersections.

Schoenflies.polygonal_overlay does that for a list of segments. What step 1 has instead is a finite family of polygonal arcs — the old nonboundary edges and the proposed new ones — so the two have to be bridged. Schoenflies.exists_overlay_of_biUnion_finite is that bridge, and it is the half of step 1 that is proved here: the union of finitely many nondegenerate polygonal sets is the point set of a finite plane graph drawn by straight segments, whose vertices are the ends of the subdivided pieces and therefore include every intersection point.

The nondegeneracy hypothesis is necessary, not cosmetic: a one-point set is polygonal (poly [a] = {a}) and is not the point set of any overlay graph, whose vertices are the ends of nondegenerate segments.

The matching-subdivision half of step 1 is completed in CommonSubdivision.lean: every source subdivision point is transported through the chosen edge parametrization to the other realization.

theorem Schoenflies.exists_overlay_of_biUnion_finite {ι : Type u_2} {s : Set ι} {A : ι → Set Plane} (hs : s.Finite) (hA : ∀ i ∈ s, IsPolygonal (A i)) (hnd : ∀ i ∈ s, ∃ a ∈ A i, ∃ b ∈ A i, a ≠ b) : ∃ (G : Graph Plane Piece), G.Finite ∧ G.IsDrawing segmentDrawing ∧ G.pointSet segmentDrawing = ⋃ i ∈ s, A i

lem:polygonal-overlay for a finite family of polygonal sets. The union of finitely many nondegenerate polygonal sets is the point set of a finite plane graph whose edges are straight segments — the overlay, subdivided at every intersection.

This is the first half of step 1 of the proof of thm:finite-transfer.

The interface, exercised

thm:finite-transfer exists to feed the recursion of the quantitative-refinement section, which consumes a transfer only through Realization.Refines. This anonymous example is a machine-checked statement that the conclusion of finite_transfer_toward_square delivers exactly what that recursion reads: the source carrier refines (lem:refinement-compatibility(a)), the same parent map serves both sides (part (c)), and the closed target star of a fixed source point shrinks (T_{n+1}(x) \subseteq T_n(x)).

Nothing below mentions how the transfer was built. If a later change to IsTransferOf stopped serving that recursion, this would break.