The complete construction of prop:initial-pair

Schoenflies/InitialPair.lean builds the initial matched pair but leaves three things that def:matched-pair and prop:initial-pair actually assert:

1. the anchor clause. The blueprint chooses a, b ∈ 𝒜, the fixed countable dense set of strongly accessible points of prop:countable-strong-access (tex 1403–1418). InitialData records neither the anchor set nor the strong accessibility of a and b, so nothing downstream can build a further crosscut ending at them, and lem:anchor-density — which needs the anchors of every stage to be points of 𝒜 — has nothing to attach to. Schoenflies.AnchorSet is 𝒜 as data, Schoenflies.AnchoredInitialData is the initial pair with the clause recorded, and Schoenflies.AnchoredInitialData.stronglyAccessible_a / .exists_access_segment_a turn it back into the straight access segment lem:tangent-cone supplies.
2. the matched labelling. InitialData.source_closure_cell_inter labels the two source 2-cells by the two boundary arcs A₁, A₂ of C, and .target_closure_cell_inter labels the two target 2-cells by the two boundary arcs of S — independently. Nothing said the two labellings correspond, which is the whole content of a matched pair. Schoenflies.InitialData.tgt_arcOf_eq_image (tgt.arcOf k = u '' src.arcOf k), .skeletonHomeo_image_arcOf and .closure_cell_face_link supply the link.
3. def:admissible-graph for the target: "all its edges are polygonal". Schoenflies.InitialData.isPolygonal_tgt_edgeArc and .isPolygonal_targetRealization_skeletonSet.

It also carried two hypotheses, harc (thm:arc-complement) and hcollars (lem:crosscut-collars), both of which are now theorems on main (Schoenflies.arc_complement, Schoenflies.IsCrosscut.hasArcCollars). Every headline result is restated here after supplying them; the primed names distinguish these strengthened statements.

Finally, initBoundary is a raw datum in CellStructure, and nothing checked that the two lists it holds are closed walks of initSkel whose cells are exactly faceCells. They are: Schoenflies.isWalk_initBoundary_false, .._true, and Schoenflies.mem_faceCells_iff.

Blueprint

• Schoenflies.AnchorSet, Schoenflies.nonempty_anchorSet, Schoenflies.anchorSet — prop:countable-strong-access as the fixed set 𝒜 of tex 1418.
• Schoenflies.AnchoredInitialData, Schoenflies.exists_anchoredInitialData, Schoenflies.anchoredInitialData, Schoenflies.initialData — prop:initial-pair including the dropped clause "two further points a, b ∈ 𝒜", the last one with the canonical anchor set supplied.
• Schoenflies.stronglyAccessible_initialData_a, .._b — the strong accessibility of the two chosen points of the canonical pair, which is what the dropped clause was for.
• Schoenflies.AnchoredInitialData.stronglyAccessible_a, .stronglyAccessible_b, .exists_access_segment_a, .exists_access_segment_b — lem:tangent-cone at the two anchors, the form lem:accessible-endpoints consumes at every later stage.
• Schoenflies.isWalk_initBoundary_false, Schoenflies.isWalk_initBoundary_true, Schoenflies.mem_faceCells_iff, Schoenflies.boundaryCycles_initialStructure — the boundary datum of def:matched-cellulation really is the simple boundary cycle of each 2-cell and carries exactly its strict subcells.
• Schoenflies.HexData.isPolygonal_arcOf, .isPolygonal_outerArcs, Schoenflies.isPolygonal_modelCurve, Schoenflies.InitialData.isPolygonal_tgt_edgeArc, .isPolygonal_targetRealization_skeletonSet — the clause "all its edges are polygonal" of def:admissible-graph for the target realization.
• Schoenflies.InitialData.src_arcOf_eq_image, .tgt_arcOf_eq_image, .skeletonHomeo_image_arcOf, .closure_cell_face_link, .closure_cell_face_link_homeo — clause 1 of def:matched-pair ("the two distinguished outer cycles correspond") at the level of the two boundary arcs, and the correspondence of the two 2-cell labellings.
• Schoenflies.InitialData.u_src_pos, .tgt_pos_corners, .u_a_mem_openTop, .u_b_mem_openBottom — the geometric content of the prop:initial-pair sentence: C is subdivided at the u-preimages of the four corners, and a, b lie in two nonadjacent corner arcs.
• Schoenflies.InitialData.source_cells_cover', .source_cell_isComponent', .source_closure_cell_inter', .source_cells_ne', .target_cells_cover', .target_closure_cell_inter', .target_cell_isComponent, .target_cells_ne — thm:general-crosscut on both sides, with its hypotheses supplied.
• Schoenflies.exists_initialData', Schoenflies.initial_pair' — prop:initial-pair, with the anchor clause and the matched labelling in the statement.

