Anchored square meshes supply the boundary anchors for reverse finite transfer

Schoenflies.TargetBoundaryAnchored is the fixed geometric input isolated from finite-transfer direction (b): every nonouter target edge ending on the model curve must end at the image of a strongly accessible source anchor.

The anchored square mesh was built to have exactly this property. Its clause 4, Schoenflies.squareMesh_inner_edge_at_fresh, says that every mesh edge which meets the model curve without lying in it meets the curve at one of the prescribed fresh points. Thus, if the fresh list consists of target images of strongly accessible source anchors, the whole boundary condition follows with no ear-order argument.

Blueprint

• Schoenflies.targetBoundaryAnchored_squareMesh — anchored-square-mesh clause 4 discharges the strong-accessibility input of reverse finite transfer.
• Schoenflies.targetEarFreshCombinatorics_squareMesh_of_outerIncidenceAtMostTwo — mesh uniqueness and the local two-branch property of the generated outer cycle discharge the evolving fresh-incidence input.
• Schoenflies.targetEarFreshCombinatorics_squareMesh_of_outerCycle — the preceding local property follows from one simple-cycle check on the base structure.
• Schoenflies.isSourceExtension_relabelledSquareMesh_closedSquare — edge relabelling and all fixed mesh clauses reduce the extension interface to the three actual subdivision statements.
• Schoenflies.finite_transfer_toward_source_relabelledSquareMesh_of_outerCycle — reverse transfer over any infinite abstract cell-name type.
• Schoenflies.finite_transfer_toward_source_squareMesh — direction (b) for an anchored square mesh, reduced only to the evolving fresh-incidence combinatorics.
• Schoenflies.finite_transfer_toward_source_squareMesh_of_outerIncidenceAtMostTwo — the same conclusion reduced to propagation of one static outer-cycle invariant.

