Reverse square-mesh transfer over the initial cell-name type

The concrete square mesh uses segments (Piece) as edge names, whereas every generated pair over the initial hexagon uses InitialCell. Only the finitely many mesh edges matter, so they can be injectively renamed into the spare InitialCell.aux supply while avoiding every current cell name. Edge relabelling preserves the ambient boundary geometry used by reverse transfer.

Blueprint

• Schoenflies.exists_initialCell_squareMesh_edgeRelabeling — choose fresh InitialCell names for all edges of one finite square mesh.
• Schoenflies.finite_transfer_toward_source_initial_relabelledSquareMesh — direction (b) for the relabelled mesh, with the initial outer-cycle base case discharged.
• Schoenflies.exists_finite_transfer_toward_source_initial_squareMesh — the bare-square-mesh specialization: choose the fresh names, assemble the extension from the three explicit subdivision hypotheses, and run reverse transfer.

theorem Schoenflies.exists_initialCell_squareMesh_edgeRelabeling {srcOuter srcDom tgtDom : Set Plane} (P : GeneratedPair initialStructure srcOuter srcDom modelCurve tgtDom) (delta : ℝ) (fresh anchors : List Plane) : ∃ (name : Piece → InitialCell), Set.InjOn name (squareMesh delta fresh anchors).edgeSet ∧ ∀ e ∈ (squareMesh delta fresh anchors).edgeSet, name e ∉ P.str.cells

Every finite square mesh can be renamed into currently unused InitialCell names.

theorem Schoenflies.finite_transfer_toward_source_initial_relabelledSquareMesh {srcOuter srcDom tgtDom : Set Plane} (P : GeneratedPair initialStructure srcOuter srcDom modelCurve tgtDom) {fresh anchors : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (hstrong : ∀ z ∈ fresh, StronglyAccessible (srcDom \ srcOuter) (P.homeo.invFun z)) (delta : ℝ) (name : Piece → InitialCell) (hname : Set.InjOn name (squareMesh delta fresh anchors).edgeSet) (hH : IsSourceExtension P.tgt modelCurve tgtDom ((squareMesh delta fresh anchors).relabelEdges name hname) ((squareMesh delta fresh anchors).relabelDrawing name segmentDrawing)) : ∃ (T : GeneratedPair initialStructure srcOuter srcDom modelCurve tgtDom) (par : InitialCell → InitialCell), IsTargetTransferOf T P ((squareMesh delta fresh anchors).relabelEdges name hname) ((squareMesh delta fresh anchors).relabelDrawing name segmentDrawing) par

Finite transfer, direction (b), over the concrete initial naming type. Once the stage constructor supplies the relabelled square mesh as a target extension, the reverse transfer is available directly: boundary anchoring, boundary-edge uniqueness, and the initial outer cycle are all discharged here.

theorem Schoenflies.exists_finite_transfer_toward_source_initial_squareMesh {srcOuter srcDom : Set Plane} (P : GeneratedPair initialStructure srcOuter srcDom modelCurve (Plane.closedSquare 0 1)) {fresh anchors : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (hstrong : ∀ z ∈ fresh, StronglyAccessible (srcDom \ srcOuter) (P.homeo.invFun z)) {delta : ℝ} (hdense : FreshDense fresh delta) (hdelta : delta < 4) (hvertices : P.tgt.graph.vertexSet ⊆ (squareMesh delta fresh anchors).vertexSet) (hskeleton : P.tgt.skeletonSet ⊆ (squareMesh delta fresh anchors).pointSet segmentDrawing) (hedge : ∀ ⦃e : InitialCell⦄, e ∈ P.str.skel.edgeSet → ∀ ⦃f : Piece⦄, f ∈ (squareMesh delta fresh anchors).edgeSet → (Graph.edgeArc segmentDrawing f ∩ (P.tgt.cell e \ (squareMesh delta fresh anchors).vertexSet)).Nonempty → Graph.edgeArc segmentDrawing f ⊆ Graph.edgeArc P.tgt.drawing e) : ∃ (name : Piece → InitialCell) (hname : Set.InjOn name (squareMesh delta fresh anchors).edgeSet) (T : GeneratedPair initialStructure srcOuter srcDom modelCurve (Plane.closedSquare 0 1)) (par : InitialCell → InitialCell), IsTargetTransferOf T P ((squareMesh delta fresh anchors).relabelEdges name hname) ((squareMesh delta fresh anchors).relabelDrawing name segmentDrawing) par

Reverse transfer specialized to a bare square mesh. Fresh abstract edge names are chosen automatically. The square-mesh theorems discharge finiteness, drawing, 2-connectivity, domain containment, boundary-edge geometry, and connectedness off the model curve. The three remaining hypotheses assert that this particular mesh subdivides the current target skeleton; they need not hold for an arbitrary current polygonal skeleton, whose stage construction uses the combined overlay in Schoenflies.TargetOverlay.