theorem Schoenflies.forall_isSeparating_of_isJordanCurve (S : Set Plane) : IsJordanCurve S → IsSeparating S

thm:jordan in the shape thm:general-crosscut consumes. Every consumer below feeds this to a lemma whose separating hypothesis is universally quantified over curves. (Schoenflies.isSeparating_of_isJordanCurve is the polygonal statement of Jordan.lean, and is a different hypothesis; this is the general one, now a theorem.)

Two missing HexData facts

The two boundary arcs are part of the outer cycle, and both are polygonal as soon as the six outer edges are. The second is the clause of def:admissible-graph that the target realization has to satisfy and the source one does not.

theorem Schoenflies.HexData.arcOf_false (H : HexData) : H.arcOf false = H.outer 1 '' unitInterval ∪ (H.outer 2 '' unitInterval ∪ H.outer 3 '' unitInterval)

theorem Schoenflies.HexData.arcOf_true (H : HexData) : H.arcOf true = H.outer 4 '' unitInterval ∪ (H.outer 5 '' unitInterval ∪ H.outer 0 '' unitInterval)

theorem Schoenflies.HexData.arcOf_subset_outerArcs (H : HexData) (k : Bool) : H.arcOf k ⊆ H.outerArcs

theorem Schoenflies.HexData.pos_mem_outer_of_succ (H : HexData) {i j : Fin 6} (h : i + 1 = j) : H.pos j ∈ H.outer i '' unitInterval

The vertex an outer edge ends at, named.

theorem Schoenflies.HexData.isPolygonal_arcOf (H : HexData) (hp : ∀ (i : Fin 6), IsPolygonal (H.outer i '' unitInterval)) (k : Bool) : IsPolygonal (H.arcOf k)

Each boundary arc is polygonal when the outer edges are. Three consecutive segments, glued at the two vertices between them.

theorem Schoenflies.HexData.isPolygonal_outerArcs (H : HexData) (hp : ∀ (i : Fin 6), IsPolygonal (H.outer i '' unitInterval)) : IsPolygonal H.outerArcs

The whole outer cycle is polygonal when the six outer edges are.

theorem Schoenflies.isPolygonal_modelCurve : IsPolygonal modelCurve

The model curve is polygonal. Instantiate the target realization at α = β = 0: its outer cycle is S and each of its six edges is a straight segment.

initBoundary really is the boundary walk

CellStructure.boundary is documented as a raw datum: nothing in the record forces it to walk anywhere. For initialStructure it does. Both lists are closed walks of initSkel, and the cells they run through are exactly the faceCells that initSub declares to be subcells of the corresponding 2-cell — so the base value of ≼_abs is not an independent choice.

theorem Schoenflies.initSkel_isLink_edge {i j : Fin 6} (h : i + 1 = j) : initSkel.IsLink (InitialCell.edge i) (InitialCell.vert i) (InitialCell.vert j)

An outer edge links its two consecutive vertices, with the second one named.

theorem Schoenflies.initSkel_isLink_chord : initSkel.IsLink InitialCell.chord (InitialCell.vert 1) (InitialCell.vert 4)

The chord links a and b.

theorem Schoenflies.isWalk_initBoundary_false : initSkel.IsWalk (InitialCell.vert 1) (initBoundary (InitialCell.face false)) (InitialCell.vert 1)

B₁ ∪ P is a closed walk at a.

theorem Schoenflies.isWalk_initBoundary_true : initSkel.IsWalk (InitialCell.vert 4) (initBoundary (InitialCell.face true)) (InitialCell.vert 4)

B₂ ∪ P is a closed walk at b.