theorem Schoenflies.squareMesh_nonouter_incident_eq {fresh anchors : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (delta : ℝ) {z : Plane} (hz : z ∈ modelCurve) {P Q : Piece} (hP : P ∈ (squareMesh delta fresh anchors).edgeSet) (hQ : Q ∈ (squareMesh delta fresh anchors).edgeSet) (hPinc : (squareMesh delta fresh anchors).Inc P z) (hQinc : (squareMesh delta fresh anchors).Inc Q z) (hPnot : ¬Graph.edgeArc segmentDrawing P ⊆ modelCurve) (hQnot : ¬Graph.edgeArc segmentDrawing Q ⊆ modelCurve) : P = Q

At a point of the model curve, two nonouter square-mesh edges cannot both be incident. Clause 4 first recognizes the point as fresh from either edge, then its uniqueness half identifies the two pieces.

theorem Schoenflies.nonouterIncidenceUniqueAtBoundary_squareMesh {fresh anchors : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (delta : ℝ) : NonouterIncidenceUniqueAtBoundary (squareMesh delta fresh anchors) segmentDrawing modelCurve

The name-independent form of square-mesh clause 4: at a point of the model curve there is at most one incident mesh edge which is not contained in the curve.

theorem Schoenflies.exists_finiteGraph_edgeRelabeling_avoiding {β : Type u_1} (γ : Type u_2) [Infinite γ] (H : Graph Plane β) [H.Finite] (used : Set γ) (hused : used.Finite) : ∃ (name : β → γ), Set.InjOn name H.edgeSet ∧ ∀ e ∈ H.edgeSet, name e ∉ used

The edges of any finite graph can be injectively renamed into an infinite type while avoiding a prescribed finite set of names.

theorem Schoenflies.exists_squareMesh_edgeRelabeling_avoiding (γ : Type u_1) [Infinite γ] (delta : ℝ) (fresh anchors : List Plane) (used : Set γ) (hused : used.Finite) : ∃ (name : Piece → γ), Set.InjOn name (squareMesh delta fresh anchors).edgeSet ∧ ∀ e ∈ (squareMesh delta fresh anchors).edgeSet, name e ∉ used

A finite square mesh can have all of its edges injectively renamed into any infinite cell name type, avoiding any prescribed finite set of names.

theorem Schoenflies.squareMesh_relabelEdges_finite {γ : Type u_1} (delta : ℝ) (fresh anchors : List Plane) (name : Piece → γ) (hname : Set.InjOn name (squareMesh delta fresh anchors).edgeSet) : ((squareMesh delta fresh anchors).relabelEdges name hname).Finite

A relabelled square mesh is finite.

theorem Schoenflies.squareMesh_relabelEdges_isDrawing {γ : Type u_1} {fresh anchors : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (delta : ℝ) (name : Piece → γ) (hname : Set.InjOn name (squareMesh delta fresh anchors).edgeSet) : ((squareMesh delta fresh anchors).relabelEdges name hname).IsDrawing ((squareMesh delta fresh anchors).relabelDrawing name segmentDrawing)

The straight-line square-mesh drawing transports to the new edge names.

theorem Schoenflies.squareMesh_pointSet_relabelEdges {γ : Type u_1} (delta : ℝ) (fresh anchors : List Plane) (name : Piece → γ) (hname : Set.InjOn name (squareMesh delta fresh anchors).edgeSet) : ((squareMesh delta fresh anchors).relabelEdges name hname).pointSet ((squareMesh delta fresh anchors).relabelDrawing name segmentDrawing) = (squareMesh delta fresh anchors).pointSet segmentDrawing

Relabelling does not change the geometric carrier of the square mesh.

theorem Schoenflies.squareMesh_relabelEdges_isTwoConnected {γ : Type u_1} {fresh anchors : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) {delta : ℝ} (hdense : FreshDense fresh delta) (hdelta : delta < 4) (name : Piece → γ) (hname : Set.InjOn name (squareMesh delta fresh anchors).edgeSet) : ((squareMesh delta fresh anchors).relabelEdges name hname).IsTwoConnected

The relabelled mesh remains 2-connected under the same density hypotheses.

theorem Schoenflies.squareMesh_edge_dichotomy {fresh anchors : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (delta : ℝ) {dom : Set Plane} (hpointSet : (squareMesh delta fresh anchors).pointSet segmentDrawing ⊆ dom) ⦃f : Piece⦄ : f ∈ (squareMesh delta fresh anchors).edgeSet → Graph.edgeArc segmentDrawing f ⊆ modelCurve ∨ IsPolygonal (Graph.edgeArc segmentDrawing f) ∧ Graph.edgeArc segmentDrawing f \ (squareMesh delta fresh anchors).vertexSet ⊆ dom \ modelCurve

Every square-mesh edge is either contained in the model curve or is a polygonal edge whose nonvertex points avoid that curve. A nonouter edge can meet the curve only at its unique fresh endpoint, and that endpoint is a graph vertex.

theorem Schoenflies.isSourceExtension_relabelledSquareMesh {γ : Type u_1} {Sbase : CellStructure γ} {srcOuter srcDom tgtDom : Set Plane} (P : GeneratedPair Sbase srcOuter srcDom modelCurve tgtDom) {fresh anchors : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) {delta : ℝ} (hdense : FreshDense fresh delta) (hdelta : delta < 4) (name : Piece → γ) (hname : Set.InjOn name (squareMesh delta fresh anchors).edgeSet) (hvertices : P.tgt.graph.vertexSet ⊆ (squareMesh delta fresh anchors).vertexSet) (hskeleton : P.tgt.skeletonSet ⊆ (squareMesh delta fresh anchors).pointSet segmentDrawing) (hedge : ∀ ⦃e : γ⦄, 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) (hpointSet : (squareMesh delta fresh anchors).pointSet segmentDrawing ⊆ tgtDom) (hdichotomy : ∀ ⦃f : Piece⦄, f ∈ (squareMesh delta fresh anchors).edgeSet → Graph.edgeArc segmentDrawing f ⊆ modelCurve ∨ IsPolygonal (Graph.edgeArc segmentDrawing f) ∧ Graph.edgeArc segmentDrawing f \ (squareMesh delta fresh anchors).vertexSet ⊆ tgtDom \ modelCurve) (hconnected : IsConnected ((squareMesh delta fresh anchors).pointSet segmentDrawing \ modelCurve)) : IsSourceExtension P.tgt modelCurve tgtDom ((squareMesh delta fresh anchors).relabelEdges name hname) ((squareMesh delta fresh anchors).relabelDrawing name segmentDrawing)

Assemble the relabelled square mesh as a target extension from hypotheses stated entirely against the original Piece-named mesh. Finiteness, planarity, 2-connectivity, and every geometric carrier equality are transported automatically.

theorem Schoenflies.isSourceExtension_relabelledSquareMesh_closedSquare {γ : Type u_1} {Sbase : CellStructure γ} {srcOuter srcDom : Set Plane} (P : GeneratedPair Sbase srcOuter srcDom modelCurve (Plane.closedSquare 0 1)) {fresh anchors : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) {delta : ℝ} (hdense : FreshDense fresh delta) (hdelta : delta < 4) (name : Piece → γ) (hname : Set.InjOn name (squareMesh delta fresh anchors).edgeSet) (hvertices : P.tgt.graph.vertexSet ⊆ (squareMesh delta fresh anchors).vertexSet) (hskeleton : P.tgt.skeletonSet ⊆ (squareMesh delta fresh anchors).pointSet segmentDrawing) (hedge : ∀ ⦃e : γ⦄, 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) : IsSourceExtension P.tgt modelCurve (Plane.closedSquare 0 1) ((squareMesh delta fresh anchors).relabelEdges name hname) ((squareMesh delta fresh anchors).relabelDrawing name segmentDrawing)

For the model closed square, the square-mesh construction itself supplies the domain containment, edge dichotomy, connected complement, planarity, and 2-connectivity. A caller only has to say that the current target skeleton is subdivided by the mesh.

theorem Schoenflies.targetBoundaryAnchored_squareMesh {srcOuter srcDom tgtDom : Set Plane} {γ : Type u_1} {Sbase : CellStructure γ} (P : GeneratedPair Sbase srcOuter srcDom modelCurve tgtDom) {fresh anchors : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (hstrong : ∀ z ∈ fresh, StronglyAccessible (srcDom \ srcOuter) (P.homeo.invFun z)) (delta : ℝ) : TargetBoundaryAnchored P (squareMesh delta fresh anchors) segmentDrawing

An anchored square mesh satisfies the fixed boundary-anchor condition for reverse finite transfer. The only hypothesis beyond membership in the model curve is the one the stage constructor records: every prescribed fresh target point pulls back to a strongly accessible source anchor.

theorem Schoenflies.targetEarEndpointsOuterOnly_squareMesh {S₀ : CellStructure Piece} {srcOuter srcDom tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom modelCurve tgtDom) {fresh anchors : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (delta : ℝ) (hH : IsSourceExtension P.tgt modelCurve tgtDom (squareMesh delta fresh anchors) segmentDrawing) {B : Graph Plane Piece} {a b : Plane} {D : List Piece} {par : Piece → Piece} (hBH : B ≤ squareMesh delta fresh anchors) (hpath : (squareMesh delta fresh anchors).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 modelCurve tgtDom} (hT : IsTargetPartialTransferOf T P B segmentDrawing par) (w : TargetSideEarStepData T B (squareMesh delta fresh anchors) segmentDrawing 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)

A wild-boundary endpoint of the next square-mesh ear is outer-only in the current abstract skeleton. If a current nonouter abstract edge reached it, local carrier reflection would produce a current ambient nonouter edge there. Clause 4 identifies that edge with the new ear edge, contradicting that every edge of the ear is absent from the current graph.

theorem Schoenflies.targetEarFreshCombinatorics_squareMesh_of_outerIncidenceAtMostTwo {S₀ : CellStructure Piece} {srcOuter srcDom tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom modelCurve tgtDom) {fresh anchors : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (delta : ℝ) (hH : IsSourceExtension P.tgt modelCurve tgtDom (squareMesh delta fresh anchors) segmentDrawing) (htwo : ∀ (S : CellStructure Piece), GeneratedStructure S₀ S → S.OuterIncidenceAtMostTwoEverywhere) : TargetEarFreshCombinatorics P (squareMesh delta fresh anchors) segmentDrawing

For a square mesh, the reverse-ear fresh-incidence invariant follows from the static fact that every generated outer graph is locally at most two-branched. Clause 4 makes each new wild-boundary endpoint outer-only; the local two-branch bound then makes its selected face the unique incident face.

theorem Schoenflies.targetEarFreshCombinatorics_squareMesh_of_outerCycle {S₀ : CellStructure Piece} {srcOuter srcDom tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom modelCurve tgtDom) {fresh anchors : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (delta : ℝ) (hH : IsSourceExtension P.tgt modelCurve tgtDom (squareMesh delta fresh anchors) segmentDrawing) (hcycle : S₀.OuterEdgesFormCycle) : TargetEarFreshCombinatorics P (squareMesh delta fresh anchors) segmentDrawing

It is enough to verify once, on the base cell structure, that the distinguished outer edges form a simple cycle. The two generated-structure constructors preserve that fact.

theorem Schoenflies.finite_transfer_toward_source_squareMesh {S₀ : CellStructure Piece} {srcOuter srcDom tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom modelCurve tgtDom) {fresh anchors : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (hstrong : ∀ z ∈ fresh, StronglyAccessible (srcDom \ srcOuter) (P.homeo.invFun z)) (delta : ℝ) (hH : IsSourceExtension P.tgt modelCurve tgtDom (squareMesh delta fresh anchors) segmentDrawing) (hcomb : TargetEarFreshCombinatorics P (squareMesh delta fresh anchors) segmentDrawing) : ∃ (T : GeneratedPair S₀ srcOuter srcDom modelCurve tgtDom) (par : Piece → Piece), IsTargetTransferOf T P (squareMesh delta fresh anchors) segmentDrawing par

Reverse finite transfer for an anchored square mesh. Strong accessibility is completely discharged from the mesh's fresh-point clause; only carrier freshness and unique current-face incidence remain for the prescribed ear order.

theorem Schoenflies.finite_transfer_toward_source_squareMesh_of_outerIncidenceAtMostTwo {S₀ : CellStructure Piece} {srcOuter srcDom tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom modelCurve tgtDom) {fresh anchors : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (hstrong : ∀ z ∈ fresh, StronglyAccessible (srcDom \ srcOuter) (P.homeo.invFun z)) (delta : ℝ) (hH : IsSourceExtension P.tgt modelCurve tgtDom (squareMesh delta fresh anchors) segmentDrawing) (htwo : ∀ (S : CellStructure Piece), GeneratedStructure S₀ S → S.OuterIncidenceAtMostTwoEverywhere) : ∃ (T : GeneratedPair S₀ srcOuter srcDom modelCurve tgtDom) (par : Piece → Piece), IsTargetTransferOf T P (squareMesh delta fresh anchors) segmentDrawing par

Reverse finite transfer for an anchored square mesh, reduced to a supplied propagation of the static local outer-cycle invariant.

theorem Schoenflies.finite_transfer_toward_source_squareMesh_of_outerCycle {S₀ : CellStructure Piece} {srcOuter srcDom tgtDom : Set Plane} (P : GeneratedPair S₀ srcOuter srcDom modelCurve tgtDom) {fresh anchors : List Plane} (hfresh : ∀ z ∈ fresh, z ∈ modelCurve) (hstrong : ∀ z ∈ fresh, StronglyAccessible (srcDom \ srcOuter) (P.homeo.invFun z)) (delta : ℝ) (hH : IsSourceExtension P.tgt modelCurve tgtDom (squareMesh delta fresh anchors) segmentDrawing) (hcycle : S₀.OuterEdgesFormCycle) : ∃ (T : GeneratedPair S₀ srcOuter srcDom modelCurve tgtDom) (par : Piece → Piece), IsTargetTransferOf T P (squareMesh delta fresh anchors) segmentDrawing par

Reverse finite transfer for an anchored square mesh from the natural base invariant: its distinguished outer edges form a simple cycle.

theorem Schoenflies.finite_transfer_toward_source_relabelledSquareMesh_of_outerCycle {srcOuter srcDom tgtDom : Set Plane} {γ : Type u_1} [Infinite γ] {Sbase : CellStructure γ} (P : GeneratedPair Sbase 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 → γ) (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)) (hcycle : Sbase.OuterEdgesFormCycle) : ∃ (T : GeneratedPair Sbase srcOuter srcDom modelCurve tgtDom) (par : γ → γ), IsTargetTransferOf T P ((squareMesh delta fresh anchors).relabelEdges name hname) ((squareMesh delta fresh anchors).relabelDrawing name segmentDrawing) par

Reverse finite transfer for a square mesh whose finitely many Piece edge labels have been injectively renamed into the abstract cell-name type. This is the integration form used by the InitialCell-named initial pair.