theorem Schoenflies.exists_isWalk_initBoundary (k : Bool) : ∃ (v : InitialCell), initSkel.IsWalk v (initialStructure.boundary (InitialCell.face k)) v

Each 2-cell of the initial structure has a closed boundary walk.

theorem Schoenflies.initSkel_inc_iff {e x : InitialCell} : initSkel.Inc e x ↔ e ∈ InitialCell.edges ∧ (x = e.ends.1 ∨ x = e.ends.2)

Incidence in initSkel is membership among the two ends.

theorem Schoenflies.mem_faceCells_iff {k : Bool} {c : InitialCell} : c ∈ faceCells k ↔ c ∈ initBoundary (InitialCell.face k) ∨ ∃ e ∈ initBoundary (InitialCell.face k), initSkel.Inc e c

The cells of a 2-cell are the cells of its boundary walk. The base value of ≼_abs declares faceCells k to be the subcells of face k; this says faceCells k is exactly the set of edges the boundary walk takes together with the vertices it visits.

The initial face-boundary cycles

The closed-walk facts above are strengthened here to the maintained data needed by thm:finite-transfer: each boundary is a simple cycle of length at least three, and its cells are exactly the strict subcells of the corresponding face.

theorem Schoenflies.isPath_initBoundary_false_tail : initSkel.IsPath (InitialCell.vert 2) [InitialCell.edge 2, InitialCell.edge 3, InitialCell.chord] (InitialCell.vert 1)

The complementary part of the first face boundary is a simple path.

theorem Schoenflies.isPath_initBoundary_true_tail : initSkel.IsPath (InitialCell.vert 5) [InitialCell.edge 5, InitialCell.edge 0, InitialCell.chord] (InitialCell.vert 4)

The complementary part of the second face boundary is a simple path.

theorem Schoenflies.isLongCycle_initBoundary_false : initSkel.IsLongCycle (InitialCell.edge 1) (InitialCell.vert 2) (InitialCell.vert 1) [InitialCell.edge 2, InitialCell.edge 3, InitialCell.chord] (InitialCell.vert 3)

The first declared boundary list presents a long simple cycle.

theorem Schoenflies.isLongCycle_initBoundary_true : initSkel.IsLongCycle (InitialCell.edge 4) (InitialCell.vert 5) (InitialCell.vert 4) [InitialCell.edge 5, InitialCell.edge 0, InitialCell.chord] (InitialCell.vert 0)

The second declared boundary list presents a long simple cycle.

theorem Schoenflies.initSub_face_iff {k : Bool} {c : InitialCell} : initSub c (InitialCell.face k) ↔ c = InitialCell.face k ∨ c ∈ faceCells k

Incidence below an initial face consists of the face itself and its declared boundary cells.

theorem Schoenflies.mem_faceCells_iff_mem_pathCells {k : Bool} {u c : InitialCell} (hu : ∃ e ∈ initBoundary (InitialCell.face k), initSkel.Inc e u) : c ∈ faceCells k ↔ c ∈ initialStructure.pathCells u (initBoundary (InitialCell.face k))

A declared initial boundary has exactly the cells recorded by faceCells, once its starting vertex is known to occur on the boundary.

theorem Schoenflies.boundaryCycles_initialStructure : initialStructure.BoundaryCycles

The two faces of the initial matched cellulation carry chosen simple boundary cycles.

The anchor set 𝒜

prop:countable-strong-access produces a countable dense set of strongly accessible points of C; the blueprint then fixes it for the whole construction (tex 1418) and every later stage draws its new boundary vertices from it. Fixing it means it is data, so it is a structure, and prop:initial-pair takes it as an argument rather than producing its own.

structure Schoenflies.AnchorSet (C : Set Plane) : Type

The anchor set 𝒜 of tex 1403–1418: a countable dense subset of the Jordan curve C every point of which is strongly accessible from the Jordan domain D.

• carrier : Set Plane

  The points of 𝒜.

• subset_curve : self.carrier ⊆ C

  They lie on the curve.

• countable : self.carrier.Countable

  There are countably many.

• stronglyAccessible (p : Plane) : p ∈ self.carrier → StronglyAccessible (inside C) p

  Each is strongly accessible from the inside — def:strong-accessibility.

• dense : C ⊆ closure self.carrier

  They are dense in the curve.

theorem Schoenflies.AnchorSet.exists_access_segment {C : Set Plane} (A : AnchorSet C) {p : Plane} (hp : p ∈ A.carrier) : ∃ z ∈ inside C, p ≠ z ∧ openSegment ℝ p z ⊆ inside C

An anchor is the endpoint of a straight access segment into D — lem:tangent-cone.

theorem Schoenflies.AnchorSet.exists_cone {C : Set Plane} (A : AnchorSet C) {p : Plane} (hp : p ∈ A.carrier) : ∃ (v : Plane), ‖v‖ = 1 ∧ ∃ r > 0, ∀ s ≤ r, accessCone p v s ⊆ inside C

An anchor has a whole open cone of straight access segments, truncatable at any radius — lem:tangent-cone in the form the later stages need, where the segment must also avoid a compact set already drawn.

theorem Schoenflies.AnchorSet.polyAccessible {C : Set Plane} (A : AnchorSet C) {p : Plane} (hp : p ∈ A.carrier) : PolyAccessible (inside C) p

An anchor is polygonally accessible, the hypothesis lem:accessible-endpoints consumes.

theorem Schoenflies.nonempty_anchorSet {C : Set Plane} (hC : IsJordanCurve C) : Nonempty (AnchorSet C)

prop:countable-strong-access, as the fixed set 𝒜. This uses the proved Jordan curve theorem.

noncomputable def Schoenflies.anchorSet {C : Set Plane} (hC : IsJordanCurve C) : AnchorSet C

The fixed anchor set of a Jordan curve, as data.

Equations

• Schoenflies.anchorSet hC = ⋯.some

The initial matched pair, anchored

The clause of prop:initial-pair that InitialData drops. It is recorded as an extension rather than as a side theorem so that a consumer holding an initial pair holds the anchoring too; the integrator merging this file into InitialPair.lean should move the two fields into InitialData itself.

structure Schoenflies.AnchoredInitialData (C : Set Plane) (A : AnchorSet C) extends Schoenflies.InitialData C : Type

The initial matched pair with the anchor clause of prop:initial-pair: the two chosen boundary points are points of the fixed set 𝒜.

• u : Plane → Plane
• w : Plane → Plane
• homeo : IsSetHomeoOn self.u self.w C modelCurve
• curve : IsJordanCurve C
• xa : ℝ
• xb : ℝ
• abs_xa : |self.xa| < 1
• abs_xb : |self.xb| < 1
• cross : ℝ → Plane
• continuousOn_cross : ContinuousOn self.cross unitInterval
• injOn_cross : Set.InjOn self.cross unitInterval
• cross_zero : self.cross 0 = self.w (tgtPos self.xa self.xb 1)
• cross_one : self.cross 1 = self.w (tgtPos self.xa self.xb 4)
• cross_inside : self.cross '' unitInterval \ {self.w (tgtPos self.xa self.xb 1), self.w (tgtPos self.xa self.xb 4)} ⊆ inside C
• polygonal_cross : IsPolygonal (self.cross '' unitInterval)
• a_mem_anchors : self.a ∈ A.carrier

  a ∈ 𝒜.

• b_mem_anchors : self.b ∈ A.carrier

  b ∈ 𝒜.

theorem Schoenflies.AnchoredInitialData.stronglyAccessible_a {C : Set Plane} {A : AnchorSet C} (D : AnchoredInitialData C A) : StronglyAccessible (inside C) D.a

a is strongly accessible — the clause def:generated-structure and thm:finite-transfer need and InitialData does not record.

theorem Schoenflies.AnchoredInitialData.stronglyAccessible_b {C : Set Plane} {A : AnchorSet C} (D : AnchoredInitialData C A) : StronglyAccessible (inside C) D.b

b is strongly accessible.

theorem Schoenflies.AnchoredInitialData.exists_access_segment_a {C : Set Plane} {A : AnchorSet C} (D : AnchoredInitialData C A) : ∃ z ∈ inside C, D.a ≠ z ∧ openSegment ℝ D.a z ⊆ inside C

A straight access segment at a — lem:tangent-cone.

theorem Schoenflies.AnchoredInitialData.exists_access_segment_b {C : Set Plane} {A : AnchorSet C} (D : AnchoredInitialData C A) : ∃ z ∈ inside C, D.b ≠ z ∧ openSegment ℝ D.b z ⊆ inside C

A straight access segment at b.

theorem Schoenflies.AnchoredInitialData.exists_cone_a {C : Set Plane} {A : AnchorSet C} (D : AnchoredInitialData C A) : ∃ (v : Plane), ‖v‖ = 1 ∧ ∃ r > 0, ∀ s ≤ r, accessCone D.a v s ⊆ inside C

The access cone at a, truncatable — what a later crosscut ending at a is built from.

theorem Schoenflies.AnchoredInitialData.exists_cone_b {C : Set Plane} {A : AnchorSet C} (D : AnchoredInitialData C A) : ∃ (v : Plane), ‖v‖ = 1 ∧ ∃ r > 0, ∀ s ≤ r, accessCone D.b v s ⊆ inside C

The access cone at b.

theorem Schoenflies.exists_anchoredInitialData_of_homeo {C : Set Plane} (hC : IsJordanCurve C) (A : AnchorSet C) (u w : Plane → Plane) (hhom : IsSetHomeoOn u w C modelCurve) : ∃ (D : AnchoredInitialData C A), D.u = u ∧ D.w = w

prop:initial-pair including the anchor clause. The two chosen points are points of the given anchor set 𝒜; the blueprint fixes 𝒜 once and reuses it at every later stage, so it must be an input, not an output.

The proof is that of Schoenflies.exists_initialData with the anchor set supplied rather than manufactured: the two open corner arcs are relatively open and nonempty in C, 𝒜 is dense in C, so 𝒜 meets both; lem:tangent-cone (through StronglyAccessible.polyAccessible) and lem:accessible-endpoints then supply the polygonal crosscut.

theorem Schoenflies.exists_anchoredInitialData {C : Set Plane} (hC : IsJordanCurve C) (A : AnchorSet C) : Nonempty (AnchoredInitialData C A)

The anchored initial pair with a boundary parametrization chosen internally.

noncomputable def Schoenflies.anchoredInitialData {C : Set Plane} (hC : IsJordanCurve C) (A : AnchorSet C) : AnchoredInitialData C A

The initial matched pair over C anchored in 𝒜, as data. def:generated-structure builds every later stage from it, so it must be a def.

Equations

• Schoenflies.anchoredInitialData hC A = ⋯.some

theorem Schoenflies.exists_initialData' {C : Set Plane} (hC : IsJordanCurve C) (A : AnchorSet C) : ∃ (d : InitialData C), d.a ∈ A.carrier ∧ d.b ∈ A.carrier

prop:initial-pair, in the shape Schoenflies.exists_initialData should have had: harc is supplied by arc_complement and the two chosen points are anchors.

The canonical initial pair

AnchorSet is an input because the blueprint fixes 𝒜 once and every later stage draws from the same set. A consumer that has no other constraint on 𝒜 can take anchorSet hC: it is a function of C alone (Nonempty (AnchorSet C) is a Prop, so proof irrelevance makes the choice independent of the proof supplied), so all its uses agree.

noncomputable def Schoenflies.initialData {C : Set Plane} (hC : IsJordanCurve C) : InitialData C

The canonical initial matched pair over C, anchored in Schoenflies.anchorSet hC.

Equations

• Schoenflies.initialData hC = (Schoenflies.anchoredInitialData hC (Schoenflies.anchorSet hC)).toInitialData

theorem Schoenflies.initialData_a_mem_anchorSet {C : Set Plane} (hC : IsJordanCurve C) : (initialData hC).a ∈ (anchorSet hC).carrier

theorem Schoenflies.initialData_b_mem_anchorSet {C : Set Plane} (hC : IsJordanCurve C) : (initialData hC).b ∈ (anchorSet hC).carrier

theorem Schoenflies.stronglyAccessible_initialData_a {C : Set Plane} (hC : IsJordanCurve C) : StronglyAccessible (inside C) (initialData hC).a

The first chosen point of the canonical initial pair is strongly accessible. This is the clause prop:initial-pair asserts, InitialData drops, and def:generated-structure and thm:finite-transfer need in order to run a further crosscut into a.

theorem Schoenflies.stronglyAccessible_initialData_b {C : Set Plane} (hC : IsJordanCurve C) : StronglyAccessible (inside C) (initialData hC).b

The second chosen point of the canonical initial pair is strongly accessible.

The two crosscut theorems on the initial pair

InitialPair.lean carries harc (thm:arc-complement) and, on the source side, hcollars (lem:crosscut-collars). Both are theorems on main: Schoenflies.arc_complement and Schoenflies.IsCrosscut.hasArcCollars. Every consumer in Part II should use the primed forms below and thread nothing.

theorem Schoenflies.InitialData.hasArcCollarsSource {C : Set Plane} (d : InitialData C) : HasArcCollars (inside C) d.crossSet

The collar hypothesis on the source side, discharged: the crosscut is polygonal.

theorem Schoenflies.InitialData.source_cells_cover' {C : Set Plane} (d : InitialData C) : inside C \ d.crossSet = d.sourceRealization.cell (InitialCell.face false) ∪ d.sourceRealization.cell (InitialCell.face true)

The two source 2-cells exhaust D ∖ P.

theorem Schoenflies.InitialData.source_cell_isComponent' {C : Set Plane} (d : InitialData C) (k : Bool) (z : Plane) : z ∈ d.sourceRealization.cell (InitialCell.face k) → connectedComponentIn (inside C \ d.crossSet) z = d.sourceRealization.cell (InitialCell.face k)

Each source 2-cell is a component of D ∖ P.

theorem Schoenflies.InitialData.source_closure_cell_inter' {C : Set Plane} (d : InitialData C) (k : Bool) : closure (d.sourceRealization.cell (InitialCell.face k)) ∩ C = d.src.arcOf k

The labelling of the two source 2-cells.

theorem Schoenflies.InitialData.source_cells_ne' {C : Set Plane} (d : InitialData C) : d.sourceRealization.cell (InitialCell.face false) ≠ d.sourceRealization.cell (InitialCell.face true)

The two source 2-cells are distinct.

theorem Schoenflies.InitialData.target_cells_cover' {C : Set Plane} (d : InitialData C) : inside modelCurve \ d.tgt.chordSet = d.targetRealization.cell (InitialCell.face false) ∪ d.targetRealization.cell (InitialCell.face true)

The two target 2-cells exhaust Q° ∖ [u(a), u(b)].

theorem Schoenflies.InitialData.target_closure_cell_inter' {C : Set Plane} (d : InitialData C) (k : Bool) : closure (d.targetRealization.cell (InitialCell.face k)) ∩ modelCurve = d.tgt.arcOf k

The labelling of the two target 2-cells.

theorem Schoenflies.InitialData.target_cell_isComponent {C : Set Plane} (d : InitialData C) (k : Bool) (z : Plane) : z ∈ d.targetRealization.cell (InitialCell.face k) → connectedComponentIn (inside modelCurve \ d.tgt.chordSet) z = d.targetRealization.cell (InitialCell.face k)

Each target 2-cell is a component of Q° ∖ [u(a), u(b)]. The source side had this already; the target side did not.

theorem Schoenflies.InitialData.target_cells_ne {C : Set Plane} (d : InitialData C) : d.targetRealization.cell (InitialCell.face false) ≠ d.targetRealization.cell (InitialCell.face true)

The two target 2-cells are distinct.

The matched labelling

def:matched-pair clause 1 asks that "the two distinguished outer cycles correspond". On the initial pair this is not automatic from the abstract structure alone: arcOf is read off the geometry of each realization, so the two 2-cell labellings — source_closure_cell_inter' and target_closure_cell_inter' — are made independently. They correspond because the source outer edges are, by construction, the w-images of the target ones.

theorem Schoenflies.InitialData.src_outer {C : Set Plane} (d : InitialData C) (i : Fin 6) : d.src.outer i = fun (t : ℝ) => d.w (tgtOuter d.xa d.xb i t)

theorem Schoenflies.InitialData.tgt_outer {C : Set Plane} (d : InitialData C) (i : Fin 6) : d.tgt.outer i = tgtOuter d.xa d.xb i

theorem Schoenflies.InitialData.src_pos {C : Set Plane} (d : InitialData C) (i : Fin 6) : d.src.pos i = d.w (d.tgt.pos i)

theorem Schoenflies.InitialData.u_src_pos {C : Set Plane} (d : InitialData C) (i : Fin 6) : d.u (d.src.pos i) = d.tgt.pos i

Corresponding 0-cells correspond, in the geometric form prop:initial-pair states it: the six source subdivision points are the u-preimages of the four corners of Q and of u(a), u(b). (SkeletonHomeo.pos_apply says the same thing about the abstract 0-cells.)

theorem Schoenflies.InitialData.tgt_pos_corners {C : Set Plane} (d : InitialData C) : d.tgt.pos 0 = Plane.mk 1 1 ∧ d.tgt.pos 2 = Plane.mk (-1) 1 ∧ d.tgt.pos 3 = Plane.mk (-1) (-1) ∧ d.tgt.pos 5 = Plane.mk 1 (-1)

The four target corners, named.

theorem Schoenflies.InitialData.u_a_mem_openTop {C : Set Plane} (d : InitialData C) : d.u d.a ∈ openTop

The nonadjacency clause of prop:initial-pair, geometrically: u(a) lies in the relative interior of the top side of S.

theorem Schoenflies.InitialData.u_b_mem_openBottom {C : Set Plane} (d : InitialData C) : d.u d.b ∈ openBottom

u(b) lies in the relative interior of the opposite, bottom side.

theorem Schoenflies.InitialData.src_outer_image {C : Set Plane} (d : InitialData C) (i : Fin 6) : d.src.outer i '' unitInterval = d.w '' d.tgt.outer i '' unitInterval

Each source outer edge is the w-image of the corresponding target one.

theorem Schoenflies.InitialData.tgt_outer_subset_modelCurve {C : Set Plane} (d : InitialData C) (i : Fin 6) : d.tgt.outer i '' unitInterval ⊆ modelCurve

theorem Schoenflies.InitialData.u_image_w_image {C : Set Plane} (d : InitialData C) {X : Set Plane} (hX : X ⊆ modelCurve) : d.u '' d.w '' X = X

u undoes w on any subset of the model curve.

theorem Schoenflies.InitialData.tgt_arcOf_subset_modelCurve {C : Set Plane} (d : InitialData C) (k : Bool) : d.tgt.arcOf k ⊆ modelCurve

theorem Schoenflies.InitialData.src_arcOf_subset_curve {C : Set Plane} (d : InitialData C) (k : Bool) : d.src.arcOf k ⊆ C

theorem Schoenflies.InitialData.src_arcOf_eq_image {C : Set Plane} (d : InitialData C) (k : Bool) : d.src.arcOf k = d.w '' d.tgt.arcOf k

The source boundary arc is the w-image of the target one.

theorem Schoenflies.InitialData.tgt_arcOf_eq_image {C : Set Plane} (d : InitialData C) (k : Bool) : d.tgt.arcOf k = d.u '' d.src.arcOf k

The target half of the 2-cell labelling is the u-image of the source half. This is what makes the pair matched: A₁, A₂ on the source and u(A₁), u(A₂) on the target are not two independent choices of labelling, they are the same one.

theorem Schoenflies.InitialData.skeletonHomeo_image_arcOf {C : Set Plane} (d : InitialData C) (k : Bool) : d.skeletonHomeo.toFun '' d.src.arcOf k = d.tgt.arcOf k

The same statement through the skeleton homeomorphism g of def:matched-pair, which is u on the outer cycle.

theorem Schoenflies.InitialData.closure_cell_face_link {C : Set Plane} (d : InitialData C) (k : Bool) : closure (d.targetRealization.cell (InitialCell.face k)) ∩ modelCurve = d.u '' (closure (d.sourceRealization.cell (InitialCell.face k)) ∩ C)

The two 2-cell labellings correspond. lem:crosscut-side-correspondence reads the labelling of a crosscut side off the closure of the side; on a matched pair the source and the target answers are u-images of one another, for the same abstract 2-cell face k.

theorem Schoenflies.InitialData.closure_cell_face_link_homeo {C : Set Plane} (d : InitialData C) (k : Bool) : d.skeletonHomeo.toFun '' (closure (d.sourceRealization.cell (InitialCell.face k)) ∩ C) = closure (d.targetRealization.cell (InitialCell.face k)) ∩ modelCurve

The same through g.

def:admissible-graph for the target: every edge is polygonal

theorem Schoenflies.InitialData.isPolygonal_tgt_outer {C : Set Plane} (d : InitialData C) (i : Fin 6) : IsPolygonal (d.tgt.outer i '' unitInterval)

Each target outer edge is a straight segment, hence polygonal.

theorem Schoenflies.InitialData.isPolygonal_tgt_edgeArc {C : Set Plane} (d : InitialData C) {e : InitialCell} (he : e ∈ initSkel.edgeSet) : IsPolygonal (Graph.edgeArc d.tgt.draw e)

Every edge of the target realization is polygonal — the clause of def:admissible-graph for an admissible graph in Q that InitialPair.lean leaves unstated.

theorem Schoenflies.InitialData.isPolygonal_tgt_arcOf {C : Set Plane} (d : InitialData C) (k : Bool) : IsPolygonal (d.tgt.arcOf k)

Both target boundary arcs are polygonal.

theorem Schoenflies.InitialData.isPolygonal_targetRealization_skeletonSet {C : Set Plane} (d : InitialData C) : IsPolygonal d.targetRealization.skeletonSet

The whole target skeleton is polygonal.

theorem Schoenflies.InitialData.isPolygonal_src_nonboundary_edgeArc {C : Set Plane} (d : InitialData C) : IsPolygonal (Graph.edgeArc d.src.draw InitialCell.chord) ∧ Graph.edgeArc d.src.draw InitialCell.chord \ C ⊆ inside C

The source realization satisfies the source form of def:admissible-graph: its edges not contained in C — here only the crosscut — are polygonal, with interior in D.

theorem Schoenflies.initial_pair' {C : Set Plane} (hC : IsJordanCurve C) (A : AnchorSet C) : ∃ (d : InitialData C), d.a ∈ A.carrier ∧ d.b ∈ A.carrier ∧ StronglyAccessible (inside C) d.a ∧ StronglyAccessible (inside C) d.b ∧ d.u d.a ∈ openTop ∧ d.u d.b ∈ openBottom ∧ (∀ (i : Fin 6), d.u (d.src.pos i) = d.tgt.pos i) ∧ d.sourceRealization.graph.IsTwoConnected ∧ d.targetRealization.graph.IsTwoConnected ∧ d.sourceRealization.outerSet = C ∧ d.targetRealization.outerSet = modelCurve ∧ IsConnected d.sourceRealization.nonboundary ∧ IsConnected d.targetRealization.nonboundary ∧ IsPolygonal d.crossSet ∧ (∀ e ∈ initSkel.edgeSet, IsPolygonal (Graph.edgeArc d.tgt.draw e)) ∧ d.tgt.chordSet = segment ℝ (d.u d.a) (d.u d.b) ∧ (∀ x ∈ C, d.skeletonHomeo.toFun x = d.u x) ∧ (∀ (k : Bool), d.tgt.arcOf k = d.u '' d.src.arcOf k) ∧ (∀ (k : Bool), closure (d.sourceRealization.cell (InitialCell.face k)) ∩ C = d.src.arcOf k) ∧ ∀ (k : Bool), closure (d.targetRealization.cell (InitialCell.face k)) ∩ modelCurve = d.tgt.arcOf k

prop:initial-pair, assembled and complete.

Over any Jordan curve C and any fixed anchor set 𝒜 there is a matched pair whose source realization is C subdivided at the u-preimages of the four corners of Q and at two further points a, b ∈ 𝒜 lying in two nonadjacent corner arcs, together with one polygonal crosscut of D from a to b, and whose target realization is S correspondingly subdivided together with the straight chord [u(a), u(b)].

Beyond Schoenflies.initial_pair this adds: no hypotheses at all; the anchor clause with its consequence that a and b are strongly accessible; the polygonality of every target edge; and the fact that the two 2-cell labellings correspond.